colorable_of_chromaticNumber_ne_top

English

If the chromatic number is finite, then G is colorable with the nat-valued chromatic number: G.Colorable (ENat.toNat G.chromaticNumber).

Русский

Если хроматическое число графа конечно, то граф раскрашивается nat-значением χ(G), то есть G.Colorable(ENat.toNat G.chromaticNumber).

LaTeX

$$$G.chromaticNumber \\neq \\top \\Rightarrow G.Colorable (ENat.toNat G.chromaticNumber)$$$

Lean4

theorem colorable_of_chromaticNumber_ne_top (h : G.chromaticNumber ≠ ⊤) : G.Colorable (ENat.toNat G.chromaticNumber) :=
  by
  rw [chromaticNumber_ne_top_iff_exists] at h
  obtain ⟨n, hn⟩ := h
  exact colorable_chromaticNumber hn

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