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⟩⟩