card_le_cliqueNum — Mathlib

English

For any finite graph G and any clique t in G, the size of t is at most the clique number: |t| ≤ cliqueNum(G).

Русский

Для конечного графа G и любой клики t выполняется неравенство |t| ≤ кликовое число G.

LaTeX

$$$\\forall t : Finset \\alpha,\\ G.IsClique t \\rightarrow \\#t \\le \\mathrm{cliqueNum}(G).$$$

Lean4

theorem card_le_cliqueNum [Finite α] {t : Finset α} {tc : G.IsClique t} : #t ≤ G.cliqueNum :=
  by
  cases nonempty_fintype α
  exact le_csSup G.fintype_cliqueNum_bddAbove (Exists.intro t ⟨tc, rfl⟩)

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