English
Let h: α → β be a function. Then for every multiset m of α, the finite set obtained by applying h to m and removing duplicates is equal to the finite set obtained by first removing duplicates from m and then applying h to each element.
Русский
Пусть h: α → β. Тогда для любого мультсетa m над α множество, получаемое применением h к элементам m с удалением дубликатов, совпадает с множеством, полученным сначала удалением дубликатов из m, а затем применением h к каждому элементу.
LaTeX
$$$ \operatorname{toFinset}(\mathrm{Multiset.map}\, h\, m) = \mathrm{Finset.image}(h, \operatorname{toFinset}(m))$$$
Lean4
@[simp]
theorem map_comp_coe (h : α → β) : Functor.map h ∘ Multiset.toFinset = Multiset.toFinset ∘ Functor.map h :=
funext fun _ => image_toFinset
