inr

Mathlib.Topology.MetricSpace.Isometry

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

English

Inr embedding is an isometry.

Русский

Inr-вложение является изометрией.

LaTeX

$$$Isometry( AddMonoidHom.inr\\, \\alpha \\beta)$ isometry: $edist((0,x),(0,y)) = edist(x,y)$$$

Lean4

protected theorem inr [AddZeroClass α] [AddZeroClass β] : Isometry (AddMonoidHom.inr α β) :=
  by
  intro x y
  rw [Prod.edist_eq]
  simp

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

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

Разделы

Аффилиация

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