Locally convex topological modules #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 everywhere
seminorm.locally_convex_space: a topology generated by a family of seminorms is locally convex
normed_space.locally_convex_space: a normed space is locally convex
- define a structure
module_filter_basis, for filter bases generating a locally convex topology
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.
In a locally convex space, if
t are disjoint convex sets,
s is compact and
closed, then we can find open disjoint convex sets containing them.