image — Mathlib

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

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