V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
V' : Type u_1
G' : SimpleGraph V'
m : ℕ
hc : Colorable G' m
h : ∀ (n : ℕ), Colorable G' n → Colorable G n
⊢ chromaticNumber G' ∈ {n | Colorable G n}
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
V' : Type u_1
G' : SimpleGraph V'
m : ℕ
hc : Colorable G' m
h : ∀ (n : ℕ), Colorable G' n → Colorable G n
⊢ chromaticNumber G ≤ chromaticNumber G'
apply csInf_le chromaticNumber_bddBelow
case a
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
V' : Type u_1
G' : SimpleGraph V'
m : ℕ
hc : Colorable G' m
h : ∀ (n : ℕ), Colorable G' n → Colorable G n
⊢ Colorable G' (chromaticNumber G')
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
V' : Type u_1
G' : SimpleGraph V'
m : ℕ
hc : Colorable G' m
h : ∀ (n : ℕ), Colorable G' n → Colorable G n
⊢ chromaticNumber G' ∈ {n | Colorable G n}
apply h
no goals
case a
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
V' : Type u_1
G' : SimpleGraph V'
m : ℕ
hc : Colorable G' m
h : ∀ (n : ℕ), Colorable G' n → Colorable G n
⊢ Colorable G' (chromaticNumber G')
apply colorable_chromaticNumber hc