V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n : ℕ
hc : Colorable G n
⊢ sInf {n | Colorable G n} ≤ n
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n : ℕ
hc : Colorable G n
⊢ chromaticNumber G ≤ n
rw [chromaticNumber]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n : ℕ
hc : Colorable G n
⊢ n ∈ {n | Colorable G n}
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n : ℕ
hc : Colorable G n
⊢ sInf {n | Colorable G n} ≤ n
apply csInf_le chromaticNumber_bddBelow
case val
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n : ℕ
hc : Colorable G n
⊢ Coloring G (Fin n)
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n : ℕ
hc : Colorable G n
⊢ n ∈ {n | Colorable G n}
constructor
no goals
case val
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
n : ℕ
hc : Colorable G n
⊢ Coloring G (Fin n)
exact Classical.choice hc