diam_range — Mathlib

English

The diameter of the image of a set under f equals the diameter of the set itself in metric terms.

Русский

Диаметр образа множества под действием f равен диаметру самого множества в метрическом смысле.

LaTeX

$$$\operatorname{diam}(f''s) = \operatorname{diam}(s)$$$

Lean4

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

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