chromaticNumber_eq_iff_colorable_not_colorable

English

The chromatic number equals n+1 exactly when G is colorable in n+1 colors and not colorable in n colors.

Русский

Хроматическое число равно n+1 тогда и только тогда граф можно окрасить в n+1 цветов и нельзя в n цветов.

LaTeX

$$G.chromaticNumber = n+1 \\iff (G.Colorable(n+1) \\land \\neg G.Colorable n)$$

Lean4

/-- If the chromatic number of `G` is `n + 1`, then `G` is colorable in no fewer than `n + 1`
colors. -/
theorem chromaticNumber_eq_iff_colorable_not_colorable :
    G.chromaticNumber = n + 1 ↔ G.Colorable (n + 1) ∧ ¬G.Colorable n := by
  rw [eq_iff_le_not_lt, not_lt, ENat.add_one_le_iff (ENat.coe_ne_top n), ← not_le, chromaticNumber_le_iff_colorable, ←
    Nat.cast_add_one, chromaticNumber_le_iff_colorable]

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