chromaticNumber_pos — Mathlib

English

If a nonempty vertex set is present and G is colorable in some n, then 0 < χ(G).

Русский

Если граф существует на непустом множестве вершин и его можно окрасить в n цветов, то χ(G) > 0.

LaTeX

$$$[Nonempty\\ V] \\, (\\forall n, G.Colorable n) \\Rightarrow 0 < G.chromaticNumber$$$

Lean4

theorem chromaticNumber_pos [Nonempty V] {n : ℕ} (hc : G.Colorable n) : 0 < G.chromaticNumber :=
  by
  rw [hc.chromaticNumber_eq_sInf, Nat.cast_pos]
  apply le_csInf (colorable_set_nonempty_of_colorable hc)
  intro m hm
  by_contra h'
  simp only [not_le] at h'
  obtain ⟨i, hi⟩ := hm.some (Classical.arbitrary V)
  have h₁ : i < 0 := lt_of_lt_of_le hi (Nat.le_of_lt_succ h')
  exact Nat.not_lt_zero _ h₁

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