surjOn_image — Mathlib

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

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