ran — Mathlib

English

The range of a partial function f is the set of all values f(x) for x in the domain of f.

Русский

Множество значений частичной функции f состоит из всех значений f(x) при x из области определения f.

LaTeX

$$$\\mathrm{ran}(f) = \\{ b \\mid \\exists a, b \\in f(a) \\}$$$

Lean4

/-- The range of a partial function is the set of values
  `f x` where `x` is in the domain of `f`. -/
def ran (f : α →. β) : Set β :=
  {b | ∃ a, b ∈ f a}

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