ediam_Icc — Mathlib

English

Let a and b be real numbers. The diameter of the closed interval [a, b] with respect to the extended metric equals ENNReal.ofReal(b − a).

Русский

Пусть a и b — вещественные числа. Диаметр закрытого интервала [a, b] по расширенной метрике равен ENNReal.ofReal(b − a).

LaTeX

$$$\operatorname{ediam}(I\!cc\, a\, b) = \operatorname{ofReal}(b - a)$$$

Lean4

@[simp]
theorem ediam_Icc (a b : ℝ) : EMetric.diam (Icc a b) = ENNReal.ofReal (b - a) :=
  by
  rcases le_or_gt a b with (h | h)
  · rw [Real.ediam_eq (isBounded_Icc _ _), csSup_Icc h, csInf_Icc h]
  · simp [h, h.le]

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