chromaticNumber_sum — Mathlib

English

The chromatic number of the sum G ⊕g H equals the maximum of the chromatic numbers of G and H.

Русский

Хроматическое число суммы равно максимуму хроматических чисел G и H.

LaTeX

$$$ (G \oplus_g H).chromaticNumber = \max(G.chromaticNumber, H.chromaticNumber) $$$

Lean4

@[simp]
theorem chromaticNumber_sum : (G ⊕g H).chromaticNumber = max G.chromaticNumber H.chromaticNumber :=
  by
  refine eq_max chromaticNumber_le_sum_left chromaticNumber_le_sum_right fun {d} hG hH => ?_
  cases d with
  | top => simp
  | coe n =>
    let cG : G.Coloring (Fin n) := (chromaticNumber_le_iff_colorable.mp hG).some
    let cH : H.Coloring (Fin n) := (chromaticNumber_le_iff_colorable.mp hH).some
    exact chromaticNumber_le_iff_colorable.mpr (Nonempty.intro (cG.sum cH))

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