ediam_range — Mathlib

English

The diameter of the range of an isometry equals the diameter of the whole domain.

Русский

Диаметр образа диапазона изометрии равен диаметру всей области.

LaTeX

$$$\operatorname{ediam}(\operatorname{range}(f)) = \operatorname{ediam}(\mathrm{univ})$$$

Lean4

theorem ediam_range [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) :
    EMetric.diam (range f) = EMetric.diam (univ : Set E) :=
  (SemilinearIsometryClass.isometry f).ediam_range

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