range — Mathlib

English

Range of a function is the set of all outputs, i.e., { x | ∃ y, f(y) = x }.

Русский

Образ функции есть множество всех значений, достижимых как x = f(y).

LaTeX

$$$\\mathrm{range}(f) = \\{ x \\mid \\exists y, f(y) = x \\}$$$

Lean4

/-- Range of a function.

This function is more flexible than `f '' univ`, as the image requires that the domain is in Type
and not an arbitrary Sort. -/
def range (f : ι → α) : Set α :=
  {x | ∃ y, f y = x}

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