English
If hl: l.sum = n and i ≠ 0, then the multiplicity of i in the partition of sums equals its multiplicity in l.
Русский
Если hl: l.sum = n и i ≠ 0, то кратность i в разбиении ofSums равна кратности i в l.
LaTeX
$$$\forall {n} {l : \mathrm{Multiset} \; \mathbb{N}} (hl : l.\mathrm{sum} = n) \forall {i : \mathbb{N}} (hi : i \ne 0),\\ (\mathrm{ofSums}(n,l,hl).\mathrm{parts}).\mathrm{count}i = l.\mathrm{count}i$$$
Lean4
/-- The number of times a positive integer `i` appears in the partition `ofSums n l hl` is the same
as the number of times it appears in the multiset `l`.
(For `i = 0`, `Partition.non_zero` combined with `Multiset.count_eq_zero_of_notMem` gives that
this is `0` instead.)
-/
theorem count_ofSums_of_ne_zero {n : ℕ} {l : Multiset ℕ} (hl : l.sum = n) {i : ℕ} (hi : i ≠ 0) :
(ofSums n l hl).parts.count i = l.count i :=
count_filter_of_pos hi
