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 #
locally_convex_space_iff_zero: in a module, local convexity at zero gives local convexity everywhereseminorm.locally_convex_space: a topology generated by a family of seminorms is locally convexnormed_space.locally_convex_space: a normed space is locally convex
TODO #
- define a structure
locally_convex_filter_basis, extendingmodule_filter_basis, for filter bases generating a locally convex topology - show that any locally convex topology is generated by a family of seminorms
@[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.
theorem
locally_convex_space_iff
(𝕜 : Type u_1)
(E : Type u_2)
[ordered_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
[topological_space E] :
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] :
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] :
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] :
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] :
@[protected, instance]
def
locally_convex_space.to_locally_connected_space
(E : Type u_2)
[add_comm_group E]
[topological_space E]
[topological_add_group E]
[module ℝ E]
[has_continuous_smul ℝ E]
[locally_convex_space ℝ E] :
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)