ediam_Ioc — Mathlib

English

Let a and b be real numbers. The diameter of the half-open 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\!oc\, a\, b) = \operatorname{ofReal}(b - a)$$$

Lean4

@[simp]
theorem ediam_Ioc (a b : ℝ) : EMetric.diam (Ioc a b) = ENNReal.ofReal (b - a) :=
  le_antisymm (ediam_Icc a b ▸ diam_mono Ioc_subset_Icc_self) (ediam_Ioo a b ▸ diam_mono Ioo_subset_Ioc_self)

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