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_iff (𝕜 : Type u_1) (E : Type u_2) [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
    LocallyConvexSpace 𝕜 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) [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace 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 i → Convex 𝕜 (b x i)) :
    theorem LocallyConvexSpace.convex_basis_zero (𝕜 : Type u_1) (E : Type u_2) [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [LocallyConvexSpace 𝕜 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) [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
    LocallyConvexSpace 𝕜 E ↔ ∀ (x : E) (U : Set E), U ∈ nhds x → ∃ S, S ∈ nhds 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 : Filter.HasBasis (nhds 0) p b) (hconvex : ∀ (i : ι), p i → Convex 𝕜 (b i)) :
    theorem locallyConvexSpace_iff_zero (𝕜 : Type u_1) (E : Type u_2) [OrderedSemiring 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] :
    LocallyConvexSpace 𝕜 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) [OrderedSemiring 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] :
    LocallyConvexSpace 𝕜 E ↔ ∀ (U : Set E), U ∈ nhds 0 → ∃ S, S ∈ nhds 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] :
    Filter.HasBasis (nhds 0) (fun s => 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 v, 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 : ∀ (t : TopologicalSpace E), t ∈ ts → 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)
    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] :
    LocallyConvexSpace 𝕜 (E × F)