English
Let 0 < r. Then for x ∈ ∏ G_i, the norm is less than r exactly when every component norm is less than r: ∥x∥ < r iff ∀ i, ∥x_i∥ < r.
Русский
Пусть 0 < r. Тогда для x ∈ ∏ G_i верно: ∥x∥ < r тогда и только если для всех i выполняется ∥x_i∥ < r.
LaTeX
$$$ (0 < r) \Rightarrow ( \|x\| < r \iff \forall i, \|x_i\| < r )$$$
Lean4
/-- The seminorm of an element in a product space is `< r` if and only if the norm of each
component is. -/
@[to_additive pi_norm_lt_iff /-- The seminorm of an element in a product space is `< r` if and only
if the norm of each component is. -/
]
theorem pi_norm_lt_iff' (hr : 0 < r) : ‖x‖ < r ↔ ∀ i, ‖x i‖ < r := by
simp only [← dist_one_right, dist_pi_lt_iff hr, Pi.one_apply]
