English
Let ha be a ∉ s and f a function on Finset α. Then the product over (insert a s).powerset factors as the product over s.powerset times the product over s.powerset of insert a t.
Русский
Пусть ha: a ∉ s, и функция f над Finset α. Тогда произведение по t ∈ (insert a s).powerset разбивается на произведение по t ∈ s.powerset и произведение по t ∈ s.powerset со значением f(insert a t).
LaTeX
$$$\\displaystyle \\prod_{t \\in (\\operatorname{insert}~a~s).\\mathrm{powerset}} f(t) = \\left(\\prod_{t \\in s.\\mathrm{powerset}} f(t)\\right) \\cdot \\left(\\prod_{t \\in s.\\mathrm{powerset}} f(\\operatorname{insert}~a~t)\\right)$$$
Lean4
/-- A product over all subsets of `s ∪ {x}` is obtained by multiplying the product over all subsets
of `s`, and over all subsets of `s` to which one adds `x`. -/
@[to_additive /-- A sum over all subsets of `s ∪ {x}` is obtained by summing the sum over all
subsets of `s`, and over all subsets of `s` to which one adds `x`. -/
]
theorem prod_powerset_insert [DecidableEq α] (ha : a ∉ s) (f : Finset α → β) :
∏ t ∈ (insert a s).powerset, f t = (∏ t ∈ s.powerset, f t) * ∏ t ∈ s.powerset, f (insert a t) :=
by
rw [powerset_insert, prod_union, prod_image]
· exact insert_erase_invOn.2.injOn.mono fun t ht ↦ notMem_mono (mem_powerset.1 ht) ha
· aesop (add simp [disjoint_left, insert_subset_iff])
