mathlib3 documentation

analysis.locally_convex.strong_topology

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 #

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 𝔖) :
@[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] :