English
Let f: α → β and S ⊆ α. Then f maps S onto its image f[S]; equivalently, every element of f[S] is of the form f(x) for some x ∈ S.
Русский
Пусть f: α → β и S ⊆ α. Тогда отображение f на S покрывает образ f[S]; то есть каждый элемент y ∈ f[S] имеет вид f(x) для некоторого x ∈ S.
LaTeX
$$$$ \\forall y\, (y \\in f[S] \\rightarrow \\exists x \\in S,\\ f(x)=y) $$$$
Lean4
theorem surjOn_image (f : α → β) (s : Set α) : SurjOn f s (f '' s) :=
Subset.rfl