English
The product over powerset s of f equals the iterated product over k from 0 to |s| of the products over powersetCard k s.
Русский
Произведение по powerset s от f равно по порядку произведению по k=0..|s| от произведений из powersetCard k s.
LaTeX
$$$\\displaystyle \\prod_{t \\in \\mathrm{powerset}(s)} f(t) = \\prod_{k \\in \\mathrm{range}(|s|+1)} \\left(\\prod_{t \\in \\mathrm{powersetCard}(k,s)} f(t)\\right)$$$
Lean4
/-- A product over `powerset s` is equal to the double product over sets of subsets of `s` with
`#s = k`, for `k = 0, ..., #s`. -/
@[to_additive /-- A sum over `powerset s` is equal to the double sum over sets of subsets of `s`
with `#s = k`, for `k = 0, ..., #s` -/
]
theorem prod_powerset (s : Finset α) (f : Finset α → β) :
∏ t ∈ powerset s, f t = ∏ j ∈ range (#s + 1), ∏ t ∈ powersetCard j s, f t := by
rw [powerset_card_disjiUnion, prod_disjiUnion]
