English
If three vertices x,y,z form a triangle in the tripartite-from-triangles graph, then there exist coordinates a,b,c with x,y,z equal to {in0 a, in1 b, in2 c} and with all three pairwise adjacencies.
Русский
Если три вершины x,y,z образуют треугольник в графе, построенном из тройки α,β,γ, то найдутся a,b,c такие, что {x,y,z} = {in0 a, in1 b, in2 c} и все пары смежны.
LaTeX
$$If $(graph\\ t).Adj x y$, $(graph\\ t).Adj x z$, and $(graph\\ t).Adj y z$, then there exist $a,b,c$ with $\\{\\mathrm{in}_0 a,\\mathrm{in}_1 b,\\mathrm{in}_2 c\\} = \\{x,y,z\\}$ and $(graph\\ t).Adj (\\mathrm{in}_0 a)(\\mathrm{in}_1 b)$, $(graph\\ t).Adj (\\mathrm{in}_0 a)(\\mathrm{in}_2 c)$, $(graph\\ t).Adj (\\mathrm{in}_1 b)(\\mathrm{in}_2 c)$.$$
Lean4
theorem in₁₀_iff' : (graph t).Adj (in₁ b) (in₀ a) ↔ ∃ x : α × β × γ, x ∈ t ∧ x.2.1 = b ∧ x.1 = a
where
mp := by rintro ⟨⟩; exact ⟨_, ‹_›, by simp⟩
mpr := by rintro ⟨⟨a, b, c⟩, h, rfl, rfl⟩; constructor; assumption
