English
For a finpartition of a finite set that is equipartitioned, there exists an equivalence between its parts and a finite index set such that the sizes of the parts are governed by the index modulo the number of parts.
Русский
Для конечной частой разбиения, являющегося равномерным разбиению, существует эквиваленция между частями и конечной множеством индексов, причем размеры частей задаются по индексу по модулю числа частей.
LaTeX
$$$\\forall {\\alpha : Type u} [DecidableEq \\alpha] {s : Finset \\alpha} {P : Finpartition s},\\ P.IsEquipartition \\Rightarrow\\ \\exists f : P.parts \\simeq Fin \\#P.parts, \\forall t, \\#t.1 = \\#s / \\#P.parts + 1 \\iff f\\ t < \\#s % \\#P.parts$$$
Lean4
/-- There exists an enumeration of an equipartition's parts where
larger parts map to smaller numbers and vice versa. -/
theorem exists_partsEquiv (hP : P.IsEquipartition) :
∃ f : P.parts ≃ Fin #P.parts, ∀ t, #t.1 = #s / #P.parts + 1 ↔ f t < #s % #P.parts :=
by
let el := {p ∈ P.parts | #p = #s / #P.parts + 1}.equivFin
let es := {p ∈ P.parts | #p = #s / #P.parts}.equivFin
simp_rw [mem_filter, hP.card_large_parts_eq_mod] at el
simp_rw [mem_filter, hP.card_small_parts_eq_mod] at es
let sneg : { x // x ∈ P.parts ∧ ¬#x = #s / #P.parts + 1 } ≃ { x // x ∈ P.parts ∧ #x = #s / #P.parts } :=
by
apply (Equiv.refl _).subtypeEquiv
simp only [Equiv.refl_apply, and_congr_right_iff]
exact fun _ ha ↦ by rw [hP.card_part_eq_average_iff ha, ne_eq]
replace el : { x : P.parts // #x.1 = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts) := (Equiv.Set.sep ..).symm.trans el
replace es : { x : P.parts // ¬#x.1 = #s / #P.parts + 1 } ≃ Fin (#P.parts - #s % #P.parts) :=
(Equiv.Set.sep ..).symm.trans (sneg.trans es)
let f := (Equiv.sumCompl _).symm.trans ((el.sumCongr es).trans finSumFinEquiv)
use f.trans (finCongr (Nat.add_sub_of_le P.card_mod_card_parts_le))
intro ⟨p, _⟩
simp_rw [f, Equiv.trans_apply, Equiv.sumCongr_apply, finCongr_apply, Fin.coe_cast]
by_cases hc : #p = #s / #P.parts + 1 <;> simp [hc]
