coe_map — Mathlib

English

For f : α ↪ β and s : Finset α, the underlying multiset of map f s equals the image under f of s's multiset.

Русский

После отображения f над Finset s, полученная мультисет-структура образа совпадает с образом мультисета s под f.

LaTeX

$$$ (\mathrm{Finset.map}\; f\; s).1 = s.1.map\; f $$$

Lean4

@[simp, norm_cast]
theorem coe_map (f : α ↪ β) (s : Finset α) : (s.map f : Set β) = f '' s := by grind

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