English
The image of a set s under f: α → β is f''s = { f(a) | a ∈ s }. In words: all values attained by f on elements of s.
Русский
Образ множества s под отображением f: α → β равен f''s = { f(a) | a ∈ s }. Это все значения, которые принимает f на элементах s.
LaTeX
$$$f''s = \{f(a) \mid a \in s\}$$$
Lean4
/-- The image of `s : Set α` by `f : α → β`, written `f '' s`, is the set of `b : β` such that
`f a = b` for some `a ∈ s`. -/
def image {β : Type v} (f : α → β) (s : Set α) : Set β :=
{f a | a ∈ s}