two_le_chromaticNumber_of_adj — Mathlib

English

If two vertices u and v are adjacent, then the chromatic number χ(G) is at least 2.

Русский

Если вершины u и v смежны, то хроматическое число χ(G) не меньше 2.

LaTeX

$$2 ≤ G.chromaticNumber$$

Lean4

theorem two_le_chromaticNumber_of_adj {α} {G : SimpleGraph α} {u v : α} (hadj : G.Adj u v) : 2 ≤ G.chromaticNumber :=
  by
  refine le_of_not_gt ?_
  intro h
  have hc : G.Colorable 1 := chromaticNumber_le_iff_colorable.mp (Order.le_of_lt_add_one h)
  let c : G.Coloring (Fin 1) := hc.some
  exact c.valid hadj (Subsingleton.elim (c u) (c v))

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