nnnorm_eq_of_L1 — Mathlib

English

For x ∈ PiLp 1 β, the NNReal norm of x coincides with the sum of the NNReal norms of its coordinates: ‖x‖₊ = ∑_i ‖x_i‖₊.

Русский

Для x ∈ PiLp 1 β получаем, что nnnorm x равна сумме nnnorm координат: ‖x‖₊ = ∑_i ‖x_i‖₊.

LaTeX

$$$\|x\|_{\mathbb{R}_{+}} = \sum_{i\in ι} \|x_i\|_{\mathbb{R}_{+}},\quad x:\; PiLp\; 1\; β$$$

Lean4

theorem nnnorm_eq_of_L1 (x : PiLp 1 β) : ‖x‖₊ = ∑ i : ι, ‖x i‖₊ :=
  NNReal.eq <| by push_cast; exact norm_eq_of_L1 x

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