Theorems · Theorem · functional analysis

lp.linearMapOfLE_comp

∀ {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] [inst_1 : NormedRing 𝕜]
  [inst_2 : (i : α) → Module 𝕜 (E i)] [inst_3 : ∀ (i : α), IsBoundedSMul 𝕜 (E i)] {p q r : ENNReal} (hpq : p ≤ q)
  (hqr : q ≤ r), lp.linearMapOfLE 𝕜 E hqr ∘ₗ lp.linearMapOfLE 𝕜 E hpq = lp.linearMapOfLE 𝕜 E ⋯

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

NormedAddCommGroupNormedRingModuleIsBoundedSMul