in₁₂_iff' — Mathlib

English

A triangle in the tripartite-from-triangles graph corresponds to a triple (a,b,c) ∈ α×β×γ giving edges among all three parts.

Русский

Каждый треугольник графа задаётся тройкой $a,b,c$ и образует тройку рёбра между частями.

LaTeX

$$If $x,y,z$ are pairwise adjacent in $graph\\ t$, then there exist $a,b,c$ with $\\{in_0 a, in_1 b, in_2 c\\} = \\{x,y,z\\}$ and the three edges hold as above.$$

Lean4

theorem in₁₂_iff' : (graph t).Adj (in₁ b) (in₂ c) ↔ ∃ x : α × β × γ, x ∈ t ∧ x.2.1 = b ∧ x.2.2 = c
    where
  mp := by rintro ⟨⟩; exact ⟨_, ‹_›, by simp⟩
  mpr := by rintro ⟨⟨a, b, c⟩, h, rfl, rfl⟩; constructor; assumption

Похожие утверждения