Structures Β· Analysis
PolynormableSpace
A topological vector space E is polynormable over π if its topology is induced by
some family of π-seminorms. Equivalently, its topology is induced by all its continuous
seminorm.
If π is RCLike, this is equivalent to LocallyConvexSpace π E.
- Shape
- 2 explicit arguments Β· adds withSeminorms'
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy indexβ¦
Assumed by16
- PolynormableSpace.withSeminorms
- Module.Dual.exists_continuous_extension_of_le_seminorm
- PolynormableSpace.withSeminorms'
- StrongDual.exists_extension
- ContinuousLinearMap.exist_extension_of_finiteDimensional_range
- Seminorm.exists_le_comp_of_isInducing
- Module.Dual.exists_continuous_extension_of_le_seminorm_real
- PolynormableSpace.banach_steinhaus
- continuousLinearMapOfTendsto
- Submodule.ClosedComplemented.of_finiteDimensional
- Topology.IsInducing.polynormableSpace
- instLocallyConvexSpaceRealOfPolynormableSpace
- instPolynormableSpaceSubtypeMemSubmodule
- instPolynormableSpaceForall
- PolynormableSpace.induced
- instPolynormableSpaceProd
Ancestors0
No ancestors.