Theorems · Theorem · functional analysis

lp.norm_mono

∀ {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] {F : α → Type u_5}
  [inst_1 : (i : α) → NormedAddCommGroup (F i)] {p : ENNReal},
  p ≠ 0 → ∀ {x : ↥(lp E p)} {y : ↥(lp F p)}, (∀ (i : α), ‖↑x i‖ ≤ ‖↑y i‖) → ‖x‖ ≤ ‖y‖

Defined in

Mathlib.Analysis.Normed.Lp.lpSpace

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedAddCommGroup