diam_eq — Mathlib

English

For any bounded set s ⊆ ℝ, the metric diameter equals sSup s − sInf s.

Русский

Для ограниченного множества s ⊆ ℝ диаметр в метрическом пространстве равен sSup s − sInf s.

LaTeX

$$$\operatorname{Metric}.diam s = sSup s - sInf s$ for bounded s.$$

Lean4

/-- For a bounded set `s : Set ℝ`, its `Metric.diam` is equal to `sSup s - sInf s`. -/
theorem diam_eq {s : Set ℝ} (h : Bornology.IsBounded s) : Metric.diam s = sSup s - sInf s :=
  by
  rw [Metric.diam, Real.ediam_eq h, ENNReal.toReal_ofReal]
  exact sub_nonneg.2 (Real.sInf_le_sSup s h.bddBelow h.bddAbove)

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