cliqueSet_eq_image — Mathlib

English

For NoAccidental t, a set s is a 3-clique of graph t if and only if s equals toTriangle x for some x ∈ t.

Русский

Для NoAccidental t множество s является 3-кликой графа t тогда и только тогда, когда существует x ∈ t такое, что s = toTriangle x.

LaTeX

$$$ (graph\ t).IsNClique\ 3\ s \iff \exists x\in t:\ toTriangle\ x = s $$$

Lean4

theorem cliqueSet_eq_image [NoAccidental t] : (graph t).cliqueSet 3 = toTriangle '' t := by ext; exact is3Clique_iff

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