α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hs : s ≠ ∅
⊢ Set.EquitableOn {s} Finset.card
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hs : s ≠ ∅
⊢ IsEquipartition (indiscrete hs)
rw [IsEquipartition, indiscrete_parts, coe_singleton]
no goals
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hs : s ≠ ∅
⊢ Set.EquitableOn {s} Finset.card
exact Set.equitableOn_singleton s _