unitization_nnnorm_inr — Mathlib

English

The embedding of A into WithLp 1 (Unitization 𝕜 A) preserves the NN-norm: ||toLp 1 (x : Unitization 𝕜 A)||_+ = ||x||_+.

Русский

Встроение A в WithLp 1 (Unitization 𝕜 A) сохраняет NN-норму: ||toLp 1 (x : Unitization 𝕜 A)||_+ = ||x||_+.

LaTeX

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

Lean4

theorem unitization_nnnorm_inr (x : A) : ‖toLp 1 (x : Unitization 𝕜 A)‖₊ = ‖x‖₊ := by simp [unitization_nnnorm_def]

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