chromaticNumber_eq_iInf — Mathlib

English

The chromatic number equals the iInf (infimum over a subtype) of colorable numbers.

Русский

Хроматическое число равно iInf по множеству цветоспособных n, записанных как субтип.

LaTeX

$$$G.chromaticNumber = \\iInf n : {m : \\mathbb{N} \\mid G.Colorable m}, (n : \\mathbb{N}_\\infty)$$$

Lean4

theorem chromaticNumber_eq_iInf {G : SimpleGraph V} : G.chromaticNumber = ⨅ n : {m | G.Colorable m}, (n : ℕ∞) := by
  rw [chromaticNumber, iInf_subtype]

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