English
Two continuous additive monoid homomorphisms from lp(E,p) to F are equal if they agree on all lp.singleEmbeddings.
Русский
Два непрерывных аддитивных однородных отображения из lp(E,p) в F совпадают, если они совпадают на всех единичных вложениях lp.single.
LaTeX
$$$\\forall f,g: \\mathrm{ContinuousAddMonoidHom}(lp(E,p),F),\\; (\\forall i, f \\circ singleContinuousAddMonoidHom(E,p,i) = g \\circ singleContinuousAddMonoidHom(E,p,i)) \\Rightarrow f = g.$$$
Lean4
/-- Two continuous additive maps from `lp E p` agree if they agree on `lp.single`.
See note [partially-applied ext lemmas]. -/
@[local ext] -- not globally `ext` due to `hp`
theorem ext_continuousAddMonoidHom {F : Type*} [AddCommMonoid F] [TopologicalSpace F] [T2Space F] [Fact (1 ≤ p)]
(hp : p ≠ ⊤) ⦃f g : ContinuousAddMonoidHom (lp E p) F⦄
(h : ∀ i, f.comp (singleContinuousAddMonoidHom E p i) = g.comp (singleContinuousAddMonoidHom E p i)) : f = g :=
by
ext x
classical
have := lp.hasSum_single hp x
rw [← (this.map f f.continuous).tsum_eq, ← (this.map g g.continuous).tsum_eq]
congr! 2 with i
exact DFunLike.congr_fun (h i) (x i)
