English
The product over a finite set of a piecewise expression equals the product over indices with the true branch times the product over indices with the false branch.
Русский
Произведение по конечному множеству выражения вида if p then f else g равно произведению по индексам с истинным ветвлением на f и по индексам с ложным ветвлением на g.
LaTeX
$$$\\prod_{x \\in s} (\\text{if } p(x) \\text{ then } f(x) \\text{ else } g(x)) = \\left(\\prod_{x \\in s, p(x)} f(x)\\right) \\cdot \\left(\\prod_{x \\in s, \\neg p(x)} g(x)\\right).$$$
Lean4
@[to_additive]
theorem prod_apply_ite {s : Finset ι} {p : ι → Prop} [DecidablePred p] (f g : ι → γ) (h : γ → M) :
(∏ x ∈ s, h (if p x then f x else g x)) = (∏ x ∈ s with p x, h (f x)) * ∏ x ∈ s with ¬p x, h (g x) :=
(prod_apply_dite _ _ _).trans <| congr_arg₂ _ (prod_attach _ (h ∘ f)) (prod_attach _ (h ∘ g))
