English
Let (G_i) be a finite family of normed groups and let x = (x_i) be an element of the product ∏_i G_i. Then the NN-norm of x satisfies ∥x∥_+ ≤ r if and only if every coordinate x_i satisfies ∥x_i∥_+ ≤ r, where r ∈ ℝ_{≥0}. In words, the product norm is controlled coordinatewise by a common bound.
Русский
Пусть {G_i} — конечное семейство нормированных групп, а x = (x_i) — элемент произведения ∏_i G_i. Тогда NN-норма x удовлетворяет ∥x∥_+ ≤ r тогда и только тогда, когда для каждого i выполняется ∥x_i∥_+ ≤ r, где r ∈ ℝ_{≥0}. Иначе говоря, нормa произведения контролируется по координатам одним общим верхним пределом.
LaTeX
$$$\|x\|_+ \le r \;\leftrightarrow\; \forall i, \|x_i\|_+ \le r$$$
Lean4
@[to_additive pi_nnnorm_le_iff]
theorem pi_nnnorm_le_iff' {r : ℝ≥0} : ‖x‖₊ ≤ r ↔ ∀ i, ‖x i‖₊ ≤ r :=
pi_norm_le_iff_of_nonneg' r.coe_nonneg
