Local convexity of the strong topology #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
continuous_linear_map.strong_topology.locally_convex_space
(R : Type u_1)
{𝕜₁ : Type u_2}
{𝕜₂ : Type u_3}
{E : Type u_4}
{F : Type u_5}
[add_comm_group E]
[topological_space E]
[add_comm_group F]
[topological_space F]
[topological_add_group F]
[ordered_semiring R]
[normed_field 𝕜₁]
[normed_field 𝕜₂]
[module 𝕜₁ E]
[module 𝕜₂ F]
{σ : 𝕜₁ →+* 𝕜₂}
[module R F]
[has_continuous_const_smul R F]
[locally_convex_space R F]
[smul_comm_class 𝕜₂ R F]
(𝔖 : set (set E))
(h𝔖₁ : 𝔖.nonempty)
(h𝔖₂ : directed_on has_subset.subset 𝔖) :
locally_convex_space R (E →SL[σ] F)
@[protected, instance]
def
continuous_linear_map.locally_convex_space
{R : Type u_1}
{𝕜₁ : Type u_2}
{𝕜₂ : Type u_3}
{E : Type u_4}
{F : Type u_5}
[add_comm_group E]
[topological_space E]
[add_comm_group F]
[topological_space F]
[topological_add_group F]
[ordered_semiring R]
[normed_field 𝕜₁]
[normed_field 𝕜₂]
[module 𝕜₁ E]
[module 𝕜₂ F]
{σ : 𝕜₁ →+* 𝕜₂}
[module R F]
[has_continuous_const_smul R F]
[locally_convex_space R F]
[smul_comm_class 𝕜₂ R F] :
locally_convex_space R (E →SL[σ] F)