English
For a finite subset s and predicate p, the product of a dite (dependent if-then-else) factorizes into a product over the true part and the false part.
Русский
Для конечного подмножества s и предиката p произведение вида dite распадается на произведение по истине и по лжи части.
LaTeX
$$$\\prod_{x \\in s} \\left( \\begin{cases} f(x, p(x)) & \\text{if } p(x) \\\\ g(x, \\neg p(x)) & \\text{otherwise} \\end{cases} \\right) = \\left(\\prod_{x : {x \\in s \\mid p(x)}} f(x, \\cdot)\\right) \\cdot \\left(\\prod_{x : {x \\in s \\mid \\neg p(x)}} g(x, \\cdot)\\right).$$$
Lean4
@[to_additive]
theorem prod_dite {s : Finset ι} {p : ι → Prop} [DecidablePred p] (f : ∀ x : ι, p x → M) (g : ∀ x : ι, ¬p x → M) :
∏ x ∈ s, (if hx : p x then f x hx else g x hx) =
(∏ x : {x ∈ s | p x}, f x.1 (by simpa using (mem_filter.mp x.2).2)) *
∏ x : {x ∈ s | ¬p x}, g x.1 (by simpa using (mem_filter.mp x.2).2) :=
by simp [prod_apply_dite _ _ fun x => x]
