English
Let f be a finsupp on α and g : α → β be a function. Then mapping g on the multiset corresponding to f equals the multiset corresponding to the finsupp mapDomain g f, i.e. f.toMultiset.map g = toMultiset (f.mapDomain g).
Русский
Пусть f — функция finsupp на α, и дано отображение g: α → β. Тогда отображение по g мультимножества, соответствующего f, равно мультимножеству, соответствующему f.mapDomain g: f.toMultiset.map g = toMultiset (f.mapDomain g).
LaTeX
$$$f.\mathrm{toMultiset}.map\; g = \mathrm{toMultiset}(f.mapDomain\ g)$$$
Lean4
theorem toMultiset_map (f : α →₀ ℕ) (g : α → β) : f.toMultiset.map g = toMultiset (f.mapDomain g) :=
by
refine f.induction ?_ ?_
· rw [toMultiset_zero, Multiset.map_zero, mapDomain_zero, toMultiset_zero]
· intro a n f _ _ ih
rw [toMultiset_add, Multiset.map_add, ih, mapDomain_add, mapDomain_single, toMultiset_single, toMultiset_add,
toMultiset_single, ← Multiset.coe_mapAddMonoidHom, (Multiset.mapAddMonoidHom g).map_nsmul]
rfl
