# Documentation

Mathlib.Topology.Algebra.Module.LocallyConvex

# Locally convex topological modules #

A LocallyConvexSpace 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 #

• locallyConvexSpace_iff_zero : in a module, local convexity at zero gives local convexity everywhere
• WithSeminorms.locallyConvexSpace : a topology generated by a family of seminorms is locally convex (in Analysis.LocallyConvex.WithSeminorms)
• NormedSpace.locallyConvexSpace : a normed space is locally convex (in Analysis.LocallyConvex.WithSeminorms)

## TODO #

• define a structure LocallyConvexFilterBasis, extending ModuleFilterBasis, for filter bases generating a locally convex topology
class LocallyConvexSpace (𝕜 : Type u_1) (E : Type u_2) [] [] [Module 𝕜 E] [] :

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

Instances
theorem locallyConvexSpace_iff (𝕜 : Type u_1) (E : Type u_2) [] [] [Module 𝕜 E] [] :
∀ (x : E), Filter.HasBasis (nhds x) (fun s => s nhds x Convex 𝕜 s) id
theorem LocallyConvexSpace.ofBases (𝕜 : Type u_1) (E : Type u_2) [] [] [Module 𝕜 E] [] {ι : Type u_3} (b : EιSet E) (p : EιProp) (hbasis : ∀ (x : E), Filter.HasBasis (nhds x) (p x) (b x)) (hconvex : ∀ (x : E) (i : ι), p x iConvex 𝕜 (b x i)) :
theorem LocallyConvexSpace.convex_basis_zero (𝕜 : Type u_1) (E : Type u_2) [] [] [Module 𝕜 E] [] [] :
Filter.HasBasis (nhds 0) (fun s => s nhds 0 Convex 𝕜 s) id
theorem locallyConvexSpace_iff_exists_convex_subset (𝕜 : Type u_1) (E : Type u_2) [] [] [Module 𝕜 E] [] :
∀ (x : E) (U : Set E), U nhds xS, S nhds x Convex 𝕜 S S U
theorem LocallyConvexSpace.ofBasisZero (𝕜 : Type u_1) (E : Type u_2) [] [] [Module 𝕜 E] [] {ι : Type u_3} (b : ιSet E) (p : ιProp) (hbasis : Filter.HasBasis (nhds 0) p b) (hconvex : ∀ (i : ι), p iConvex 𝕜 (b i)) :
theorem locallyConvexSpace_iff_zero (𝕜 : Type u_1) (E : Type u_2) [] [] [Module 𝕜 E] [] :
Filter.HasBasis (nhds 0) (fun s => s nhds 0 Convex 𝕜 s) id
theorem locallyConvexSpace_iff_exists_convex_subset_zero (𝕜 : Type u_1) (E : Type u_2) [] [] [Module 𝕜 E] [] :
∀ (U : Set E), U nhds 0S, S nhds 0 Convex 𝕜 S S U
instance LocallyConvexSpace.toLocallyConnectedSpace (E : Type u_2) [] [] [] [] [] :
theorem LocallyConvexSpace.convex_open_basis_zero (𝕜 : Type u_1) (E : Type u_2) [] [Module 𝕜 E] [] [] [] :
Filter.HasBasis (nhds 0) (fun s => 0 s Convex 𝕜 s) id
theorem Disjoint.exists_open_convexes {𝕜 : Type u_1} {E : Type u_2} [] [Module 𝕜 E] [] [] [] {s : Set E} {t : Set E} (disj : Disjoint s t) (hs₁ : Convex 𝕜 s) (hs₂ : ) (ht₁ : Convex 𝕜 t) (ht₂ : ) :
u v, Convex 𝕜 u Convex 𝕜 v s u t v Disjoint u 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 locallyConvexSpace_sInf {𝕜 : Type u_2} {E : Type u_3} [] [] [Module 𝕜 E] {ts : } (h : ∀ (t : ), t ts) :
theorem locallyConvexSpace_iInf {ι : Sort u_1} {𝕜 : Type u_2} {E : Type u_3} [] [] [Module 𝕜 E] {ts' : ι} (h' : ∀ (i : ι), ) :
theorem locallyConvexSpace_inf {𝕜 : Type u_2} {E : Type u_3} [] [] [Module 𝕜 E] {t₁ : } {t₂ : } (h₁ : ) (h₂ : ) :
theorem locallyConvexSpace_induced {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [] [] [Module 𝕜 E] [] [Module 𝕜 F] {t : } [] (f : E →ₗ[𝕜] F) :
instance Pi.locallyConvexSpace {𝕜 : Type u_2} [] {ι : Type u_5} {X : ιType u_6} [(i : ι) → AddCommMonoid (X i)] [(i : ι) → TopologicalSpace (X i)] [(i : ι) → Module 𝕜 (X i)] [∀ (i : ι), LocallyConvexSpace 𝕜 (X i)] :
LocallyConvexSpace 𝕜 ((i : ι) → X i)
instance Prod.locallyConvexSpace {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [] [] [Module 𝕜 E] [] [Module 𝕜 F] [] [] [] [] :