English
Theorem isUniformInducing_postcomp asserts uniform-inducing property for composition with ContinuousMultilinearMap into another target.
Русский
Теорема isUniformInducing_postcomp утверждает свойство равномерной индукции для композиции с ContinuousMultilinearMap в другую целевую пространство.
LaTeX
$$isUniformInducing_postcomp {G : Type*} [AddCommGroup G] [UniformSpace G] [IsUniformAddGroup G] [Module 𝕜 G] (g : F →L[𝕜] G) (hg : IsUniformInducing g) : IsUniformInducing (g.compContinuousMultilinearMap : ContinuousMultilinearMap 𝕜 E F → ContinuousMultilinearMap 𝕜 E G)$$
Lean4
theorem completeSpace (h : IsCoherentWith {s : Set (Π i, E i) | IsVonNBounded 𝕜 s}) :
CompleteSpace (ContinuousMultilinearMap 𝕜 E F) := by
classical
wlog hF : T2Space F generalizing F
· rw [(isUniformInducing_postcomp (SeparationQuotient.mkCLM _ _)
SeparationQuotient.isUniformInducing_mk).completeSpace_congr]
· exact this inferInstance
· intro f
use (SeparationQuotient.outCLM _ _).compContinuousMultilinearMap f
simp [DFunLike.ext_iff]
have H : ∀ {m : Π i, E i}, Continuous fun f : (Π i, E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F ↦ toFun _ f m :=
(uniformContinuous_eval (isVonNBounded_covers) _).continuous
rw [completeSpace_iff_isComplete_range isUniformInducing_toUniformOnFun, range_toUniformOnFun]
simp only [setOf_and, setOf_forall]
apply_rules [IsClosed.isComplete, IsClosed.inter]
· exact UniformOnFun.isClosed_setOf_continuous h
·
exact
isClosed_iInter fun m ↦
isClosed_iInter fun i ↦ isClosed_iInter fun x ↦ isClosed_iInter fun y ↦ isClosed_eq H (H.add H)
·
exact
isClosed_iInter fun m ↦
isClosed_iInter fun i ↦ isClosed_iInter fun c ↦ isClosed_iInter fun x ↦ isClosed_eq H (H.const_smul _)
