toGlueL_isometry

Mathlib.Topology.MetricSpace.Gluing

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

English

The injection map i ↦ Sigma.mk i is an isometry.

Русский

Инъекция i ↦ Sigma.mk i является изометрией.

LaTeX

$$$\text{Isometry}(\Sigma.mk_i : E_i \to \Sigma_k E_k)$$$

Lean4

theorem toGlueL_isometry (hΦ : Isometry Φ) (hΨ : Isometry Ψ) : Isometry (toGlueL hΦ hΨ) :=
  Isometry.of_dist_eq fun _ _ => rfl

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

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

Разделы

Аффилиация

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