colorable_chromaticNumber — Mathlib

English

If a graph is colorable with m colors, then it is colorable with the Nat-valued chromatic number: G.Colorable m implies G.Colorable (ENat.toNat G.chromaticNumber).

Русский

Если граф можно окрасить в m цветов, то он можно окрасить и численно равным натуальному числу хроматического числа графа: G.Colorable m ⇒ G.Colorable (ENat.toNat G.chromaticNumber).

LaTeX

$$$G.Colorable m \\Rightarrow G.Colorable (ENat.toNat\$G.chromaticNumber\$)$$$

Lean4

theorem colorable_chromaticNumber {m : ℕ} (hc : G.Colorable m) : G.Colorable (ENat.toNat G.chromaticNumber) := by
  classical
  rw [hc.chromaticNumber_eq_sInf, Nat.sInf_def]
  · apply Nat.find_spec
  · exact colorable_set_nonempty_of_colorable hc

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