toTriangle_is3Clique — Mathlib

English

Variant statement that the three edges among the vertices of toTriangle x form a triangle when x ∈ t.

Русский

Вариант утверждения: три ребра между вершинами toTriangle x образуют треугольник при x∈t.

LaTeX

$$$(graph\\ t).IsNClique 3\\ (toTriangle x) \\;\\text{for } x \\in t$, i.e. the three pairwise adjacencies hold.$$

Lean4

theorem toTriangle_is3Clique (hx : x ∈ t) : (graph t).IsNClique 3 (toTriangle x) :=
  by
  simp only [toTriangle_apply, is3Clique_triple_iff, in₀₁_iff, in₀₂_iff, in₁₂_iff]
  exact ⟨⟨_, hx⟩, ⟨_, hx⟩, _, hx⟩

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