# mathlib3documentation

topology.algebra.module.locally_convex

# Locally convex topological modules #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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
@[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)
@[protected, instance]
theorem locally_convex_space.convex_open_basis_zero (𝕜 : Type u_1) (E : Type u_2) [ E] [ E] :
(nhds 0).has_basis (λ (s : set E), 0 s s) id
theorem disjoint.exists_open_convexes {𝕜 : Type u_1} {E : Type u_2} [ E] [ E] {s t : set E} (disj : t) (hs₁ : s) (hs₂ : is_compact s) (ht₁ : t) (ht₂ : is_closed t) :
(u v : set E), u v s u t v v

In a locally convex space, if s, t are disjoint convex sets, s is compact and t is closed, then we can find open disjoint convex sets containing them.

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)