isBounded_range_iff — Mathlib

English

For a function f, the range is bounded iff there exists a constant C bounding all pairwise distances in the image.

Русский

Для функции f множество образа ограничено тогда и только тогда, существует константа C, ограничивающая все попарные расстояния между изображениями.

LaTeX

$$$IsBounded(\operatorname{range} f) \iff \exists C, \forall x,y, \operatorname{dist}(f x, f y) \le C$$$

Lean4

/-- Characterization of the boundedness of the range of a function -/
theorem isBounded_range_iff {f : β → α} : IsBounded (range f) ↔ ∃ C, ∀ x y, dist (f x) (f y) ≤ C :=
  isBounded_iff.trans <| by simp only [forall_mem_range]

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