case mp
V : Type u
G : SimpleGraph V
n : ℕ
⊢ Partitionable G n → Colorable G n

case mpr
V : Type u
G : SimpleGraph V
n : ℕ
⊢ Colorable G n → Partitionable G n
V : Type u
G : SimpleGraph V
n : ℕ
⊢ Partitionable G n ↔ Colorable G n
constructor
case mp.intro.intro
V : Type u
G : SimpleGraph V
n : ℕ
P : Partition G
hf : Set.Finite P.parts
hc : Finset.card (Set.Finite.toFinset hf) ≤ n
⊢ Colorable G n
case mp
V : Type u
G : SimpleGraph V
n : ℕ
⊢ Partitionable G n → Colorable G n
rintro ⟨P, hf, hc⟩
case mp.intro.intro
V : Type u
G : SimpleGraph V
n : ℕ
P : Partition G
hf : Set.Finite P.parts
hc : Finset.card (Set.Finite.toFinset hf) ≤ n
this : Fintype ↑P.parts
⊢ Colorable G n
case mp.intro.intro
V : Type u
G : SimpleGraph V
n : ℕ
P : Partition G
hf : Set.Finite P.parts
hc : Finset.card (Set.Finite.toFinset hf) ≤ n
⊢ Colorable G n
have : Fintype P.parts := hf.fintype
case mp.intro.intro
V : Type u
G : SimpleGraph V
n : ℕ
P : Partition G
hf : Set.Finite P.parts
this : Fintype ↑P.parts
hc : Fintype.card ↑P.parts ≤ n
⊢ Colorable G n
case mp.intro.intro
V : Type u
G : SimpleGraph V
n : ℕ
P : Partition G
hf : Set.Finite P.parts
hc : Finset.card (Set.Finite.toFinset hf) ≤ n
this : Fintype ↑P.parts
⊢ Colorable G n
rw [Set.Finite.card_toFinset hf] at hc
no goals
case mp.intro.intro
V : Type u
G : SimpleGraph V
n : ℕ
P : Partition G
hf : Set.Finite P.parts
this : Fintype ↑P.parts
hc : Fintype.card ↑P.parts ≤ n
⊢ Colorable G n
apply P.to_colorable.mono hc
case mpr.intro
V : Type u
G : SimpleGraph V
n : ℕ
C : Coloring G (Fin n)
⊢ Partitionable G n
case mpr
V : Type u
G : SimpleGraph V
n : ℕ
⊢ Colorable G n → Partitionable G n
rintro ⟨C⟩
case mpr.intro
V : Type u
G : SimpleGraph V
n : ℕ
C : Coloring G (Fin n)
⊢ Finset.card (Set.Finite.toFinset (_ : Set.Finite (Coloring.colorClasses C))) ≤ Fintype.card (Fin n)
case mpr.intro
V : Type u
G : SimpleGraph V
n : ℕ
C : Coloring G (Fin n)
⊢ Partitionable G n
refine' ⟨C.toPartition, C.colorClasses_finite, le_trans _ (Fintype.card_fin n).le⟩
case mpr.intro
V : Type u
G : SimpleGraph V
n : ℕ
C : Coloring G (Fin n)
h : Set.Finite (Coloring.colorClasses C)
⊢ Finset.card (Set.Finite.toFinset h) ≤ Fintype.card (Fin n)
case mpr.intro
V : Type u
G : SimpleGraph V
n : ℕ
C : Coloring G (Fin n)
⊢ Finset.card (Set.Finite.toFinset (_ : Set.Finite (Coloring.colorClasses C))) ≤ Fintype.card (Fin n)
generalize_proofs h
case mpr.intro
V : Type u
G : SimpleGraph V
n : ℕ
C : Coloring G (Fin n)
h : Set.Finite (Coloring.colorClasses C)
this : Fintype ↑(Coloring.colorClasses C)
⊢ Finset.card (Set.Finite.toFinset h) ≤ Fintype.card (Fin n)
case mpr.intro
V : Type u
G : SimpleGraph V
n : ℕ
C : Coloring G (Fin n)
h : Set.Finite (Coloring.colorClasses C)
⊢ Finset.card (Set.Finite.toFinset h) ≤ Fintype.card (Fin n)
haveI : Fintype C.colorClasses := C.colorClasses_finite.fintype
case mpr.intro
V : Type u
G : SimpleGraph V
n : ℕ
C : Coloring G (Fin n)
h : Set.Finite (Coloring.colorClasses C)
this : Fintype ↑(Coloring.colorClasses C)
⊢ Fintype.card ↑(Coloring.colorClasses C) ≤ Fintype.card (Fin n)
case mpr.intro
V : Type u
G : SimpleGraph V
n : ℕ
C : Coloring G (Fin n)
h : Set.Finite (Coloring.colorClasses C)
this : Fintype ↑(Coloring.colorClasses C)
⊢ Finset.card (Set.Finite.toFinset h) ≤ Fintype.card (Fin n)
rw [h.card_toFinset]
no goals
case mpr.intro
V : Type u
G : SimpleGraph V
n : ℕ
C : Coloring G (Fin n)
h : Set.Finite (Coloring.colorClasses C)
this : Fintype ↑(Coloring.colorClasses C)
⊢ Fintype.card ↑(Coloring.colorClasses C) ≤ Fintype.card (Fin n)
exact C.card_colorClasses_le