English
Let op and op' be binary operations with op commutative and associative on α and β respectively, and m: α→β a function preserving the operation, i.e., m(op x y) = op'(m x)(m y) for all x,y. Then for any b∈α and any multiset s⊆α, the fold of m over s starting at m b equals m applied to the fold of op over s starting at b:\n (s.map m).fold op' (m b) = m (s.fold op b).
Русский
Пусть op и op' — бинарные операции, обладающие коммутативностью и ассоциативностью на множествах α и β соответственно, и пусть m: α→β сохраняет операцию: m(op x y) = op'(m x)(m y). Тогда для любого b∈α и любого мультиноса s возрастает равенство свёрток: (s.map m).fold op' (m b) = m (s.fold op b).
LaTeX
$$$\\forall b\\, s:\\ Multiset\\,\\alpha,\\ (s.map m).fold\\ op'\\ (m b) = m\\big( s.fold\\ op\\ b\\big)$$$
Lean4
theorem fold_hom {op' : β → β → β} [Std.Commutative op'] [Std.Associative op'] {m : α → β}
(hm : ∀ x y, m (op x y) = op' (m x) (m y)) (b : α) (s : Multiset α) : (s.map m).fold op' (m b) = m (s.fold op b) :=
Multiset.induction_on s (by simp) (by simp +contextual [hm])
