toTriangle — Mathlib

English

If x ∈ t, then the three vertices given by toTriangle x form a 3-clique in graph t.

Русский

Если $x\\in t$, то три вершины, образованные $toTriangle x$, образуют тройку, смежную между собой.

LaTeX

$$If $\\,x\\in t$, then $(graph\\ t).IsNClique 3\\ (toTriangle x)$.$$

Lean4

/-- The map that turns a triangle index into an explicit triangle. -/
@[simps]
def toTriangle : α × β × γ ↪ Finset (α ⊕ β ⊕ γ)
    where
  toFun x := {in₀ x.1, in₁ x.2.1, in₂ x.2.2}
  inj' := fun ⟨a, b, c⟩ ⟨a', b', c'⟩ ↦ by
    simpa only [Finset.Subset.antisymm_iff, Finset.subset_iff, mem_insert, mem_singleton, forall_eq_or_imp, forall_eq,
      Prod.mk_inj, or_false, false_or, in₀, in₁, in₂, Sum.inl.inj_iff, Sum.inr.inj_iff, reduceCtorEq] using And.left

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