unitization_nnnorm_def — Mathlib

English

Let x lie in the L1-unitization of A. Then the nonnegative norm of x equals the sum of the nonnegative norms of its scalar part and its A-part: ||x||_+ = ||fst||_+ + ||snd||_+.

Русский

Пусть x принадлежит единичизации A в рамках конструкций WithLp. Тогда ненулевой NN-норме x соответствует сумма NN-норм его скалярной части и части из A: ||x||_+ = ||fst||_+ + ||snd||_+.

LaTeX

$$$\\|x\\|_+ = \\|(ofLp x).fst\\|_+ + \\|(ofLp x).snd\\|_+$$$

Lean4

theorem unitization_nnnorm_def (x : WithLp 1 (Unitization 𝕜 A)) : ‖x‖₊ = ‖(ofLp x).fst‖₊ + ‖(ofLp x).snd‖₊ :=
  Subtype.ext <| unitization_norm_def x

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