nnnorm_fst_le — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem nnnorm_fst_le [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (x : WithLp p (α × β)) : ‖x.fst‖₊ ≤ ‖x‖₊ :=
  by simpa using nndist_fst_le x 0

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