isometry_inr — Mathlib

English

The right injection is an isometry into the disjoint sum with the glued metric.

Русский

Правое вложение является изометрией в дискретное суммарное пространство с склеенной метрикой.

LaTeX

$$$ \mathrm{isometry\_inr} : \mathrm{Isometry}(\mathrm{Sum.inr}). $$$

Lean4

/-- The right injection of a space in a disjoint union is an isometry -/
theorem isometry_inr : Isometry (Sum.inr : Y → X ⊕ Y) :=
  Isometry.of_dist_eq fun _ _ => rfl

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