V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : IsEmpty V
⊢ chromaticNumber G ≤ 0
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : IsEmpty V
⊢ chromaticNumber G = 0
rw [← nonpos_iff_eq_zero]
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : IsEmpty V
⊢ 0 ∈ {n | Colorable G n}
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : IsEmpty V
⊢ chromaticNumber G ≤ 0
apply csInf_le chromaticNumber_bddBelow
no goals
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : IsEmpty V
⊢ 0 ∈ {n | Colorable G n}
apply colorable_of_isEmpty