def NOF.forget {ι : Type u_1} {G : Type u_2} (i : ι) (x : ι → G) (j : { j : ι // j ≠ i }) : G

Equations

• NOF.forget i x j = x ↑j

def NOF.IsForbiddenPatternWithTip {ι : Type u_1} {G : Type u_2} (a : ι → ι → G) (v : ι → G) : Prop

Equations

• NOF.IsForbiddenPatternWithTip a v = ∀ ⦃i j : ι⦄, i ≠ j → a i j = v j

def NOF.IsForbiddenPattern {ι : Type u_1} {G : Type u_2} (a : ι → ι → G) : Prop

Equations

• NOF.IsForbiddenPattern a = ∃ (v : ι → G), NOF.IsForbiddenPatternWithTip a v

theorem NOF.isForbiddenPatternWithTip_iff_forget {ι : Type u_1} {G : Type u_2} {a : ι → ι → G} {v : ι → G} : IsForbiddenPatternWithTip a v ↔ ∀ (i : ι), forget i v = forget i (a i)

theorem NOF.IsForbiddenPatternWithTip.forget {ι : Type u_1} {G : Type u_2} {a : ι → ι → G} {v : ι → G} : IsForbiddenPatternWithTip a v → ∀ (i : ι), forget i v = forget i (a i)

Alias of the forward direction of NOF.isForbiddenPatternWithTip_iff_forget.

theorem NOF.IsForbiddenPatternWithTip.of_forget {ι : Type u_1} {G : Type u_2} {a : ι → ι → G} {v : ι → G} : (∀ (i : ι), forget i v = forget i (a i)) → IsForbiddenPatternWithTip a v

Alias of the reverse direction of NOF.isForbiddenPatternWithTip_iff_forget.

structure NOF.IsMultidimCorner {ι : Type u_1} {G : Type u_2} [Fintype ι] [AddCommGroup G] (a : ι → ι → G) (b : ι → G) : Prop

• sum_eq_sum (i j : ι) : ∑ k : ι, a i k = ∑ k : ι, a j k
• isForbiddenPatternWithTip : IsForbiddenPatternWithTip a b

theorem NOF.isMultidimCorner_forget_of_isForbiddenPattern {ι : Type u_1} {G : Type u_2} [Fintype ι] [AddCommGroup G] [DecidableEq ι] (a : ι → ι → G) (h : IsForbiddenPattern a) (hS : ∀ (i : ι), ∑ j : ι, a i j = 0) (i : ι) : IsMultidimCorner (fun (j : { j : ι // j ≠ i }) => forget i (a ↑j)) (forget i (a i))