toGlueR_isometry

Mathlib.Topology.MetricSpace.Gluing

URI: https://scilib.ai/kg/mathlib#Metric.toGlueR_isometry

English

The right glue map is an isometry.

Русский

Правая карта склейки является изометрией.

LaTeX

$$$\text{Isometry}(\mathrm{toGlueR}(h_\Phi,h_\Psi))$$$

Lean4

theorem toGlueR_isometry (hΦ : Isometry Φ) (hΨ : Isometry Ψ) : Isometry (toGlueR hΦ hΨ) :=
  Isometry.of_dist_eq fun _ _ => rfl

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

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

Разделы

Аффилиация

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