bicoloring_of_even — Mathlib

English

A cycle graph with even length has a bicoloring (2-coloring).

Русский

Циклический граф с четной длиной имеет двукрасность (2-окраску).

LaTeX

$$def bicoloring_of_even (n) (h) : Coloring (cycleGraph n) Bool$$

Lean4

/-- Bicoloring of a cycle graph of even size -/
def bicoloring_of_even (n : ℕ) (h : Even n) : Coloring (cycleGraph n) Bool :=
  Coloring.mk (fun u ↦ u.val % 2 = 0) <| by
    intro u v hadj
    match n with
    | 0 => exact u.elim0
    | 1 => simp at h
    | n + 2 =>
      simp only [ne_eq, decide_eq_decide]
      simp only [cycleGraph_adj] at hadj
      cases hadj with
      | inl huv
      | inr
        huv =>
        rw [← add_eq_of_eq_sub' huv.symm, ← Fin.even_iff_mod_of_even h, ← Fin.even_iff_mod_of_even h,
          Fin.even_add_one_iff_odd]
        apply Classical.not_iff.mpr
        simp [Fin.not_odd_iff_even_of_even h, Fin.not_even_iff_odd_of_even h]

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