map_toFinset — Mathlib

English

For any s : Multiset α, the Finset obtained by mapping f over s.toFinset equals the toFinset of the mapped multiset.

Русский

Для любого s : Multiset α Finset, полученный отображением f over s.toFinset равен toFinset отображённой мультисети.

LaTeX

$$$ s.\!toFinset.map f = (s.map f).toFinset $$$

Lean4

theorem map_toFinset [DecidableEq α] [DecidableEq β] {s : Multiset α} : s.toFinset.map f = (s.map f).toFinset :=
  ext fun _ => by simp only [mem_map, Multiset.mem_map, Multiset.mem_toFinset]

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