chromaticNumber_cycleGraph_of_even

English

If n is even, then the cycle graph C_n has chromatic number 2.

Русский

Если n четное, то цикл граф C_n имеет хроматическое число 2.

LaTeX

$$(cycleGraph n).chromaticNumber = 2$$

Lean4

theorem chromaticNumber_cycleGraph_of_even (n : ℕ) (h : 2 ≤ n) (hEven : Even n) : (cycleGraph n).chromaticNumber = 2 :=
  by
  have hc := (cycleGraph.bicoloring_of_even n hEven).colorable
  apply le_antisymm
  · apply hc.chromaticNumber_le
  · have hadj : (cycleGraph n).Adj ⟨0, Nat.zero_lt_of_lt h⟩ ⟨1, h⟩ := by simp [cycleGraph_adj', Fin.sub_val_of_le]
    exact two_le_chromaticNumber_of_adj hadj

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