exists_isNClique_cliqueNum — Mathlib

English

There exists a maximum clique in G; i.e., ∃ s : Finset α, G.IsNClique (cliqueNum(G)) s.

Русский

Существует максимальная клика в графе G; т.е. существует s : Finset α such that G.IsNClique(cliqueNum(G)) s.

LaTeX

$$$\\exists s : Finset \\alpha,\\ G.IsNClique(\\mathrm{cliqueNum}(G))\\ s.$$$

Lean4

theorem exists_isNClique_cliqueNum [Finite α] : ∃ s, G.IsNClique G.cliqueNum s :=
  by
  cases nonempty_fintype α
  exact Nat.sSup_mem ⟨0, by simp⟩ G.fintype_cliqueNum_bddAbove

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