diam_range

Mathlib.Topology.MetricSpace.Isometry

URI: https://scilib.ai/kg/mathlib#Isometry.diam_range

English

The diameter of the image range of an isometry equals the diameter of the whole space.

Русский

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

LaTeX

$$$Isometry(f) \rightarrow Metric.diam( range(f) ) = Metric.diam( univ : Set \alpha )$$$

Lean4

theorem diam_range (hf : Isometry f) : Metric.diam (range f) = Metric.diam (univ : Set α) :=
  by
  rw [← image_univ]
  exact hf.diam_image univ

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

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

Разделы

Аффилиация

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