English
For any finite s and n with n ≠ 0 and n ≤ |s|, there exists an equipartition P of s with |P.parts| = n.
Русский
Для любого конечного множества s и числа n, не равного 0, не большего чем |s|, существует равновесное разбиение P разбиения s с количеством частей |P.parts| = n.
LaTeX
$$$\\exists P:\\ Finpartition\\ s, P.IsEquipartition \\land \\#P.parts = n$ при $n \\neq 0$ и $n \\le \\lvert s\\rvert$$$
Lean4
/-- We can find equipartitions of arbitrary size. -/
theorem exists_equipartition_card_eq (hn : n ≠ 0) (hs : n ≤ #s) :
∃ P : Finpartition s, P.IsEquipartition ∧ #P.parts = n :=
by
rw [← pos_iff_ne_zero] at hn
have : (n - #s % n) * (#s / n) + #s % n * (#s / n + 1) = #s := by
rw [tsub_mul, mul_add, ← add_assoc, tsub_add_cancel_of_le (Nat.mul_le_mul_right _ (mod_lt _ hn).le), mul_one,
add_comm, mod_add_div]
refine ⟨(indiscrete (card_pos.1 <| hn.trans_le hs).ne_empty).equitabilise this, equitabilise_isEquipartition, ?_⟩
rw [card_parts_equitabilise _ _ (Nat.div_pos hs hn).ne', tsub_add_cancel_of_le (mod_lt _ hn).le]
