isometry

Mathlib.Topology.MetricSpace.Isometry

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

English

For h: α ≃ᵢ β, h is an isometry.

Русский

Для h: α ≃ᵢ β, h является изометрией.

LaTeX

$$$ \operatorname{Isometry}(h). $$$

Lean4

protected theorem isometry (h : α ≃ᵢ β) : Isometry h :=
  h.isometry_toFun

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

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

Разделы

Аффилиация

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