ediam_image — Mathlib

English

The diameter distance in the target space of the image equals the diameter distance of the original set.

Русский

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

LaTeX

$$$ \operatorname{EDiam}(f[S]) = \operatorname{EDiam}(S). $$$

Lean4

theorem ediam_image (s : Set α) : EMetric.diam (f '' s) = EMetric.diam s :=
  (IsometryClass.isometry f).ediam_image s

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