English
Let f : α →₀ M be a finitely supported function into an additive commutative monoid M with zero, m : β → γ a map, and h : α → M → Multiset β a family of multisets indexed by α and by the value f(a). Then mapping m over the total multiset given by the finsupp sum f.sum h equals the finsupp sum of the mapped multisets: Multiset.map m (f.sum h) = f.sum (λ a b, (h a b).map m).
Русский
Пусть f : α →₀ M — конечноподдерживаемая функция в аддитивном коммутативном моноидe M (с нулём), m : β → γ — отображение, и h : α → M → Multiset β — семья мультимножест в индексами по α и по значению f(a). Тогда отображение m над суммой по f распр. суммам по элементам: Multiset.map m (f.sum h) = f.sum (λ a b, (h a b).map m).
LaTeX
$$$\operatorname{Multiset.map}\\, m\\, (f.sum h) = f.sum (\\lambda a b, (h a b).\\operatorname{map} m).$$$
Lean4
theorem multiset_map_sum [Zero M] {f : α →₀ M} {m : β → γ} {h : α → M → Multiset β} :
Multiset.map m (f.sum h) = f.sum fun a b => (h a b).map m :=
map_sum (Multiset.mapAddMonoidHom m) _ f.support
