chromaticNumber_eq_biInf — Mathlib

English

The chromatic number equals the infimum (biInf) of all n for which the graph is colorable with n colors.

Русский

Хроматическое число равно инфимума биInf всех n, для которых граф можно раскрасить не более чем n цветами.

LaTeX

$$$G.chromaticNumber = \\inf_{n} \\{ n : G.Colorable n \\}$ in ENat$$

Lean4

theorem chromaticNumber_eq_biInf {G : SimpleGraph V} : G.chromaticNumber = ⨅ n ∈ setOf G.Colorable, (n : ℕ∞) :=
  rfl

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