chromaticNumber_le_iff_colorable — Mathlib

English

The chromatic number of G is at most n if and only if G is colorable with n colors.

Русский

Хроматическое число графа G не хуже n тогда и только тогда граф можно окрасить в n цветов.

LaTeX

$$$G.chromaticNumber \\le n \\iff G.Colorable n$$$

Lean4

theorem chromaticNumber_le_iff_colorable {n : ℕ} : G.chromaticNumber ≤ n ↔ G.Colorable n :=
  by
  refine ⟨fun h ↦ ?_, Colorable.chromaticNumber_le⟩
  have : G.chromaticNumber ≠ ⊤ := (trans h (WithTop.coe_lt_top n)).ne
  rw [chromaticNumber_ne_top_iff_exists] at this
  obtain ⟨m, hm⟩ := this
  rw [hm.chromaticNumber_eq_sInf, Nat.cast_le] at h
  have := Nat.sInf_mem (⟨m, hm⟩ : {n' | G.Colorable n'}.Nonempty)
  rw [Set.mem_setOf_eq] at this
  exact this.mono h

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