Theorems · Theorem · functional analysis

pi_norm_le_iff_of_nonneg

∀ {ι : Type u_1} {G : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedAddGroup (G i)] {x : (i : ι) → G i}
  {r : ℝ}, 0 ≤ r → (‖x‖ ≤ r ↔ ∀ (i : ι), ‖x i‖ ≤ r)

The seminorm of an element in a product space is ≤ r if and only if the norm of each component is.

Defined in

Mathlib.Analysis.Normed.Group.Constructions

Cited by

18 results in Mathlib

Foundations

Depth 155 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeSeminormedAddGroup