isometry_inl — Mathlib

English

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

Русский

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

LaTeX

$$$ \mathrm{isometry\_inl} : \mathrm{Isometry}(\mathrm{Sum.inl} ). $$$

Lean4

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

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