English
The image of a set s under a partial function f is the set of all y for which there exists x ∈ s with y ∈ f(x).
Русский
Образ множества s при частичной функции f — множество всех y, для которых существует x ∈ s такая, что y ∈ f(x).
LaTeX
$$$f.image\\,s = \\{ y : \\beta \\mid \\exists x \\in s,\\ y \\in f(x) \\}$$$
Lean4
/-- Image of a set under a partial function. -/
def image (s : Set α) : Set β :=
f.graph'.image s