chromaticNumber_ne_top_iff_exists

English

A graph has finite chromatic number (i.e., χ(G) ≠ ∞) if and only if there exists some n with G.Colorable n.

Русский

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

LaTeX

$$$G.chromaticNumber \\neq \\top \\iff \\exists n, G.Colorable n$$$

Lean4

theorem chromaticNumber_ne_top_iff_exists : G.chromaticNumber ≠ ⊤ ↔ ∃ n, G.Colorable n :=
  by
  rw [chromaticNumber]
  convert_to ⨅ n : {m | G.Colorable m}, (n : ℕ∞) ≠ ⊤ ↔ _
  · rw [iInf_subtype]
  rw [← lt_top_iff_ne_top, ENat.iInf_coe_lt_top]
  simp

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