Structures · Topology
DiscreteUniformity
The discrete uniformity
- Shape
- One type argument · adds eq_bot
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances5
- TopologicalSpace.NonemptyCompacts
- TopologicalSpace.Compacts
- TopologicalSpace.Closeds
- Prod
- Set
How is a type an instance?
Loading the hierarchy index…
Assumed by30
- MvPowerSeries.substAlgHom_eq_aeval
- IsUniformEmbedding.discreteUniformity
- DiscreteUniformity.eq_bot
- DiscreteUniformity.eq_principal_setRelId
- MvPowerSeries.subst_eq_eval₂
- MvPowerSeries.continuous_subst
- PowerSeries.substAlgHom_eq_aeval
- DiscreteUniformity.cauchyConst
- DiscreteUniformity.eq_pure_of_cauchy
- DiscreteUniformity.eq_pure_cauchyConst
- MvPowerSeries.comp_subst
- MvPowerSeries.comp_substAlgHom
- MvPowerSeries.comp_subst_apply
- DiscreteUniformity.instProd
- instIsUniformGroupOfDiscreteUniformity
- TopologicalSpace.Compacts.instDiscreteUniformity
- PowerSeries.subst_tsum
- MvPowerSeries.summable_subst
- MvPowerSeries.subst_tsum
- UniformSpace.hausdorff.instDiscreteUniformitySet
- DiscreteUniformity.instCompleteSpace
- DiscreteUniformity.uniformContinuous
- MvPowerSeries.eval₂_subst
- TopologicalSpace.Closeds.instDiscreteUniformity
- DiscreteUniformity.instDiscreteTopology
- IsUltraUniformity.bot
- instIsUniformAddGroupOfDiscreteUniformity
- TopologicalSpace.NonemptyCompacts.instDiscreteUniformity
- PowerSeries.summable_subst
- DiscreteUniformity.relId_mem_uniformity
Ancestors0
No ancestors.