English
Let α finite, p a decidable predicate on α, β a commutative monoid. For f and g as given, the product over a of (if p a then f a else g a) equals the product over the subtype {a : α // p a} of f a a.2 times the product over {a : α // ¬p a} of g a a.2.
Русский
Пусть α конечен, p — договоримо определяемый предикат на α, β — коммутативный моноид. Пусть есть функции f и g, тогда произведение по a от (если p a, то f a, иначе g a) равно произведению по подтипу {a | p a} от f a и по подтипу {a | ¬p a} от g a.
LaTeX
$$$ \\displaystyle \\prod a, \\mathrm{dite}(p\\,a)(f\\,a)(g\\,a) = \\left( \\prod a : \\{ a \\mid p a \\}, f a a.2 \\right) \\cdot \\left( \\prod a : \\{ a \\mid \\neg p a \\}, g a a.2 \\right). $$$
Lean4
nonrec theorem prod_dite [Fintype α] {p : α → Prop} [DecidablePred p] [CommMonoid β] (f : ∀ a, p a → β)
(g : ∀ a, ¬p a → β) :
(∏ a, dite (p a) (f a) (g a)) = (∏ a : { a // p a }, f a a.2) * ∏ a : { a // ¬p a }, g a a.2 :=
by
simp only [prod_dite]
congr 1
· exact (Equiv.subtypeEquivRight <| by simp).prod_comp fun x : { x // p x } => f x x.2
· exact (Equiv.subtypeEquivRight <| by simp).prod_comp fun x : { x // ¬p x } => g x x.2
