toFinset_map — Mathlib

English

Mapping a multiset through a function and then converting to a Finset yields the same as taking the Finset image of the deduplicated multiset.

Русский

Отображение мульти-сета через функцию и преобразование в Finset эквивалентны изображению финсета отуменённого мультисета.

LaTeX

$$$\\mathrm{(m.map\, f).toFinset = m.toFinset.image\, f}$$$

Lean4

theorem toFinset_map [DecidableEq α] [DecidableEq β] (f : α → β) (m : Multiset α) :
    (m.map f).toFinset = m.toFinset.image f :=
  Finset.val_inj.1 (Multiset.dedup_map_dedup_eq _ _).symm

Похожие утверждения