English
If two continuous linear maps from lp(E,p) to F agree on all lp.single p i, then they are equal.
Русский
Если два непрерывных линейных отображения из lp(E,p) в F совпадают на всех lp.single p i, то они равны.
LaTeX
$$$\\forall f,g: lp(E,p) \\to_L[F],\\; (\\forall i, f \\circ singleContinuousLinearMap(𝕜,E,p,i) = g \\circ singleContinuousLinearMap(𝕜,E,p,i)) \\Rightarrow f = g.$$$
Lean4
/-- Two continuous linear 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_continuousLinearMap {F : Type*} [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] [T2Space F]
[Fact (1 ≤ p)] (hp : p ≠ ⊤) ⦃f g : lp E p →L[𝕜] F⦄
(h : ∀ i, f.comp (singleContinuousLinearMap 𝕜 E p i) = g.comp (singleContinuousLinearMap 𝕜 E p i)) : f = g :=
ContinuousLinearMap.toContinuousAddMonoidHom_injective <|
ext_continuousAddMonoidHom hp fun i => ContinuousLinearMap.toContinuousAddMonoidHom_inj.2 (h i)
