English
Let a and b be real numbers. The diameter of the open interval (a, b) with respect to the extended metric equals ENNReal.ofReal(b − a). In particular, if b ≤ a the interval is empty and the diameter is 0, which matches ENNReal.ofReal(b − a) by the convention for negative lengths.
Русский
Пусть a и b — вещественные числа. Диаметр открытого интервала (a, b) по расширенной метрике равен ENNReal.ofReal(b − a). В частности, если b ≤ a, интервал пуст, и диаметр равен 0, что согласуется с ENNReal.ofReal(b − a).
LaTeX
$$$\operatorname{ediam}(I\!oo\, a\, b) = \operatorname{ofReal}(b - a)$$$
Lean4
@[simp]
theorem ediam_Ioo (a b : ℝ) : EMetric.diam (Ioo a b) = ENNReal.ofReal (b - a) :=
by
rcases le_or_gt b a with (h | h)
· simp [h]
· rw [Real.ediam_eq (isBounded_Ioo _ _), csSup_Ioo h, csInf_Ioo h]
