English
If f1 and f2 are finsupps with disjoint supports, then for any g : α → M → β the product over α of g(a, f1(a) + f2(a)) factors as the product over a in the support of f1 of g(a, f1(a)) times the product over a in the support of f2 of g(a, f2(a)).
Русский
Пусть f1 и f2 — конечноподдерживаемые функции на α с непересекающимися опорами; тогда произведение по a: g(a, f1(a) + f2(a)) распадается на произведение по опоре f1 и по опоре f2.
LaTeX
$$$(f_1 + f_2).prod g = f_1.prod g \cdot f_2.prod g$ при $\operatorname{Disjoint}(f_1\!\!\!\!\!\!\operatorname{support}, f_2\!\!\!\!\!\!\operatorname{support}).$$$
Lean4
/-- For disjoint `f1` and `f2`, and function `g`, the product of the products of `g`
over `f1` and `f2` equals the product of `g` over `f1 + f2` -/
@[to_additive /-- For disjoint `f1` and `f2`, and function `g`, the sum of the sums of `g`
over `f1` and `f2` equals the sum of `g` over `f1 + f2` -/
]
theorem prod_add_index_of_disjoint [AddCommMonoid M] {f1 f2 : α →₀ M} (hd : Disjoint f1.support f2.support) {β : Type*}
[CommMonoid β] (g : α → M → β) : (f1 + f2).prod g = f1.prod g * f2.prod g :=
by
have : ∀ {f1 f2 : α →₀ M}, Disjoint f1.support f2.support → (∏ x ∈ f1.support, g x (f1 x + f2 x)) = f1.prod g :=
fun hd => Finset.prod_congr rfl fun x hx => by simp only [notMem_support_iff.mp (disjoint_left.mp hd hx), add_zero]
classical
simp_rw [← this hd, ← this hd.symm, add_comm (f2 _), Finsupp.prod, support_add_eq hd, prod_union hd, add_apply]
