V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Fintype V
⊢ ∀ (C' : Coloring ⊤ V), Function.Surjective ↑C'
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Fintype V
⊢ chromaticNumber ⊤ = Fintype.card V
apply chromaticNumber_eq_card_of_forall_surj (selfColoring _)
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype V
C : Coloring ⊤ V
⊢ Function.Surjective ↑C
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝ : Fintype V
⊢ ∀ (C' : Coloring ⊤ V), Function.Surjective ↑C'
intro C
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype V
C : Coloring ⊤ V
⊢ Function.Injective ↑C
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype V
C : Coloring ⊤ V
⊢ Function.Surjective ↑C
rw [← Finite.injective_iff_surjective]
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype V
C : Coloring ⊤ V
v w : V
⊢ ↑C v = ↑C w → v = w
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype V
C : Coloring ⊤ V
⊢ Function.Injective ↑C
intro v w
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype V
C : Coloring ⊤ V
v w : V
⊢ ¬v = w → ¬↑C v = ↑C w
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype V
C : Coloring ⊤ V
v w : V
⊢ ↑C v = ↑C w → v = w
contrapose
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype V
C : Coloring ⊤ V
v w : V
h : ¬v = w
⊢ ¬↑C v = ↑C w
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype V
C : Coloring ⊤ V
v w : V
⊢ ¬v = w → ¬↑C v = ↑C w
intro h
no goals
V : Type u
G : SimpleGraph V
α : Type v
C✝ : Coloring G α
inst✝ : Fintype V
C : Coloring ⊤ V
v w : V
h : ¬v = w
⊢ ¬↑C v = ↑C w
exact C.valid h