English
If a proposition p is decided, then product over a Finset of ite p ... simplifies to the ite of the product: ∏_{x∈s} (if p then f x else g x) = if p then ∏_{x∈s} f x else ∏_{x∈s} g x.
Русский
Если решение есть для p, то произведение ∏_{x∈s} (if p then f x else g x) равно if p then ∏_{x∈s} f x else ∏_{x∈s} g x.
LaTeX
$$$\\prod x \\in s, \\; \\text{if } p \\text{ then } f x \\text{ else } g x = \\text{if } p \\text{ then } \\prod x \\in s, f x \\text{ else } \\prod x \\in s, g x$$$
Lean4
@[to_additive (attr := simp)]
theorem prod_dite_irrel (p : Prop) [Decidable p] (s : Finset ι) (f : p → ι → M) (g : ¬p → ι → M) :
∏ x ∈ s, (if h : p then f h x else g h x) = if h : p then ∏ x ∈ s, f h x else ∏ x ∈ s, g h x := by
split_ifs with h <;> rfl
