English
Let ha: a ∉ s and f: Finset α → β. Then ∏ t ∈ (s.cons a ha).powerset, f t equals product over s.powerset times product over s.powerset.attach of f(cons a t).
Русский
Пусть ha: a ∉ s и f: Finset α → β. Тогда произведение по t ∈ (s.cons a ha).powerset f t равно произведению по t ∈ s.powerset f t умноженному на произведение по t ∈ s.powerset.attach f(cons a t).
LaTeX
$$$\\displaystyle \\prod_{t \\in (s.\\text{cons } a\, ha).powerset} f(t) = \\left(\\prod_{t \\in s.\\powerset} f(t)\\right) \\cdot \\left(\\prod_{t \\in s.\\powerset.attach} f(\\text{cons } 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_cons (ha : a ∉ s) (f : Finset α → β) :
∏ t ∈ (s.cons a ha).powerset, f t =
(∏ t ∈ s.powerset, f t) * ∏ t ∈ s.powerset.attach, f (cons a t <| notMem_mono (mem_powerset.1 t.2) ha) :=
by
classical
simp_rw [cons_eq_insert]
rw [prod_powerset_insert ha, prod_attach _ fun t ↦ f (insert a t)]
