diam_le_iff — Mathlib

English

Characterizes when the diameter is bounded by d via pairwise edist bounds.

Русский

Характеризует, когда диаметр ограничен величиной d через пары расстояний edist.

LaTeX

$$$\\mathrm{diam}(s) \\le d \\iff \\forall x\\in s, \\forall y\\in s, \\ edist(x,y) \\le d$$$

Lean4

theorem diam_le_iff {d : ℝ≥0∞} : diam s ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist x y ≤ d := by simp only [diam, iSup_le_iff]

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