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][bourbaki1987]
Todo #
- Characterization in terms of seminorms
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 : Set E) => x ⊆ x_1) 𝔖)
:
LocallyConvexSpace R (E →SL[σ] F)
instance
ContinuousLinearMap.instLocallyConvexSpaceContinuousLinearMapToSemiringToDivisionSemiringToSemifieldToFieldToSemiringToDivisionSemiringToSemifieldToFieldToAddCommMonoidToAddCommMonoidAddCommMonoidToContinuousAddToAddGroupModuleToSemiringTopologicalSpace
{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)
Equations
- (_ : LocallyConvexSpace R (E →SL[σ] F)) = (_ : LocallyConvexSpace R (E →SL[σ] F))