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 #

TODO #

class LocallyConvexSpace (𝕜 : Type u_1) (E : Type u_2) [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace 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.convex_basis {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [self : LocallyConvexSpace 𝕜 E] (x : E) :
    (nhds x).HasBasis (fun (s : Set E) => s nhds x Convex 𝕜 s) id
    theorem locallyConvexSpace_iff (𝕜 : Type u_1) (E : Type u_2) [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
    LocallyConvexSpace 𝕜 E ∀ (x : E), (nhds x).HasBasis (fun (s : Set E) => s nhds x Convex 𝕜 s) id
    theorem LocallyConvexSpace.ofBases (𝕜 : Type u_1) (E : Type u_2) [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] {ι : Type u_3} (b : EιSet E) (p : EιProp) (hbasis : ∀ (x : E), (nhds x).HasBasis (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) [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [LocallyConvexSpace 𝕜 E] :
    (nhds 0).HasBasis (fun (s : Set E) => s nhds 0 Convex 𝕜 s) id
    theorem locallyConvexSpace_iff_exists_convex_subset (𝕜 : Type u_1) (E : Type u_2) [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
    LocallyConvexSpace 𝕜 E ∀ (x : E), Unhds x, Snhds x, Convex 𝕜 S S U
    theorem LocallyConvexSpace.ofBasisZero (𝕜 : Type u_1) (E : Type u_2) [OrderedSemiring 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] {ι : Type u_3} (b : ιSet E) (p : ιProp) (hbasis : (nhds 0).HasBasis p b) (hconvex : ∀ (i : ι), p iConvex 𝕜 (b i)) :
    theorem locallyConvexSpace_iff_zero (𝕜 : Type u_1) (E : Type u_2) [OrderedSemiring 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] :
    LocallyConvexSpace 𝕜 E (nhds 0).HasBasis (fun (s : Set E) => s nhds 0 Convex 𝕜 s) id
    theorem locallyConvexSpace_iff_exists_convex_subset_zero (𝕜 : Type u_1) (E : Type u_2) [OrderedSemiring 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] :
    LocallyConvexSpace 𝕜 E Unhds 0, Snhds 0, Convex 𝕜 S S U
    theorem LocallyConvexSpace.convex_open_basis_zero (𝕜 : Type u_1) (E : Type u_2) [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] [LocallyConvexSpace 𝕜 E] :
    (nhds 0).HasBasis (fun (s : Set E) => 0 s IsOpen s Convex 𝕜 s) id
    theorem Disjoint.exists_open_convexes {𝕜 : Type u_1} {E : Type u_2} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] [LocallyConvexSpace 𝕜 E] {s : Set E} {t : Set E} (disj : Disjoint s t) (hs₁ : Convex 𝕜 s) (hs₂ : IsCompact s) (ht₁ : Convex 𝕜 t) (ht₂ : IsClosed t) :
    ∃ (u : Set E) (v : Set E), IsOpen u IsOpen 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} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {ts : Set (TopologicalSpace E)} (h : tts, LocallyConvexSpace 𝕜 E) :
    theorem locallyConvexSpace_iInf {ι : Sort u_1} {𝕜 : Type u_2} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {ts' : ιTopologicalSpace E} (h' : ∀ (i : ι), LocallyConvexSpace 𝕜 E) :
    theorem locallyConvexSpace_inf {𝕜 : Type u_2} {E : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {t₁ : TopologicalSpace E} {t₂ : TopologicalSpace E} (h₁ : LocallyConvexSpace 𝕜 E) (h₂ : LocallyConvexSpace 𝕜 E) :
    theorem locallyConvexSpace_induced {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] {t : TopologicalSpace F} [LocallyConvexSpace 𝕜 F] (f : E →ₗ[𝕜] F) :
    instance Pi.locallyConvexSpace {𝕜 : Type u_2} [OrderedSemiring 𝕜] {ι : 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)
    Equations
    • =
    instance Prod.locallyConvexSpace {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace E] [TopologicalSpace F] [LocallyConvexSpace 𝕜 E] [LocallyConvexSpace 𝕜 F] :
    Equations
    • =