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 #
- 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]
[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) 𝔖)
:
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]
[TopologicalAddGroup F]
[OrderedSemiring R]
[NormedField 𝕜₁]
[NormedField 𝕜₂]
[Module 𝕜₁ E]
[Module 𝕜₂ F]
{σ : 𝕜₁ →+* 𝕜₂}
[Module R F]
[ContinuousConstSMul R F]
[LocallyConvexSpace R F]
[SMulCommClass 𝕜₂ R F]
:
LocallyConvexSpace R (E →SL[σ] F)