chromaticNumber_top_eq_top_of_infinite

English

If V is infinite, then the chromatic number of the complete graph on V is infinite.

Русский

Если множество вершин бесконечно, то хроматическое число полного графа на этом множестве бесконечно.

LaTeX

$$$\chi(\top_V) = \infty$$$

Lean4

theorem chromaticNumber_top_eq_top_of_infinite (V : Type*) [Infinite V] : (⊤ : SimpleGraph V).chromaticNumber = ⊤ :=
  by
  by_contra hc
  rw [← Ne, chromaticNumber_ne_top_iff_exists] at hc
  obtain ⟨n, ⟨hn⟩⟩ := hc
  exact not_injective_infinite_finite _ hn.injective_of_top_hom

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