not_cliqueFree_iff — Mathlib

English

Not G.CliqueFree n if and only if there exists a complete graph on Fin n embeddable into G.

Русский

Не G.CliqueFree n тогда и только тогда, когда существует вложение полного графа на Fin n в G.

LaTeX

$$$ \neg G.CliqueFree(n) \iff \text{Nonempty}((\mathrm{completeGraph}(\mathrm{Fin} n)) \hookrightarrow G). $$$

Lean4

theorem not_cliqueFree_iff (n : ℕ) : ¬G.CliqueFree n ↔ Nonempty (completeGraph (Fin n) ↪g G) :=
  ⟨fun h ↦ ⟨topEmbeddingOfNotCliqueFree h⟩, fun ⟨f⟩ ↦ not_cliqueFree_of_top_embedding f⟩

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