isBounded_image_iff — Mathlib

English

The image of f is bounded iff there exists a C such that all pairwise distances in the image are bounded by C.

Русский

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

LaTeX

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

Lean4

theorem isBounded_image_iff {f : β → α} {s : Set β} :
    IsBounded (f '' s) ↔ ∃ C, ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ C :=
  isBounded_iff.trans <| by simp only [forall_mem_image]

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