α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hP : IsEquipartition P
ht : t ∈ P.parts
⊢ (Finset.sum P.parts fun i => Finset.card i) / Finset.card P.parts ≤ Finset.card t
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hP : IsEquipartition P
ht : t ∈ P.parts
⊢ Finset.card s / Finset.card P.parts ≤ Finset.card t
rw [← P.sum_card_parts]
no goals
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hP : IsEquipartition P
ht : t ∈ P.parts
⊢ (Finset.sum P.parts fun i => Finset.card i) / Finset.card P.parts ≤ Finset.card t
exact Finset.EquitableOn.le hP ht