Theorems · Theorem · functional analysis

lp.ext_continuousAddMonoidHom

∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] [inst_1 : DecidableEq α]
  {F : Type u_5} [inst_2 : AddCommMonoid F] [inst_3 : TopologicalSpace F] [T2Space F] [inst_5 : Fact (1 ≤ p)],
  p ≠ ⊤ →
    ∀ ⦃f g : ↥(lp E p) →ₜ+ F⦄,
      (∀ (i : α), f.comp (lp.singleContinuousAddMonoidHom E p i) = g.comp (lp.singleContinuousAddMonoidHom E p i)) →
        f = g

Two continuous additive 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

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupDecidableEqAddCommMonoidTopologicalSpaceT2SpaceFact