English
Two continuous additive monoid homomorphisms from lp(E,p) to F are equal if they agree on all coordinate embeddings lp.single p i.
Русский
Два непрерывных аддитивных однородных отображения из lp(E,p) в F равны, если совпадают на всех координатах lp.single p i.
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
/-- If a sequence is Cauchy in the `lp E p` topology and pointwise convergent to an element `f` of
`lp E p`, then it converges to `f` in the `lp E p` topology. -/
theorem tendsto_lp_of_tendsto_pi {F : ℕ → lp E p} (hF : CauchySeq F) {f : lp E p}
(hf : Tendsto (id fun i => F i : ℕ → ∀ a, E a) atTop (𝓝 f)) : Tendsto F atTop (𝓝 f) :=
by
rw [Metric.nhds_basis_closedBall.tendsto_right_iff]
intro ε hε
have hε' : {p : lp E p × lp E p | ‖p.1 - p.2‖ < ε} ∈ uniformity (lp E p) :=
NormedAddCommGroup.uniformity_basis_dist.mem_of_mem hε
refine (hF.eventually_eventually hε').mono ?_
rintro n (hn : ∀ᶠ l in atTop, ‖(fun f => F n - f) (F l)‖ < ε)
refine norm_le_of_tendsto (hn.mono fun k hk => hk.le) ?_
rw [tendsto_pi_nhds]
intro a
exact (hf.apply_nhds a).const_sub (F n a)
