chromaticNumber_le — Mathlib

English

If a graph is colorable in n colors, then its chromatic number is at most n.

Русский

Если граф можно раскрасить в n цветов, то хроматическое число не превосходит n.

LaTeX

$$$G.Colorable n \\Rightarrow G.chromaticNumber \\le n$$$

Lean4

theorem chromaticNumber_le {n : ℕ} (hc : G.Colorable n) : G.chromaticNumber ≤ n :=
  by
  rw [hc.chromaticNumber_eq_sInf]
  norm_cast
  apply csInf_le chromaticNumber_bddBelow
  exact hc

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