English
Let s be a multiset of i, t(i) a multiset of α for each i, and b(i) ∈ α with b0 ∈ α. Then folding op over the bound structure equals folding over the transformed factors: fold op (fold op b0 (map b s)) (bind s t) = fold op b0 (map (i ↦ fold op (b i) (t i)) s).
Русский
Пусть s — мульти-множество индексов i, для каждого i имеется мультисет α = t(i), и задана функция b(i). Тогда свёртка по связыванию равна свёртке по преобразованным частям: fold op (fold op b0 (map b s)) (bind s t) = fold op b0 (map (i ↦ fold op (b i) (t i)) s).
LaTeX
$$$\mathrm{(s.bind\; t).fold\; op}\; ( (s.map\; b).fold\; op\; b_0 ) = \; (s.map\; (\lambda i. (t\,i).fold\; op\; (b\,i))).fold\; op\; b_0$$$
Lean4
theorem fold_bind {ι : Type*} (s : Multiset ι) (t : ι → Multiset α) (b : ι → α) (b₀ : α) :
(s.bind t).fold op ((s.map b).fold op b₀) = (s.map fun i => (t i).fold op (b i)).fold op b₀ := by
induction s using Multiset.induction_on with
| empty => rw [zero_bind, map_zero, map_zero, fold_zero]
| cons a ha ih => rw [cons_bind, map_cons, map_cons, fold_cons_left, fold_cons_left, fold_add, ih]
