V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Nonempty V
C : Coloring ⊥ (Fin 1) := Coloring.mk (fun x => 0) (_ : ∀ {v w : V}, Adj ⊥ v w → (fun x => 0) v ≠ (fun x => 0) w)
⊢ chromaticNumber ⊥ = 1
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Nonempty V
⊢ chromaticNumber ⊥ = 1
let C : (⊥ : SimpleGraph V).Coloring (Fin 1) :=
    Coloring.mk (fun _ => 0) fun {v w} h => False.elim h
case a
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Nonempty V
C : Coloring ⊥ (Fin 1) := Coloring.mk (fun x => 0) (_ : ∀ {v w : V}, Adj ⊥ v w → (fun x => 0) v ≠ (fun x => 0) w)
⊢ chromaticNumber ⊥ ≤ 1

case a
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Nonempty V
C : Coloring ⊥ (Fin 1) := Coloring.mk (fun x => 0) (_ : ∀ {v w : V}, Adj ⊥ v w → (fun x => 0) v ≠ (fun x => 0) w)
⊢ 1 ≤ chromaticNumber ⊥
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Nonempty V
C : Coloring ⊥ (Fin 1) := Coloring.mk (fun x => 0) (_ : ∀ {v w : V}, Adj ⊥ v w → (fun x => 0) v ≠ (fun x => 0) w)
⊢ chromaticNumber ⊥ = 1
apply le_antisymm
no goals
case a
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Nonempty V
C : Coloring ⊥ (Fin 1) := Coloring.mk (fun x => 0) (_ : ∀ {v w : V}, Adj ⊥ v w → (fun x => 0) v ≠ (fun x => 0) w)
⊢ chromaticNumber ⊥ ≤ 1
exact chromaticNumber_le_card C
no goals
case a
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Nonempty V
C : Coloring ⊥ (Fin 1) := Coloring.mk (fun x => 0) (_ : ∀ {v w : V}, Adj ⊥ v w → (fun x => 0) v ≠ (fun x => 0) w)
⊢ 1 ≤ chromaticNumber ⊥
exact chromaticNumber_pos C.to_colorable