nnnorm_snd_le — Mathlib

English

For x in WithLp p (α × β), the NN-norm of the second coordinate is not larger than the NN-norm of x.

Русский

Для x ∈ WithLp p (α × β) nnnorm второго координата не превосходит nnnorm самого x.

LaTeX

$$$\|x_{\mathrm{snd}}\|_{\!nn} \le \|x\|_{\!nn}$$$

Lean4

theorem nnnorm_snd_le [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (x : WithLp p (α × β)) : ‖x.snd‖₊ ≤ ‖x‖₊ :=
  by simpa using nndist_snd_le x 0

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