ediam_Ico — 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\!co\, a\, b) = \operatorname{ofReal}(b - a)$$$

Lean4

@[simp]
theorem ediam_Ico (a b : ℝ) : EMetric.diam (Ico a b) = ENNReal.ofReal (b - a) :=
  le_antisymm (ediam_Icc a b ▸ diam_mono Ico_subset_Icc_self) (ediam_Ioo a b ▸ diam_mono Ioo_subset_Ico_self)

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