English
If f is an embedding α ↪ β and s is a Finset α, then the image Finset in β is obtained by applying f to all elements of s and carrying over the no-duplicates property.
Русский
Если f — вложение α в β и s — Finset α, то образ s под действием f — Finset β, получаемый применением f ко всем элементам s и сохраняющий отсутствие дубликатов.
LaTeX
$$$ \mathrm{map}(f,s) \text{ is a Finset } β \text{ with } (\mathrm{map}(f,s)).1 = s.1.map f$$$
Lean4
/-- When `f` is an embedding of `α` in `β` and `s` is a finset in `α`, then `s.map f` is the image
finset in `β`. The embedding condition guarantees that there are no duplicates in the image. -/
def map (f : α ↪ β) (s : Finset α) : Finset β :=
⟨s.1.map f, s.2.map f.2⟩
