English
A triangle decomposition statement that any triangle in the tripartite-from-triangles graph corresponds to a triple (a,b,c) forming edges among the three parts.
Русский
В графе тройного разбиения любой треугольник соответствует тройке (a,b,c), образующей рёбра между всеми тремя частями.
LaTeX
$$If $x,y,z$ are pairwise adjacent in graph $t$, then there exist $a,b,c$ such that $\\{in_0 a, in_1 b, in_2 c\\} = \\{x,y,z\\}$ and the three adjacencies hold.$$
Lean4
instance instDecidableRelAdj : DecidableRel (graph t).Adj
| in₀ _a, in₀ _a' => Decidable.isFalse not_in₀₀
| in₀ _a, in₁ _b' => decidable_of_iff' _ in₀₁_iff'
| in₀ _a, in₂ _c' => decidable_of_iff' _ in₀₂_iff'
| in₁ _b, in₀ _a' => decidable_of_iff' _ in₁₀_iff'
| in₁ _b, in₁ _b' => Decidable.isFalse not_in₁₁
| in₁ _b, in₂ _b' => decidable_of_iff' _ in₁₂_iff'
| in₂ _c, in₀ _a' => decidable_of_iff' _ in₂₀_iff'
| in₂ _c, in₁ _b' => decidable_of_iff' _ in₂₁_iff'
| in₂ _c, in₂ _b' => Decidable.isFalse not_in₂₂
