diam_le — Mathlib

English

If every pair of points in s has edist at most d, then the diameter of s is at most d.

Русский

Если для всех x, y ∈ s выполнено edist(x, y) ≤ d, то diam(s) ≤ d.

LaTeX

$$((∀ x ∈ s, ∀ y ∈ s, \operatorname{edist}(x, y) ≤ d)) ⇒ \operatorname{diam}(s) ≤ d$$

Lean4

/-- If the distance between any two points in a set is bounded by some constant, this constant
bounds the diameter. -/
theorem diam_le {d : ℝ≥0∞} (h : ∀ x ∈ s, ∀ y ∈ s, edist x y ≤ d) : diam s ≤ d :=
  diam_le_iff.2 h

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