English
For any function h: α → β and any multiset s of α, the Finset obtained by applying h to the elements of s and then taking the Finset is equal to the Finset obtained by first converting s to a Finset and then applying h to each element.
Русский
Пусть h: α → β и мультсет s над α. Множество Finset, получаемое применением h к элементам s и затем взятием Finset, совпадает с Finset, полученным сначала преобразованием s в Finset, а затем применением h к каждому элементу.
LaTeX
$$$ \operatorname{toFinset}(\mathrm{Multiset.map}\, h\, s) = \mathrm{Finset.image}(h, \operatorname{toFinset}(s))$$$
Lean4
@[simp]
theorem map_comp_coe_apply (h : α → β) (s : Multiset α) : s.toFinset.image h = (h <$> s).toFinset :=
congrFun (map_comp_coe h) s
