English
For a finite set s, a predicate p on indices, and functions f, g, h, the product over s of h applied to a piecewise choice equals the product over the subset where p holds and the subset where ¬p holds after applying the corresponding pieces.
Русский
Для множества s, предиката p и функций f, g, h произведение по s функции h над разбиением по p равно произведению по подмножеству, где p истинно, и по подмножеству, где p ложно.
LaTeX
$$$\\prod_{x \\in s} h\\bigl(\\text{if } p(x) \\text{ then } f(x) \\text{ else } g(x)\\bigr) = \\left(\\prod_{x \\in \\{x \\in s \\mid p(x)\\}} h\\bigl(f(x)\\bigr)\\right) \\cdot \\left(\\prod_{x \\in \\{x \\in s \\mid \\neg p(x)\\}} h\\bigl(g(x)\\bigr)\\right).$$$
Lean4
@[to_additive]
theorem prod_apply_dite {p : ι → Prop} [DecidablePred p] [DecidablePred fun x => ¬p x] (f : ∀ x : ι, p x → γ)
(g : ∀ x : ι, ¬p x → γ) (h : γ → M) :
(∏ x ∈ s, h (if hx : p x then f x hx else g x hx)) =
(∏ x : {x ∈ s | p x}, h (f x.1 <| by simpa using (mem_filter.mp x.2).2)) *
∏ x : {x ∈ s | ¬p x}, h (g x.1 <| by simpa using (mem_filter.mp x.2).2) :=
calc
(∏ x ∈ s, h (if hx : p x then f x hx else g x hx)) =
(∏ x ∈ s with p x, h (if hx : p x then f x hx else g x hx)) *
∏ x ∈ s with ¬p x, h (if hx : p x then f x hx else g x hx) :=
(prod_filter_mul_prod_filter_not s p _).symm
_ =
(∏ x : {x ∈ s | p x}, h (if hx : p x.1 then f x.1 hx else g x.1 hx)) *
∏ x : {x ∈ s | ¬p x}, h (if hx : p x.1 then f x.1 hx else g x.1 hx) :=
(congr_arg₂ _ (prod_attach _ _).symm (prod_attach _ _).symm)
_ =
(∏ x : {x ∈ s | p x}, h (f x.1 <| by simpa using (mem_filter.mp x.2).2)) *
∏ x : {x ∈ s | ¬p x}, h (g x.1 <| by simpa using (mem_filter.mp x.2).2) :=
congr_arg₂ _ (prod_congr rfl fun x _hx ↦ congr_arg h (dif_pos <| by simpa using (mem_filter.mp x.2).2))
(prod_congr rfl fun x _hx => congr_arg h (dif_neg <| by simpa using (mem_filter.mp x.2).2))
