pi_norm_le_iff_of_nonneg' — Mathlib

English

If r ≥ 0, then the seminorm of the Pi-space element x is ≤ r if and only if every component has norm ≤ r.

Русский

Если r ≥ 0, то полумонормированное пространство Пи-элемент x имеет норму ≤ r тогда и только тогда, когда каждая компонента имеет норму ≤ r.

LaTeX

$$$‖x‖ ≤ r \iff ∀ i, ‖x(i)‖ ≤ r \quad(\text{при } r \ge 0)$$$

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_le_iff_of_nonneg /-- The seminorm of an element in a product space is `≤ r` if
    and only if the norm of each component is. -/
    ]
theorem pi_norm_le_iff_of_nonneg' (hr : 0 ≤ r) : ‖x‖ ≤ r ↔ ∀ i, ‖x i‖ ≤ r := by
  simp only [← dist_one_right, dist_pi_le_iff hr, Pi.one_apply]

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