Local convexity of the strong topology

In this file we prove that the strong topology on E →L[ℝ] F is locally convex provided that F is locally convex.

References

• N. Bourbaki, Topological Vector Spaces

TODO

• Characterization in terms of seminorms

Tags

locally convex, bounded convergence

theorem UniformConvergenceCLM.locallyConvexSpace (R : Type u_1) {𝕜₁ : Type u_2} {𝕜₂ : Type u_3} {E : Type u_4} {F : Type u_5} [AddCommGroup E] [TopologicalSpace E] [AddCommGroup F] [TopologicalSpace F] [IsTopologicalAddGroup F] [Semiring R] [PartialOrder R] [NormedField 𝕜₁] [NormedField 𝕜₂] [Module 𝕜₁ E] [Module 𝕜₂ F] {σ : 𝕜₁ →+* 𝕜₂} [Module R F] [ContinuousConstSMul R F] [LocallyConvexSpace R F] [SMulCommClass 𝕜₂ R F] (𝔖 : Set (Set E)) (h𝔖₁ : 𝔖.Nonempty) (h𝔖₂ : DirectedOn (fun (x1 x2 : Set E) => x1 ⊆ x2) 𝔖) : LocallyConvexSpace R (UniformConvergenceCLM σ F 𝔖)

instance ContinuousLinearMap.instLocallyConvexSpace {R : Type u_1} {𝕜₁ : Type u_2} {𝕜₂ : Type u_3} {E : Type u_4} {F : Type u_5} [AddCommGroup E] [TopologicalSpace E] [AddCommGroup F] [TopologicalSpace F] [IsTopologicalAddGroup F] [Semiring R] [PartialOrder R] [NormedField 𝕜₁] [NormedField 𝕜₂] [Module 𝕜₁ E] [Module 𝕜₂ F] {σ : 𝕜₁ →+* 𝕜₂} [Module R F] [ContinuousConstSMul R F] [LocallyConvexSpace R F] [SMulCommClass 𝕜₂ R F] : LocallyConvexSpace R (E →SL[σ] F)