mono — Mathlib

English

A restatement of edge-disjoint triangles in terms of subsingleton conditions for Sym2 edges, along with other elementary equivalences.

Русский

Переформулировка независимых треугольников через условия Subsingleton для ребер Sym2.

LaTeX

$$Iff (G.EdgeDisjointTriangles) ((∀ ⦃e : Sym2 α⦄, ¬e.IsDiag → {s ∈ G.cliqueSet 3 | e ∈ (s : Finset α).sym2}.Subsingleton))$$

Lean4

nonrec theorem mono (hε : G.FarFromTriangleFree ε) (h : δ ≤ ε) : G.FarFromTriangleFree δ :=
  hε.mono <| by gcongr

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