chromaticNumber_bot — Mathlib

English

The chromatic number of the bottom graph on a nonempty vertex set is 1.

Русский

Хроматическое число нижнего графа на непустом множестве вершин равно 1.

LaTeX

$$$[Nonempty V] \\Rightarrow (\\perp : SimpleGraph V).chromaticNumber = 1$$$

Lean4

theorem chromaticNumber_bot [Nonempty V] : (⊥ : SimpleGraph V).chromaticNumber = 1 :=
  by
  have : (⊥ : SimpleGraph V).Colorable 1 := ⟨.mk 0 <| by simp⟩
  exact this.chromaticNumber_le.antisymm <| Order.one_le_iff_pos.2 <| chromaticNumber_pos this

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