English
Let (α, ⊗) be a commutative and associative binary operation. For any β→α and γ→α, and for any multiset s of β, and any u1,u2 in α, the fold of the pointwise product f(x)⊗g(x) over s, starting from u1⊗u2, equals the product of the folds of f and g separately starting from u1 and u2 respectively:\n( fold_op (u1⊗u2) (map (x↦ f(x)⊗ g(x)) s) ) = ( fold_op u1 (map f s) ) ⊗ ( fold_op u2 (map g s) ).
Русский
Пусть α - множество с коммутативной и ассоциативной бинарной операцией ⊗. Для любых функций f: β→α и g: β→α, для любой мультисет s⊆β и любых u1,u2∈α выполняется равенство:\nfold_{⊗}(u1⊗u2) над map(x↦ f(x)⊗g(x)) s = fold_{⊗}(u1) над map f s ⊗ fold_{⊗}(u2) над map g s.
LaTeX
$$$\\operatorname{fold}_{\\otimes}(u_1 \\otimes u_2)\\big(\\operatorname{map}(x \\mapsto f(x) \\otimes g(x))\\ s\\big) = \\operatorname{fold}_{\\otimes} (u_1)\\big(\\operatorname{map} f\\ s\\big) \\otimes \\operatorname{fold}_{\\otimes} (u_2)\\big(\\operatorname{map} g\\ s\\big)$$$
Lean4
theorem fold_distrib {f g : β → α} (u₁ u₂ : α) (s : Multiset β) :
(s.map fun x => f x * g x).fold op (u₁ * u₂) = (s.map f).fold op u₁ * (s.map g).fold op u₂ :=
Multiset.induction_on s (by simp)
(fun a b h => by
rw [map_cons, fold_cons_left, h, map_cons, fold_cons_left, map_cons, fold_cons_right, ha.assoc, ← ha.assoc (g a),
hc.comm (g a), ha.assoc, hc.comm (g a), ha.assoc])
