English
If 𝔖 is coherent and its union is all of E, then the space of uniform convergence CLMs on 𝔖 is complete (provided F is complete and other natural hypotheses hold).
Русский
Если семейство 𝔖 совместимо и объединение 𝔖 равно всему E, тогда пространство равномерной связности для UniformConvergenceCLM на 𝔖 является полным (при выполнении прочих естественных предпосылок).
LaTeX
$$$$ \text{CompleteSpace}(\mathrm{UniformConvergenceCLM}_{\sigma} F \mathfrak{S}) $$$$
Lean4
theorem completeSpace [UniformSpace F] [IsUniformAddGroup F] [ContinuousSMul 𝕜₂ F] [CompleteSpace F] {𝔖 : Set (Set E)}
(h𝔖 : IsCoherentWith 𝔖) (h𝔖U : ⋃₀ 𝔖 = univ) : CompleteSpace (UniformConvergenceCLM σ F 𝔖) :=
by
wlog hF : T2Space F generalizing F
· rw [(isUniformInducing_postcomp σ (SeparationQuotient.mkCLM 𝕜₂ F) SeparationQuotient.isUniformInducing_mk
_).completeSpace_congr]
exacts [this _ inferInstance, SeparationQuotient.postcomp_mkCLM_surjective F σ E]
rw [completeSpace_iff_isComplete_range (isUniformInducing_coeFn _ _ _)]
apply IsClosed.isComplete
have H₁ : IsClosed {f : E →ᵤ[𝔖] F | Continuous ((UniformOnFun.toFun 𝔖) f)} :=
UniformOnFun.isClosed_setOf_continuous h𝔖
convert
H₁.inter <| (LinearMap.isClosed_range_coe E F σ).preimage (UniformOnFun.uniformContinuous_toFun h𝔖U).continuous
exact ContinuousLinearMap.range_coeFn_eq
