colorable_chromaticNumber_of_fintype

English

For a finite vertex set, the chromatic number toNat equals a colorable coloring: the graph is colorable with ENat.toNat(G.chromaticNumber).

Русский

При конечном множестве вершин число цветов равно toNat хроматического числа графа и граф можно раскрасить соответствующим числом цветов.

LaTeX

$$$G.Colorable (ENat.toNat G.chromaticNumber)$$$

Lean4

theorem colorable_chromaticNumber_of_fintype (G : SimpleGraph V) [Finite V] :
    G.Colorable (ENat.toNat G.chromaticNumber) :=
  by
  cases nonempty_fintype V
  exact colorable_chromaticNumber G.colorable_of_fintype

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