English
Let m be a finite multiset of α and f: α → β. The image of m under f equals m.map f; i.e., applying f to every element of m yields the multiset obtained by mapping f over m.
Русский
Пусть m — конечное мультимножество над α и f: α → β. Образ m под действием f равен m.map f; то есть применение f ко всем элементам m даёт мультимножество, полученное применением f к элементам m.
LaTeX
$$$ ((\mathrm{Finset.univ} : \mathrm{Finset} m).\mathrm{val}.\mathrm{map} (\lambda x : m, f (x : \alpha))) = m.\mathrm{map} f $$$
Lean4
@[simp]
theorem map_univ {β : Type*} (m : Multiset α) (f : α → β) :
((Finset.univ : Finset m).val.map fun (x : m) ↦ f (x : α)) = m.map f :=
by
simp_rw [← Function.comp_apply (f := f)]
exact map_univ_comp_coe m f
