bounded — Mathlib

English

There exists a constant C such that for all x,y in α, dist(f(x), f(y)) ≤ C. In words, the image of f is bounded.

Русский

Существует константа C, такая что для любых x,y ∈ α выполняется d(f(x), f(y)) ≤ C; образ f ограничен.

LaTeX

$$$\exists C \in \mathbb{R}, \forall x,y \in \alpha, \operatorname{dist}(f(x), f(y)) \le C$$$

Lean4

protected theorem bounded (f : α →ᵇ β) : ∃ C, ∀ x y : α, dist (f x) (f y) ≤ C :=
  f.map_bounded'

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