English
For a bounded set s ⊆ R, the emetric diameter equals the real difference sSup s − sInf s, viewed as ENNReal.
Русский
Для ограниченного множества s ⊆ ℝ Эм-диаметр равен разности верхней и нижней границ: sSup s − sInf s, представленной как ENNReal.
LaTeX
$$$\operatorname{EMetric}.diam s = \mathrm{ENNReal}.ofReal (\mathrm{sup}(s) - \mathrm{inf}(s))$ for bounded s.$$
Lean4
/-- For a bounded set `s : Set ℝ`, its `EMetric.diam` is equal to `sSup s - sInf s` reinterpreted as
`ℝ≥0∞`. -/
theorem ediam_eq {s : Set ℝ} (h : Bornology.IsBounded s) : EMetric.diam s = ENNReal.ofReal (sSup s - sInf s) :=
by
rcases eq_empty_or_nonempty s with (rfl | hne)
· simp
refine le_antisymm (Metric.ediam_le_of_forall_dist_le fun x hx y hy => ?_) ?_
· exact Real.dist_le_of_mem_Icc (h.subset_Icc_sInf_sSup hx) (h.subset_Icc_sInf_sSup hy)
· apply ENNReal.ofReal_le_of_le_toReal
rw [← Metric.diam, ← Metric.diam_closure]
calc
sSup s - sInf s ≤ dist (sSup s) (sInf s) := le_abs_self _
_ ≤ Metric.diam (closure s) :=
dist_le_diam_of_mem h.closure (csSup_mem_closure hne h.bddAbove) (csInf_mem_closure hne h.bddBelow)
