# mathlibdocumentation

topology.algebra.module.locally_convex

# Locally convex topological modules #

A locally_convex_space is a topological semimodule over an ordered semiring in which any point admits a neighborhood basis made of convex sets, or equivalently, in which convex neighborhoods of a point form a neighborhood basis at that point.

In a module, this is equivalent to 0 satisfying such properties.

## Main results #

• locally_convex_space_iff_zero : in a module, local convexity at zero gives local convexity everywhere
• seminorm.locally_convex_space : a topology generated by a family of seminorms is locally convex
• normed_space.locally_convex_space : a normed space is locally convex

## TODO #

• define a structure locally_convex_filter_basis, extending module_filter_basis, for filter bases generating a locally convex topology
• show that any locally convex topology is generated by a family of seminorms
@[class]
structure locally_convex_space (𝕜 : Type u_1) (E : Type u_2) [ E]  :
Prop

A locally_convex_space is a topological semimodule over an ordered semiring in which convex neighborhoods of a point form a neighborhood basis at that point.

Instances of this typeclass
theorem locally_convex_space_iff (𝕜 : Type u_1) (E : Type u_2) [ E]  :
∀ (x : E), (nhds x).has_basis (λ (s : set E), s nhds x s) id
theorem locally_convex_space.of_bases (𝕜 : Type u_1) (E : Type u_2) [ E] {ι : Type u_3} (b : E → ι → set E) (p : E → ι → Prop) (hbasis : ∀ (x : E), (nhds x).has_basis (p x) (b x)) (hconvex : ∀ (x : E) (i : ι), p x i (b x i)) :
theorem locally_convex_space.convex_basis_zero (𝕜 : Type u_1) (E : Type u_2) [ E] [ E] :
(nhds 0).has_basis (λ (s : set E), s nhds 0 s) id
theorem locally_convex_space_iff_exists_convex_subset (𝕜 : Type u_1) (E : Type u_2) [ E]  :
∀ (x : E) (U : set E), U nhds x(∃ (S : set E) (H : S nhds x), S S U)
theorem locally_convex_space.of_basis_zero (𝕜 : Type u_1) (E : Type u_2) [ E] {ι : Type u_3} (b : ι → set E) (p : ι → Prop) (hbasis : (nhds 0).has_basis p b) (hconvex : ∀ (i : ι), p i (b i)) :
theorem locally_convex_space_iff_zero (𝕜 : Type u_1) (E : Type u_2) [ E]  :
(nhds 0).has_basis (λ (s : set E), s nhds 0 s) id
theorem locally_convex_space_iff_exists_convex_subset_zero (𝕜 : Type u_1) (E : Type u_2) [ E]  :
∀ (U : set E), U nhds 0(∃ (S : set E) (H : S nhds 0), S S U)
theorem locally_convex_space_Inf {𝕜 : Type u_2} {E : Type u_3} [ E] {ts : set } (h : ∀ (t : , t ts) :
theorem locally_convex_space_infi {ι : Sort u_1} {𝕜 : Type u_2} {E : Type u_3} [ E] {ts' : ι → } (h' : ∀ (i : ι), ) :
theorem locally_convex_space_inf {𝕜 : Type u_2} {E : Type u_3} [ E] {t₁ t₂ : topological_space E} (h₁ : E) (h₂ : E) :
theorem locally_convex_space_induced {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [ E] [ F] {t : topological_space F} [ F] (f : E →ₗ[𝕜] F) :
@[protected, instance]
def pi.locally_convex_space {𝕜 : Type u_2} {ι : Type u_1} {X : ι → Type u_3} [Π (i : ι), add_comm_monoid (X i)] [Π (i : ι), topological_space (X i)] [Π (i : ι), (X i)] [∀ (i : ι), (X i)] :
(Π (i : ι), X i)
@[protected, instance]
def prod.locally_convex_space {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [ E] [ F] [ E] [ F] :
(E × F)