English
The map sending a triple (a,b,c) to the explicit triangle {in0 a, in1 b, in2 c} is an embedding of α×β×γ into Finset(α⊕β⊕γ).
Русский
Отображение тройки $(a,b,c)$ в явный треугольник $\\{in_0 a, in_1 b, in_2 c\\}$ является вложением в множество трёхктавых вершин.
LaTeX
$$@[simp] def toTriangle : α × β × γ ↪ Finset (α ⊕ β ⊕ γ) with toFun and inj'.$$
Lean4
/-- 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 : γ`. -/
theorem graph_triple ⦃x y z⦄ :
(graph t).Adj x y →
(graph t).Adj x z →
(graph t).Adj y z →
∃ a b c,
({in₀ a, in₁ b, in₂ c} : Finset (α ⊕ β ⊕ γ)) = { x, y, z } ∧
(graph t).Adj (in₀ a) (in₁ b) ∧ (graph t).Adj (in₀ a) (in₂ c) ∧ (graph t).Adj (in₁ b) (in₂ c) :=
by
rintro (_ | _ | _) (_ | _ | _) (_ | _ | _) <;>
refine ⟨_, _, _, by ext; simp only [Finset.mem_insert, Finset.mem_singleton]; try tauto, ?_, ?_, ?_⟩ <;>
constructor <;>
assumption
