Construct a tripartite graph from its triangles

This file contains the construction of a simple graph on α ⊕ β ⊕ γ from a list of triangles (a, b, c) (with a in the first component, b in the second, c in the third).

We call

• t : Finset (α × β × γ) the set of triangle indices (its elements are not triangles within the graph but instead index them).
• explicit a triangle of the constructed graph coming from a triangle index.
• accidental a triangle of the constructed graph not coming from a triangle index.

The two important properties of this construction are:

• SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint: Whether the explicit triangles are edge-disjoint.
• SimpleGraph.TripartiteFromTriangles.NoAccidental: Whether all triangles are explicit.

This construction shows up unrelatedly twice in the theory of Roth numbers:

• The lower bound of the Ruzsa-Szemerédi problem: From a set s in a finite abelian group G of odd order, we construct a tripartite graph on G ⊕ G ⊕ G. The triangle indices are (x, x + a, x + 2 * a) for x any element and a ∈ s. The explicit triangles are always edge-disjoint and there is no accidental triangle if s is 3AP-free.
• The proof of the corners theorem from the triangle removal lemma: For a set s in a finite abelian group G, we construct a tripartite graph on G ⊕ G ⊕ G, whose vertices correspond to the horizontal, vertical and diagonal lines in G × G. The explicit triangles are (h, v, d) where h, v, d are horizontal, vertical, diagonal lines that intersect in an element of s. The explicit triangles are always edge-disjoint and there is no accidental triangle if s is corner-free.

theorem SimpleGraph.TripartiteFromTriangles.rel_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : Finset (α × β × γ)) : ∀ (a a_1 : α ⊕ β ⊕ γ), SimpleGraph.TripartiteFromTriangles.Rel t a a_1 ↔ (∃ (a_2 : α) (b : β) (c : γ), (a_2, b, c) ∈ t ∧ a = Sum3.in₀ a_2 ∧ a_1 = Sum3.in₁ b) ∨ (∃ (a_2 : α) (b : β) (c : γ), (a_2, b, c) ∈ t ∧ a = Sum3.in₁ b ∧ a_1 = Sum3.in₀ a_2) ∨ (∃ (a_2 : α) (b : β) (c : γ), (a_2, b, c) ∈ t ∧ a = Sum3.in₀ a_2 ∧ a_1 = Sum3.in₂ c) ∨ (∃ (a_2 : α) (b : β) (c : γ), (a_2, b, c) ∈ t ∧ a = Sum3.in₂ c ∧ a_1 = Sum3.in₀ a_2) ∨ (∃ (a_2 : α) (b : β) (c : γ), (a_2, b, c) ∈ t ∧ a = Sum3.in₁ b ∧ a_1 = Sum3.in₂ c) ∨ ∃ (a_2 : α) (b : β) (c : γ), (a_2, b, c) ∈ t ∧ a = Sum3.in₂ c ∧ a_1 = Sum3.in₁ b

inductive SimpleGraph.TripartiteFromTriangles.Rel {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : Finset (α × β × γ)) : α ⊕ β ⊕ γ → α ⊕ β ⊕ γ → Prop

The underlying relation of the tripartite-from-triangles graph.

Two vertices are related iff there exists a triangle index containing them both.

• in₀₁: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, (a, b, c) ∈ t → SimpleGraph.TripartiteFromTriangles.Rel t (Sum3.in₀ a) (Sum3.in₁ b)
• in₁₀: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, (a, b, c) ∈ t → SimpleGraph.TripartiteFromTriangles.Rel t (Sum3.in₁ b) (Sum3.in₀ a)
• in₀₂: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, (a, b, c) ∈ t → SimpleGraph.TripartiteFromTriangles.Rel t (Sum3.in₀ a) (Sum3.in₂ c)
• in₂₀: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, (a, b, c) ∈ t → SimpleGraph.TripartiteFromTriangles.Rel t (Sum3.in₂ c) (Sum3.in₀ a)
• in₁₂: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, (a, b, c) ∈ t → SimpleGraph.TripartiteFromTriangles.Rel t (Sum3.in₁ b) (Sum3.in₂ c)
• in₂₁: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, (a, b, c) ∈ t → SimpleGraph.TripartiteFromTriangles.Rel t (Sum3.in₂ c) (Sum3.in₁ b)

theorem SimpleGraph.TripartiteFromTriangles.rel_irrefl {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} (x : α ⊕ β ⊕ γ) : ¬SimpleGraph.TripartiteFromTriangles.Rel t x x

theorem SimpleGraph.TripartiteFromTriangles.rel_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} : Symmetric (SimpleGraph.TripartiteFromTriangles.Rel t)

def SimpleGraph.TripartiteFromTriangles.graph {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : Finset (α × β × γ)) : SimpleGraph (α ⊕ β ⊕ γ)

The tripartite-from-triangles graph. Two vertices are related iff there exists a triangle index containing them both.

Equations

• SimpleGraph.TripartiteFromTriangles.graph t = { Adj := SimpleGraph.TripartiteFromTriangles.Rel t, symm := ⋯, loopless := ⋯ }

@[simp]

theorem SimpleGraph.TripartiteFromTriangles.Graph.not_in₀₀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {a : α} {a' : α} : ¬(SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₀ a) (Sum3.in₀ a')

@[simp]

theorem SimpleGraph.TripartiteFromTriangles.Graph.not_in₁₁ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {b : β} {b' : β} : ¬(SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₁ b) (Sum3.in₁ b')

@[simp]

theorem SimpleGraph.TripartiteFromTriangles.Graph.not_in₂₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {c : γ} {c' : γ} : ¬(SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₂ c) (Sum3.in₂ c')

@[simp]

theorem SimpleGraph.TripartiteFromTriangles.Graph.in₀₁_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {a : α} {b : β} : (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₀ a) (Sum3.in₁ b) ↔ ∃ (c : γ), (a, b, c) ∈ t

@[simp]

theorem SimpleGraph.TripartiteFromTriangles.Graph.in₁₀_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {a : α} {b : β} : (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₁ b) (Sum3.in₀ a) ↔ ∃ (c : γ), (a, b, c) ∈ t

@[simp]

theorem SimpleGraph.TripartiteFromTriangles.Graph.in₀₂_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {a : α} {c : γ} : (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₀ a) (Sum3.in₂ c) ↔ ∃ (b : β), (a, b, c) ∈ t

@[simp]

theorem SimpleGraph.TripartiteFromTriangles.Graph.in₂₀_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {a : α} {c : γ} : (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₂ c) (Sum3.in₀ a) ↔ ∃ (b : β), (a, b, c) ∈ t

@[simp]

theorem SimpleGraph.TripartiteFromTriangles.Graph.in₁₂_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {b : β} {c : γ} : (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₁ b) (Sum3.in₂ c) ↔ ∃ (a : α), (a, b, c) ∈ t

@[simp]

theorem SimpleGraph.TripartiteFromTriangles.Graph.in₂₁_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {b : β} {c : γ} : (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₂ c) (Sum3.in₁ b) ↔ ∃ (a : α), (a, b, c) ∈ t

theorem SimpleGraph.TripartiteFromTriangles.Graph.in₀₁_iff' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {a : α} {b : β} : (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₀ a) (Sum3.in₁ b) ↔ ∃ x ∈ t, x.1 = a ∧ x.2.1 = b

theorem SimpleGraph.TripartiteFromTriangles.Graph.in₁₀_iff' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {a : α} {b : β} : (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₁ b) (Sum3.in₀ a) ↔ ∃ x ∈ t, x.2.1 = b ∧ x.1 = a

theorem SimpleGraph.TripartiteFromTriangles.Graph.in₀₂_iff' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {a : α} {c : γ} : (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₀ a) (Sum3.in₂ c) ↔ ∃ x ∈ t, x.1 = a ∧ x.2.2 = c

theorem SimpleGraph.TripartiteFromTriangles.Graph.in₂₀_iff' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {a : α} {c : γ} : (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₂ c) (Sum3.in₀ a) ↔ ∃ x ∈ t, x.2.2 = c ∧ x.1 = a

theorem SimpleGraph.TripartiteFromTriangles.Graph.in₁₂_iff' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {b : β} {c : γ} : (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₁ b) (Sum3.in₂ c) ↔ ∃ x ∈ t, x.2.1 = b ∧ x.2.2 = c

theorem SimpleGraph.TripartiteFromTriangles.Graph.in₂₁_iff' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {b : β} {c : γ} : (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₂ c) (Sum3.in₁ b) ↔ ∃ x ∈ t, x.2.2 = c ∧ x.2.1 = b

class SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : Finset (α × β × γ)) : Prop

Predicate on the triangle indices for the explicit triangles to be edge-disjoint.

• inj₀ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄ ⦃a' : α⦄, (a, b, c) ∈ t → (a', b, c) ∈ t → a = a'
• inj₁ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄ ⦃b' : β⦄, (a, b, c) ∈ t → (a, b', c) ∈ t → b = b'
• inj₂ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c c' : γ⦄, (a, b, c) ∈ t → (a, b, c') ∈ t → c = c'

theorem SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint.inj₀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} [self : SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint t] ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄ ⦃a' : α⦄ : (a, b, c) ∈ t → (a', b, c) ∈ t → a = a'

theorem SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint.inj₁ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} [self : SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint t] ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄ ⦃b' : β⦄ : (a, b, c) ∈ t → (a, b', c) ∈ t → b = b'

theorem SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint.inj₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} [self : SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint t] ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄ ⦃c' : γ⦄ : (a, b, c) ∈ t → (a, b, c') ∈ t → c = c'

class SimpleGraph.TripartiteFromTriangles.NoAccidental {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : Finset (α × β × γ)) : Prop

Predicate on the triangle indices for there to be no accidental triangle.

Note that we cheat a bit, since the exact translation of this informal description would have (a', b', c') ∈ t as a conclusion rather than a = a' ∨ b = b' ∨ c = c'. Those conditions are equivalent when the explicit triangles are edge-disjoint (which is the case we care about).

• eq_or_eq_or_eq : ∀ ⦃a a' : α⦄ ⦃b b' : β⦄ ⦃c c' : γ⦄, (a', b, c) ∈ t → (a, b', c) ∈ t → (a, b, c') ∈ t → a = a' ∨ b = b' ∨ c = c'

theorem SimpleGraph.TripartiteFromTriangles.NoAccidental.eq_or_eq_or_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} [self : SimpleGraph.TripartiteFromTriangles.NoAccidental t] ⦃a : α⦄ ⦃a' : α⦄ ⦃b : β⦄ ⦃b' : β⦄ ⦃c : γ⦄ ⦃c' : γ⦄ : (a', b, c) ∈ t → (a, b', c) ∈ t → (a, b, c') ∈ t → a = a' ∨ b = b' ∨ c = c'

instance SimpleGraph.TripartiteFromTriangles.graph.instDecidableRelAdj {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} [DecidableEq α] [DecidableEq β] [DecidableEq γ] : DecidableRel (SimpleGraph.TripartiteFromTriangles.graph t).Adj

Equations

• SimpleGraph.TripartiteFromTriangles.graph.instDecidableRelAdj (Sum.inl _a) (Sum.inl _a') = isFalse ⋯
• SimpleGraph.TripartiteFromTriangles.graph.instDecidableRelAdj (Sum.inl _a) (Sum.inr (Sum.inl _b')) = decidable_of_iff' (∃ x ∈ t, x.1 = _a ∧ x.2.1 = _b') ⋯
• SimpleGraph.TripartiteFromTriangles.graph.instDecidableRelAdj (Sum.inl _a) (Sum.inr (Sum.inr _c')) = decidable_of_iff' (∃ x ∈ t, x.1 = _a ∧ x.2.2 = _c') ⋯
• SimpleGraph.TripartiteFromTriangles.graph.instDecidableRelAdj (Sum.inr (Sum.inl _b)) (Sum.inl _a') = decidable_of_iff' (∃ x ∈ t, x.2.1 = _b ∧ x.1 = _a') ⋯
• SimpleGraph.TripartiteFromTriangles.graph.instDecidableRelAdj (Sum.inr (Sum.inl _b)) (Sum.inr (Sum.inl _b')) = isFalse ⋯
• SimpleGraph.TripartiteFromTriangles.graph.instDecidableRelAdj (Sum.inr (Sum.inl _b)) (Sum.inr (Sum.inr _b')) = decidable_of_iff' (∃ x ∈ t, x.2.1 = _b ∧ x.2.2 = _b') ⋯
• SimpleGraph.TripartiteFromTriangles.graph.instDecidableRelAdj (Sum.inr (Sum.inr _c)) (Sum.inl _a') = decidable_of_iff' (∃ x ∈ t, x.2.2 = _c ∧ x.1 = _a') ⋯
• SimpleGraph.TripartiteFromTriangles.graph.instDecidableRelAdj (Sum.inr (Sum.inr _c)) (Sum.inr (Sum.inl _b')) = decidable_of_iff' (∃ x ∈ t, x.2.2 = _c ∧ x.2.1 = _b') ⋯
• SimpleGraph.TripartiteFromTriangles.graph.instDecidableRelAdj (Sum.inr (Sum.inr _c)) (Sum.inr (Sum.inr _b')) = isFalse ⋯

theorem SimpleGraph.TripartiteFromTriangles.graph_triple {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} [DecidableEq α] [DecidableEq β] [DecidableEq γ] ⦃x : α ⊕ β ⊕ γ⦄ ⦃y : α ⊕ β ⊕ γ⦄ ⦃z : α ⊕ β ⊕ γ⦄ : (SimpleGraph.TripartiteFromTriangles.graph t).Adj x y → (SimpleGraph.TripartiteFromTriangles.graph t).Adj x z → (SimpleGraph.TripartiteFromTriangles.graph t).Adj y z → ∃ (a : α) (b : β) (c : γ), {Sum3.in₀ a, Sum3.in₁ b, Sum3.in₂ c} = {x, y, z} ∧ (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₀ a) (Sum3.in₁ b) ∧ (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₀ a) (Sum3.in₂ c) ∧ (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₁ b) (Sum3.in₂ c)

This lemma reorders the elements of a triangle in the tripartite graph. It turns a triangle {x, y, z} into a triangle {a, b, c} where a : α , b : β, c : γ.

@[simp]

theorem SimpleGraph.TripartiteFromTriangles.toTriangle_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq α] [DecidableEq β] [DecidableEq γ] (x : α × β × γ) : SimpleGraph.TripartiteFromTriangles.toTriangle x = {Sum3.in₀ x.1, Sum3.in₁ x.2.1, Sum3.in₂ x.2.2}

def SimpleGraph.TripartiteFromTriangles.toTriangle {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq α] [DecidableEq β] [DecidableEq γ] : α × β × γ ↪ Finset (α ⊕ β ⊕ γ)

The map that turns a triangle index into an explicit triangle.

Equations

• SimpleGraph.TripartiteFromTriangles.toTriangle = { toFun := fun (x : α × β × γ) => {Sum3.in₀ x.1, Sum3.in₁ x.2.1, Sum3.in₂ x.2.2}, inj' := ⋯ }

theorem SimpleGraph.TripartiteFromTriangles.toTriangle_is3Clique {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {x : α × β × γ} [DecidableEq α] [DecidableEq β] [DecidableEq γ] (hx : x ∈ t) : (SimpleGraph.TripartiteFromTriangles.graph t).IsNClique 3 (SimpleGraph.TripartiteFromTriangles.toTriangle x)

theorem SimpleGraph.TripartiteFromTriangles.exists_mem_toTriangle {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} [DecidableEq α] [DecidableEq β] [DecidableEq γ] {x : α ⊕ β ⊕ γ} {y : α ⊕ β ⊕ γ} (hxy : (SimpleGraph.TripartiteFromTriangles.graph t).Adj x y) : ∃ z ∈ t, x ∈ SimpleGraph.TripartiteFromTriangles.toTriangle z ∧ y ∈ SimpleGraph.TripartiteFromTriangles.toTriangle z

theorem SimpleGraph.TripartiteFromTriangles.is3Clique_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} [DecidableEq α] [DecidableEq β] [DecidableEq γ] [SimpleGraph.TripartiteFromTriangles.NoAccidental t] {s : Finset (α ⊕ β ⊕ γ)} : (SimpleGraph.TripartiteFromTriangles.graph t).IsNClique 3 s ↔ ∃ x ∈ t, SimpleGraph.TripartiteFromTriangles.toTriangle x = s

theorem SimpleGraph.TripartiteFromTriangles.toTriangle_surjOn {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} [DecidableEq α] [DecidableEq β] [DecidableEq γ] [SimpleGraph.TripartiteFromTriangles.NoAccidental t] : Set.SurjOn (⇑SimpleGraph.TripartiteFromTriangles.toTriangle) (↑t) ((SimpleGraph.TripartiteFromTriangles.graph t).cliqueSet 3)

theorem SimpleGraph.TripartiteFromTriangles.map_toTriangle_disjoint {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : Finset (α × β × γ)) [DecidableEq α] [DecidableEq β] [DecidableEq γ] [SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint t] : (↑(Finset.map SimpleGraph.TripartiteFromTriangles.toTriangle t)).Pairwise fun (x y : Finset (α ⊕ β ⊕ γ)) => (↑x ∩ ↑y).Subsingleton

theorem SimpleGraph.TripartiteFromTriangles.cliqueSet_eq_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : Finset (α × β × γ)) [DecidableEq α] [DecidableEq β] [DecidableEq γ] [SimpleGraph.TripartiteFromTriangles.NoAccidental t] : (SimpleGraph.TripartiteFromTriangles.graph t).cliqueSet 3 = ⇑SimpleGraph.TripartiteFromTriangles.toTriangle '' ↑t

theorem SimpleGraph.TripartiteFromTriangles.cliqueFinset_eq_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : Finset (α × β × γ)) [DecidableEq α] [DecidableEq β] [DecidableEq γ] [Fintype α] [Fintype β] [Fintype γ] [SimpleGraph.TripartiteFromTriangles.NoAccidental t] : (SimpleGraph.TripartiteFromTriangles.graph t).cliqueFinset 3 = Finset.image (⇑SimpleGraph.TripartiteFromTriangles.toTriangle) t

theorem SimpleGraph.TripartiteFromTriangles.cliqueFinset_eq_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : Finset (α × β × γ)) [DecidableEq α] [DecidableEq β] [DecidableEq γ] [Fintype α] [Fintype β] [Fintype γ] [SimpleGraph.TripartiteFromTriangles.NoAccidental t] : (SimpleGraph.TripartiteFromTriangles.graph t).cliqueFinset 3 = Finset.map SimpleGraph.TripartiteFromTriangles.toTriangle t

@[simp]

theorem SimpleGraph.TripartiteFromTriangles.card_triangles {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : Finset (α × β × γ)) [DecidableEq α] [DecidableEq β] [DecidableEq γ] [Fintype α] [Fintype β] [Fintype γ] [SimpleGraph.TripartiteFromTriangles.NoAccidental t] : ((SimpleGraph.TripartiteFromTriangles.graph t).cliqueFinset 3).card = t.card

theorem SimpleGraph.TripartiteFromTriangles.farFromTriangleFree {α : Type u_1} {β : Type u_2} {γ : Type u_3} {𝕜 : Type u_4} [LinearOrderedField 𝕜] (t : Finset (α × β × γ)) [DecidableEq α] [DecidableEq β] [DecidableEq γ] [Fintype α] [Fintype β] [Fintype γ] [SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint t] {ε : 𝕜} (ht : ε * ↑((Fintype.card α + Fintype.card β + Fintype.card γ) ^ 2) ≤ ↑t.card) : (SimpleGraph.TripartiteFromTriangles.graph t).FarFromTriangleFree ε

theorem SimpleGraph.TripartiteFromTriangles.locallyLinear {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : Finset (α × β × γ)) [SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint t] [SimpleGraph.TripartiteFromTriangles.NoAccidental t] : (SimpleGraph.TripartiteFromTriangles.graph t).LocallyLinear