V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(colorClasses C)
⊢ Fintype.card ↑(Setoid.classes (Setoid.ker ↑C)) ≤ Fintype.card α
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(colorClasses C)
⊢ Fintype.card ↑(colorClasses C) ≤ Fintype.card α
simp [colorClasses]
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(colorClasses C)
this : Fintype ↑(Setoid.classes (Setoid.ker ↑C))
⊢ Fintype.card ↑(Setoid.classes (Setoid.ker ↑C)) ≤ Fintype.card α
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(colorClasses C)
⊢ Fintype.card ↑(Setoid.classes (Setoid.ker ↑C)) ≤ Fintype.card α
haveI : Fintype (Setoid.classes (Setoid.ker C)) := by assumption
no goals
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(colorClasses C)
this : Fintype ↑(Setoid.classes (Setoid.ker ↑C))
⊢ Fintype.card ↑(Setoid.classes (Setoid.ker ↑C)) ≤ Fintype.card α
convert Setoid.card_classes_ker_le C
no goals
V : Type u
G : SimpleGraph V
α : Type v
C : Coloring G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(colorClasses C)
⊢ Fintype ↑(Setoid.classes (Setoid.ker ↑C))
assumption