enorm_snd_le — Mathlib

English

In WithLp p (α × β), the EN-norm of the second projection is not larger than the EN-norm of the whole element.

Русский

В WithLp p (α × β) EN-нормa второго проекции не превосходит EN-нормы всего элемента.

LaTeX

$$$\|x_{\mathrm{snd}}\|_e \le \,\|x\|_e$$$

Lean4

theorem enorm_snd_le [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (x : WithLp p (α × β)) : ‖x.snd‖ₑ ≤ ‖x‖ₑ :=
  by simpa using edist_snd_le x 0

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