maximumClique_card_eq_cliqueNum — Mathlib

English

If s is a maximum clique, then |s| = cliqueNum(G).

Русский

Если s является максимальной кликой, то её размер равен cliqueNum(G).

LaTeX

$$$|s| = \\mathrm{cliqueNum}(G).$$$

Lean4

theorem maximumClique_card_eq_cliqueNum [Fintype α] (s : Finset α) (sm : G.IsMaximumClique s) : #s = G.cliqueNum :=
  by
  obtain ⟨sc, sm⟩ := sm
  obtain ⟨t, tc, tcard⟩ := G.exists_isNClique_cliqueNum
  exact eq_of_le_of_not_lt sc.card_le_cliqueNum (by simp [← tcard, sm t tc])

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