English
For a finite s and a ∉ s, the finprod over 𝒫(insert a s) factors as the product over 𝒫 s of f times the product over 𝒫 s of f( insert a t ).
Русский
Для конечного s и a не принадлежащего s, финпроизведение по 𝒫(добавление a к s) раскладывается как произведение по 𝒫 s от f и по 𝒫 s от f(insert a t).
LaTeX
$$$\\prod^\\!t \\in \\mathcal{P}(\\mathrm{insert}\\ a\ s), f(t) = \\left(\\prod^\\!t \\in \\mathcal{P}(s), f(t)\\right) \\cdot \\left(\\prod^\\!t \\in \\mathcal{P}(s), f(\\mathrm{insert}\\ a\, t)\\right)$$$
Lean4
@[to_additive]
theorem finprod_mem_powerset_insert {f : Set α → M} {s : Set α} {a : α} (hs : s.Finite) (has : a ∉ s) :
∏ᶠ t ∈ 𝒫 insert a s, f t = (∏ᶠ t ∈ 𝒫 s, f t) * ∏ᶠ t ∈ 𝒫 s, f (insert a t) := by
rw [Set.powerset_insert, finprod_mem_union (disjoint_powerset_insert has) hs.powerset (hs.powerset.image (insert a)),
finprod_mem_image (powerset_insert_injOn has)]
