English
If there is a homomorphism m: β → γ compatible with op and op', then folding with op' is mapped by m to folding with op.
Русский
Если есть гомоморфизм m: β → γ, сохраняющий операторы, то свёртка op' соответствует свёртке op через m.
LaTeX
$$$\\mathrm{fold}_{op'}\\ (m\\ b)\\ (\\lambda x. m(f x)) = m(\\mathrm{fold}_{op}\\ b f)$$$
Lean4
theorem fold_hom {op' : γ → γ → γ} [Std.Commutative op'] [Std.Associative op'] {m : β → γ}
(hm : ∀ x y, m (op x y) = op' (m x) (m y)) : (s.fold op' (m b) fun x => m (f x)) = m (s.fold op b f) :=
by
rw [fold, fold, ← Multiset.fold_hom op hm, Multiset.map_map]
simp only [Function.comp_apply]
