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.convex_open_basis_zero (π•œ : Type u_1) (E : Type u_2) [linear_ordered_field π•œ] [add_comm_group E] [module π•œ E] [topological_space E] [topological_add_group E] [has_continuous_const_smul π•œ E] [locally_convex_space π•œ E] :
(nhds 0).has_basis (Ξ» (s : set E), 0 ∈ s ∧ is_open s ∧ convex π•œ s) id
theorem disjoint.exists_open_convexes {π•œ : Type u_1} {E : Type u_2} [linear_ordered_field π•œ] [add_comm_group E] [module π•œ E] [topological_space E] [topological_add_group E] [has_continuous_const_smul π•œ E] [locally_convex_space π•œ E] {s t : set E} (disj : disjoint s t) (hs₁ : convex π•œ s) (hsβ‚‚ : is_compact s) (ht₁ : convex π•œ t) (htβ‚‚ : is_closed t) :
βˆƒ (u v : set E), is_open u ∧ is_open 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 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)