nnnorm_le_pi_nnnorm' — Mathlib

English

For any i, the NN-norm of the i-th component is bounded by the NN-norm of the whole tuple: ∥f(i)∥₊ ≤ ∥f∥₊.

Русский

Для любого i нормa NN-нормы i-й компоненты не превышает NN-норму всего кортежа: ∥f(i)∥₊ ≤ ∥f∥₊.

LaTeX

$$$\|f(i)\|_+ \le \|f\|_+$$$

Lean4

@[to_additive nnnorm_le_pi_nnnorm]
theorem nnnorm_le_pi_nnnorm' (i : ι) : ‖f i‖₊ ≤ ‖f‖₊ :=
  norm_le_pi_norm' _ i

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