English
For any a and s, the (n+1)-element submultisets of a :: s split into those not using a and those that do, with a prepended to n-element submultisets of s.
Русский
Для любого элемента a и множества s множества подмножест в размером n+1 из a :: s разлагаются на те, которые не используют a, и те, которые используют, где к каждому n-элементному подмножеству s прибавляется a.
LaTeX
$$$\mathrm{powersetCard}(n+1, a \;::_m\; s) = \mathrm{powersetCard}(n+1, s) + \mathrm{map}(\mathrm{cons}\,a)\big(\mathrm{powersetCard}(n, s)\big)$$$
Lean4
@[simp]
theorem powersetCard_cons (n : ℕ) (a : α) (s) :
powersetCard (n + 1) (a ::ₘ s) = powersetCard (n + 1) s + map (cons a) (powersetCard n s) :=
Quotient.inductionOn s fun l => by simp [powersetCard_coe']
