chromaticNumber_pathGraph — Mathlib

English

The path graph P_n has chromatic number 2 for all n ≥ 2.

Русский

Граф пути P_n имеет хроматическое число 2 при любом n ≥ 2.

LaTeX

$$∀ n ≥ 2, (pathGraph n).chromaticNumber = 2$$

Lean4

theorem chromaticNumber_pathGraph (n : ℕ) (h : 2 ≤ n) : (pathGraph n).chromaticNumber = 2 :=
  by
  have hc := (pathGraph.bicoloring n).colorable
  apply le_antisymm
  · exact hc.chromaticNumber_le
  · have hadj : (pathGraph n).Adj ⟨0, Nat.zero_lt_of_lt h⟩ ⟨1, h⟩ := by simp [pathGraph_adj]
    exact two_le_chromaticNumber_of_adj hadj

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