Topology induced by a family of seminorms #
Main definitions #
seminorm_family.basis_sets
: The set of open seminorm balls for a family of seminorms.seminorm_family.module_filter_basis
: A module filter basis formed by the open balls.seminorm.is_bounded
: A linear mapf : E ββ[π] F
is bounded iff every seminorm inF
can be bounded by a finite number of seminorms inE
.
Main statements #
continuous_from_bounded
: A bounded linear mapf : E ββ[π] F
is continuous.seminorm_family.to_locally_convex_space
: A space equipped with a family of seminorms is locally convex.
TODO #
Show that for any locally convex space there exist seminorms that induce the topology.
Tags #
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.
The add_group_filter_basis
induced by the filter basis seminorm_basis_zero
.
Equations
- p.add_group_filter_basis = add_group_filter_basis_of_comm p.basis_sets _ _ _ _ _
The module_filter_basis
induced by the filter basis seminorm_basis_zero
.
Equations
- p.module_filter_basis = {to_add_group_filter_basis := p.add_group_filter_basis _inst_4, smul' := _, smul_left' := _, smul_right' := _}
The proposition that a linear map is bounded between spaces with families of seminorms.
- topology_eq_with_seminorms : t = p.module_filter_basis.topology
The proposition that the topology of E
is induced by a family of seminorms p
.
Instances of this typeclass
The topology of a normed_space π E
is induced by the seminorm norm_seminorm π E
.
Not an instance since π
can't be inferred. See normed_space.to_locally_convex_space
for a
slightly weaker instance version.
See normed_space.to_locally_convex_space'
for a slightly stronger version which is not an
instance.
The family of seminorms obtained by composing each seminorm by a linear map.