ediam_range — Mathlib

English

The diameter of the range of f equals the diameter of the whole domain in the E-metric sense.

Русский

Диаметр диапазона отображения f равен диаметру всего множества в рамках E‑метрики.

LaTeX

$$$ \operatorname{EDiam}(\operatorname{range} f) = \operatorname{EDiam}(\operatorname{univ}). $$$

Lean4

theorem ediam_range : EMetric.diam (range f) = EMetric.diam (univ : Set α) :=
  (IsometryClass.isometry f).ediam_range

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