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
@[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)) :
locally_convex_space π E
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)) :
locally_convex_space π E
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.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] :
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) :
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) :
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) :
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) :
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) :
locally_convex_space π E
@[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)