English
For finite s and a ∈ s, the finprod over 𝒫 s equals the finprod over 𝒫(s\\{a}) times finprod over 𝒫(s\\{a}) of f(insert a t).
Русский
Для конечного s и a ∈ s имеем разложение по 𝒫 s и 𝒫 (s\\{a}) совместно с insert a.
LaTeX
$$$\\prod^\\!t ∈ 𝒫 s, f(t) = \\left(\\prod^\\!t ∈ 𝒫(s \\ {a}), f(t)\\right) \\cdot \\left(\\prod^\\!t ∈ 𝒫(s \\ {a}), f(\\mathrm{insert}\ a\ t)\\right)$$$
Lean4
@[to_additive]
theorem finprod_mem_powerset_diff_elem {f : Set α → M} {s : Set α} {a : α} (hs : s.Finite) (has : a ∈ s) :
∏ᶠ t ∈ 𝒫 s, f t = (∏ᶠ t ∈ 𝒫(s \ { a }), f t) * ∏ᶠ t ∈ 𝒫(s \ { a }), f (insert a t) :=
by
nth_rw 1 2 [← Set.insert_diff_self_of_mem has] -- second appearance hidden by notation
exact finprod_mem_powerset_insert (hs.subset Set.diff_subset) (notMem_diff_of_mem (Set.mem_singleton a))
