English
Let s and t be finite index sets (Finsets) and let f: ι → M and g: κ → M be functions into a commutative monoid M. Then the product over the disjoint sum s ⊎ t of the function that on the s-part uses f and on the t-part uses g equals the product over s of f times the product over t of g:
Русский
Пусть s и t — конечные множества индексов, и пусть f: ι → M, g: κ → M с M коммутативный моноид. Тогда произведение по дизъюнктному объединению s и t функции Sum.elim(f,g) равно произведению по s от f и по t от g:
LaTeX
$$$\displaystyle \prod x \in s.disjSum t, \operatorname{Sum.elim}(f,g)(x) = \left(\prod x \in s, f(x)\right) \cdot \left(\prod x \in t, g(x)\right)$$$
Lean4
@[to_additive]
theorem prod_sumElim (s : Finset ι) (t : Finset κ) (f : ι → M) (g : κ → M) :
∏ x ∈ s.disjSum t, Sum.elim f g x = (∏ x ∈ s, f x) * ∏ x ∈ t, g x := by simp
