Topology induced by a family of seminorms #
Main definitions #
Main statements #
Show that for any locally convex space there exist seminorms that induce the topology.
seminorm, locally convex
An abbreviation for indexed families of seminorms. This is mainly to allow for dot-notation.
The sets of a filter basis for the neighborhood filter of 0.
module_filter_basis induced by the filter basis
The proposition that a linear map is bounded between spaces with families of seminorms.
The proposition that the topology of
E is induced by a family of seminorms
Instances of this typeclass
normed_space.to_locally_convex_space' for a slightly stronger version which is not an
The family of seminorms obtained by composing each seminorm by a linear map.