English
If F is a complete uniform additive group with continuous scalar action, and a coherence condition holds with von Neumann bounded domain sets, then the space of continuous linear maps E →SL[σ] F, endowed with the strong topology, is complete.
Русский
Пусть F — полноформное униформное аддитивное множество с непрерывным скалярным действием, и выполняется условие когерентности по von Neumann ограниченным множествам в области. Тогда пространство непрерывных линейных отображений E →SL[σ] F с сильной топологией полно.
LaTeX
$$$(IsUniformAddGroup\\, F) \\wedge CompleteSpace(F) \\wedge IsInducing( ) \\Rightarrow CompleteSpace(E \\toSL[σ] F)$$$
Lean4
theorem completeSpace [UniformSpace F] [IsUniformAddGroup F] [ContinuousSMul 𝕜₂ F] [CompleteSpace F]
[ContinuousSMul 𝕜₁ E] (h : IsCoherentWith {s : Set E | IsVonNBounded 𝕜₁ s}) : CompleteSpace (E →SL[σ] F) :=
UniformConvergenceCLM.completeSpace _ _ h isVonNBounded_covers
