Documentation

Mathlib.Analysis.LocallyConvex.StrongTopology

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