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 #

Todo #

Tags #

locally convex, bounded convergence

theorem ContinuousLinearMap.strongTopology.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] [TopologicalAddGroup F] [OrderedSemiring R] [NormedField 𝕜₁] [NormedField 𝕜₂] [Module 𝕜₁ E] [Module 𝕜₂ F] {σ : 𝕜₁ →+* 𝕜₂} [Module R F] [ContinuousConstSMul R F] [LocallyConvexSpace R F] [SMulCommClass 𝕜₂ R F] (𝔖 : Set (Set E)) (h𝔖₁ : Set.Nonempty 𝔖) (h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖) :