V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Subsingleton V
⊢ sInf {n | Colorable G n} ≤ 1
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Subsingleton V
⊢ chromaticNumber G ≤ 1
rw [chromaticNumber]
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Subsingleton V
⊢ 1 ∈ {n | Colorable G n}
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Subsingleton V
⊢ sInf {n | Colorable G n} ≤ 1
apply csInf_le chromaticNumber_bddBelow
case val
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Subsingleton V
⊢ Coloring G (Fin 1)
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Subsingleton V
⊢ 1 ∈ {n | Colorable G n}
constructor
case val
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Subsingleton V
⊢ ∀ {v w : V}, Adj G v w → (fun x => 0) v ≠ (fun x => 0) w
case val
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Subsingleton V
⊢ Coloring G (Fin 1)
refine' Coloring.mk (fun _ => 0) _
case val
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Subsingleton V
v w : V
⊢ Adj G v w → (fun x => 0) v ≠ (fun x => 0) w
case val
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Subsingleton V
⊢ ∀ {v w : V}, Adj G v w → (fun x => 0) v ≠ (fun x => 0) w
intro v w
case val
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Subsingleton V
v w : V
⊢ Adj G w w → (fun x => 0) w ≠ (fun x => 0) w
case val
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Subsingleton V
v w : V
⊢ Adj G v w → (fun x => 0) v ≠ (fun x => 0) w
rw [Subsingleton.elim v w]
no goals
case val
V : Type u
G✝ : SimpleGraph V
α : Type v
C : Coloring G✝ α
G : SimpleGraph V
inst✝ : Subsingleton V
v w : V
⊢ Adj G w w → (fun x => 0) w ≠ (fun x => 0) w
simp