English
For a finite set s and a predicate p, the product of dite with a family b(x,h) equals the product over the p-filtered domain and the rest equals 1 when appropriate.
Русский
Для конечного множества s и предиката p произведение dite равно произведению по отфильтрованному по p подмножеству с учётом зависимости и по остальным частям, которые дают единицу.
LaTeX
$$$\\prod_{x \\in s} (\\text{if } p(x) \\text{ then } f(x,[p(x)]) \\text{ else } g(x,[¬p(x)])) = (\\prod_{x : {x \\in s | p x}} f(x,\\cdot)) \\cdot (\\prod_{x : {x \\in s | ¬p x}} g(x,\\cdot)).$$$
Lean4
@[to_additive]
theorem prod_ite_of_true {p : ι → Prop} [DecidablePred p] (h : ∀ x ∈ s, p x) (f g : ι → M) :
∏ x ∈ s, (if p x then f x else g x) = ∏ x ∈ s, f x :=
(prod_dite_of_true h _ _).trans (prod_attach _ _)
