unitization_norm_inr — Mathlib

English

The embedding of A into WithLp 1 (Unitization 𝕜 A) preserves norms: for x in A, ||toLp 1 (x : Unitization 𝕜 A)|| = ||x||.

Русский

Встроение A в WithLp 1 (Unitization 𝕜 A) сохраняет норму: для x ∈ A имеет место ||toLp 1 (x : Unitization 𝕜 A)|| = ||x||.

LaTeX

$$$\\|toLp 1 (x : Unitization 𝕜 A)\\| = \\|x\\|$$$

Lean4

theorem unitization_norm_inr (x : A) : ‖toLp 1 (x : Unitization 𝕜 A)‖ = ‖x‖ := by simp [unitization_norm_def]

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