diam_image — Mathlib

English

There is a natural isometry between a space and its image that preserves diameter: diam(h''s) = diam(s).

Русский

Существует естественная изометрия между пространством и его изображением, сохраняющая диаметр: diam(h''s) = diam(s).

LaTeX

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

Lean4

@[simp]
theorem diam_image (s : Set α) : Metric.diam (h '' s) = Metric.diam s :=
  h.isometry.diam_image s

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