English
Two continuous linear maps 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: lp(E,p) \\to_L[𝕜] F,\\; (\\forall i, f \\circ singleContinuousLinearMap(𝕜,E,p,i) = g \\circ singleContinuousLinearMap(𝕜,E,p,i)) \\Rightarrow f = g.$$$
Lean4
instance completeSpace : CompleteSpace (lp E p) :=
Metric.complete_of_cauchySeq_tendsto
(by
intro F hF
obtain ⟨f, hf⟩ :=
cauchySeq_tendsto_of_complete
((uniformContinuous_coe (p := p)).comp_cauchySeq hF)
-- Since the Cauchy sequence is bounded, its pointwise limit `f` is in `lp E p`.
have hf' : Memℓp f p := memℓp_of_tendsto hF.isBounded_range hf
exact ⟨⟨f, hf'⟩, tendsto_lp_of_tendsto_pi hF hf⟩)
