card_le_chromaticNumber — Mathlib

English

For any clique s in G, s.card ≤ G.chromaticNumber.

Русский

Для любой клики s графа G выполняется s.card ≤ χ(G).

LaTeX

$$$|s| \le \chi(G)$$$

Lean4

theorem card_le_chromaticNumber {s : Finset V} (h : G.IsClique s) : s.card ≤ G.chromaticNumber :=
  by
  obtain (hc | hc) := eq_or_ne G.chromaticNumber ⊤
  · rw [hc]
    exact le_top
  · have hc' := hc
    rw [chromaticNumber_ne_top_iff_exists] at hc'
    obtain ⟨n, c⟩ := hc'
    rw [← ENat.coe_toNat_eq_self] at hc
    rw [← hc, Nat.cast_le]
    exact h.card_le_of_colorable (colorable_chromaticNumber c)

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