English
If A is a complete normed space, then 𝓜(𝕜,A) is complete as a normed ring/algebra.
Русский
Если A—полное нормированное пространство, то 𝓜(𝕜,A) также является полным нормированным кольцом/алгеброй.
LaTeX
$$$\text{CompleteSpace}(\mathcal{M}(\mathbb{K},A))$ whenever $\text{CompleteSpace}(A)$$$
Lean4
instance [CompleteSpace A] : CompleteSpace 𝓜(𝕜, A) :=
by
rw [completeSpace_iff_isComplete_range isUniformEmbedding_toProdMulOpposite.isUniformInducing]
apply IsClosed.isComplete
simp only [range_toProdMulOpposite, Set.setOf_forall]
refine isClosed_iInter fun x => isClosed_iInter fun y => isClosed_eq ?_ ?_
·
exact
((ContinuousLinearMap.apply 𝕜 A _).continuous.comp <| continuous_unop.comp continuous_snd).mul continuous_const
exact continuous_const.mul ((ContinuousLinearMap.apply 𝕜 A _).continuous.comp continuous_fst)
