diam_image_le_iff — Mathlib

English

Let α be a pseudo-emetric space, f: β → α and s ⊆ β. Then the image diameter satisfies diam(f[s]) ≤ d if and only if every pair of points in s has distance at most d after applying f.

Русский

Пусть α — псевдэметрическое пространство, f: β → α, и s ⊆ β. Диаметр образа f[s] не превосходит d тогда и только тогда, когда для любых x, y ∈ s величина edist(f(x), f(y)) ≤ d.

LaTeX

$$$\operatorname{diam}(f[S]) \le d \iff \forall x \in S, \forall y \in S,\ edist(f(x), f(y)) \le d$$$

Lean4

theorem diam_image_le_iff {d : ℝ≥0∞} {f : β → α} {s : Set β} :
    diam (f '' s) ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) ≤ d := by simp only [diam_le_iff, forall_mem_image]

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