Structures · Topology
IsUltraUniformity
A uniform space is ultrametric if the uniformity 𝓤 X has a basis of equivalence relations.
- Shape
- One type argument · adds hasBasis
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances4
- SeparationQuotient
- UniformSpace.Completion
- CauchyFilter
- Prod
How is a type an instance?
Loading the hierarchy index…
Assumed by10
- IsUltraUniformity.hasBasis
- IsUniformInducing.isUltraUniformity
- UniformSpace.nhds_basis_clopens
- IsUltraUniformity.cauchyFilter
- TopologicalSpace.isTopologicalBasis_clopens
- IsUltraUniformity.prod
- IsUltraUniformity.mem_nhds_iff_symm_trans
- IsUltraUniformity.completion
- IsUltraUniformity.pi
- IsUltraUniformity.separationQuotient
Ancestors0
No ancestors.