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