diam_preimage

Mathlib.Topology.MetricSpace.Isometry

URI: https://scilib.ai/kg/mathlib#IsometryEquiv.diam_preimage

English

Diameter is preserved under preimages by an isometry: diam(h⁻¹' s) = diam s.

Русский

Диаметр сохраняется при взятии предобраза под изометрией: diam(h⁻¹' s) = diam s.

LaTeX

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

Lean4

@[simp]
theorem diam_preimage (s : Set β) : Metric.diam (h ⁻¹' s) = Metric.diam s := by rw [← image_symm, diam_image]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru