Theorems · Theorem · functional analysis

lp.ext_continuousLinearMap

∀ {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)]
  [inst_1 : NormedRing 𝕜] [inst_2 : (i : α) → Module 𝕜 (E i)] [inst_3 : ∀ (i : α), IsBoundedSMul 𝕜 (E i)]
  [inst_4 : DecidableEq α] {F : Type u_5} [inst_5 : AddCommMonoid F] [inst_6 : Module 𝕜 F] [inst_7 : TopologicalSpace F]
  [T2Space F] [inst_9 : Fact (1 ≤ p)],
  p ≠ ⊤ →
    ∀ ⦃f g : ↥(lp E p) →L[𝕜] F⦄,
      (∀ (i : α), f ∘SL lp.singleContinuousLinearMap 𝕜 E p i = g ∘SL lp.singleContinuousLinearMap 𝕜 E p i) → f = g

Two continuous linear maps from lp E p agree if they agree on lp.single. See note [partially-applied ext lemmas].

Defined in

Mathlib.Analysis.Normed.Lp.lpSpace

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedRingModuleIsBoundedSMulDecidableEqAddCommMonoidModuleTopologicalSpaceT2SpaceFact