unitization_isometry_inr — Mathlib

English

The map x ↦ toLp 1 (Unitization.inr x) from A into WithLp 1 (Unitization 𝕜 A) is an isometry, i.e., distance is preserved.

Русский

Отображение x ↦ toLp 1 (Unitization.inr x) от A в WithLp 1 (Unitization 𝕜 A) является изометрией, то есть сохраняет расстояния.

LaTeX

$$$\forall x,y \in A, \\|toLp 1 (Unitization.inr x) - toLp 1 (Unitization.inr y)\\| = \\|x - y\\|$$$

Lean4

theorem unitization_isometry_inr : Isometry fun x : A ↦ toLp 1 (x : Unitization 𝕜 A) :=
  AddMonoidHomClass.isometry_of_norm ((WithLp.linearEquiv 1 𝕜 (Unitization 𝕜 A)).symm.comp <| Unitization.inrHom 𝕜 A)
    unitization_norm_inr

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