English
The powerset of a multiset S is the concatenation over all lengths k from 0 to |S| of the k-element submultisets of S.
Русский
Множество подмножеств S разбивается на части по размеру: от 0 до |S|; каждая часть содержит подмножества соответствующей длины.
LaTeX
$$$\operatorname{bind}(\operatorname{range}(\operatorname{card} S + 1), \\; \lambda k, S.\mathrm{powersetCard} k) = S.\mathrm{powerset}$$$
Lean4
theorem bind_powerset_len {α : Type*} (S : Multiset α) :
(bind (Multiset.range (card S + 1)) fun k => S.powersetCard k) = S.powerset :=
by
induction S using Quotient.inductionOn
simp_rw [quot_mk_to_coe, powerset_coe', powersetCard_coe, ← coe_range, coe_bind, ← List.map_flatMap, coe_card]
exact coe_eq_coe.mpr ((List.range_bind_sublistsLen_perm _).map _)
