nnnorm_apply_le — Mathlib

English

Let p ≥ 1 and ι be finite. For any x in the Lp-product PiLp p β, the i-th NN-norm of x_i is at most the NN-norm of x: ‖x_i‖₊ ≤ ‖x‖₊ for all i.

Русский

Пусть p ≥ 1 и ι — конечное множество. Для любого x в PiLp p β выполняется неравенство ‖x_i‖₊ ≤ ‖x‖₊ для каждого i.

LaTeX

$$$$ \forall i : \iota,\; \|x_i\|_{+} \le \|x\|_{+} $$$$

Lean4

theorem nnnorm_apply_le [∀ i, SeminormedAddCommGroup (β i)] (x : PiLp p β) (i : ι) : ‖x i‖₊ ≤ ‖x‖₊ := by
  simpa using nndist_apply_le x 0 i

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