mathlib documentation

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 #

TODO #

@[class]
structure locally_convex_space (𝕜 : Type u_1) (E : Type u_2) [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] [topological_space 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) [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] [topological_space E] :
locally_convex_space 𝕜 E ↔ ∀ (x : E), (nhds x).has_basis (λ (s : set E), s ∈ nhds x ∧ convex 𝕜 s) id
theorem locally_convex_space.of_bases (𝕜 : Type u_1) (E : Type u_2) [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] [topological_space 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 → convex 𝕜 (b x i)) :
theorem locally_convex_space.convex_basis_zero (𝕜 : Type u_1) (E : Type u_2) [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] [topological_space E] [locally_convex_space 𝕜 E] :
(nhds 0).has_basis (λ (s : set E), s ∈ nhds 0 ∧ convex 𝕜 s) id
theorem locally_convex_space_iff_exists_convex_subset (𝕜 : Type u_1) (E : Type u_2) [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] [topological_space E] :
locally_convex_space 𝕜 E ↔ ∀ (x : E) (U : set E), U ∈ nhds x → (∃ (S : set E) (H : S ∈ nhds x), convex 𝕜 S ∧ S ⊆ U)
theorem locally_convex_space.of_basis_zero (𝕜 : Type u_1) (E : Type u_2) [ordered_semiring 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] {ι : Type u_3} (b : ι → set E) (p : ι → Prop) (hbasis : (nhds 0).has_basis p b) (hconvex : ∀ (i : ι), p i → convex 𝕜 (b i)) :
theorem locally_convex_space_iff_zero (𝕜 : Type u_1) (E : Type u_2) [ordered_semiring 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] :
locally_convex_space 𝕜 E ↔ (nhds 0).has_basis (λ (s : set E), s ∈ nhds 0 ∧ convex 𝕜 s) id
theorem locally_convex_space_iff_exists_convex_subset_zero (𝕜 : Type u_1) (E : Type u_2) [ordered_semiring 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] :
locally_convex_space 𝕜 E ↔ ∀ (U : set E), U ∈ nhds 0 → (∃ (S : set E) (H : S ∈ nhds 0), convex 𝕜 S ∧ S ⊆ U)
theorem locally_convex_space_Inf {𝕜 : Type u_2} {E : Type u_3} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {ts : set (topological_space E)} (h : ∀ (t : topological_space E), t ∈ ts → locally_convex_space 𝕜 E) :
theorem locally_convex_space_infi {ι : Sort u_1} {𝕜 : Type u_2} {E : Type u_3} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {ts' : ι → topological_space E} (h' : ∀ (i : ι), locally_convex_space 𝕜 E) :
theorem locally_convex_space_inf {𝕜 : Type u_2} {E : Type u_3} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {t₁ t₂ : topological_space E} (h₁ : locally_convex_space 𝕜 E) (h₂ : locally_convex_space 𝕜 E) :
theorem locally_convex_space_induced {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] [add_comm_monoid F] [module 𝕜 F] {t : topological_space F} [locally_convex_space 𝕜 F] (f : E →ₗ[𝕜] F) :
@[protected, instance]
def pi.locally_convex_space {𝕜 : Type u_2} [ordered_semiring 𝕜] {ι : Type u_1} {X : ι → Type u_3} [Π (i : ι), add_comm_monoid (X i)] [Π (i : ι), topological_space (X i)] [Π (i : ι), module 𝕜 (X i)] [∀ (i : ι), locally_convex_space 𝕜 (X i)] :
locally_convex_space 𝕜 (Π (i : ι), X i)
@[protected, instance]
def prod.locally_convex_space {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] [add_comm_monoid F] [module 𝕜 F] [topological_space E] [topological_space F] [locally_convex_space 𝕜 E] [locally_convex_space 𝕜 F] :
locally_convex_space 𝕜 (E × F)