cliqueFree_iff_top_free — Mathlib

English

For a finite β, G has no card β clique iff the top copy on β does not embed into G.

Русский

Для конечного β граф G не имеет клики размера card β тогда и только тогда, когда копия вершины сверху на β не вложена в G.

LaTeX

$$$ \forall \beta\, (\text{card}\beta = n) : G.CliqueFree(n) \iff (\top : SimpleGraph\, \beta).Free G. $$$

Lean4

/-- A simple graph has no `card β`-cliques iff it does not contain `⊤ : SimpleGraph β`. -/
theorem cliqueFree_iff_top_free {β : Type*} [Fintype β] : G.CliqueFree (card β) ↔ (⊤ : SimpleGraph β).Free G :=
  by
  rw [← not_iff_not, not_free, not_cliqueFree_iff, isContained_congr (Iso.completeGraph (Fintype.equivFin β)) Iso.refl]
  exact ⟨fun ⟨f⟩ ↦ ⟨f.toCopy⟩, fun ⟨f⟩ ↦ ⟨f.topEmbedding⟩⟩

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