Structures · Topology
SSet.HasDimensionLT
A simplicial set X has dimension < d iff for any n : ℕ
such that d ≤ n, all n-simplices are degenerate.
- Shape
- 2 explicit arguments · adds degenerate_eq_top
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- CategoryTheory.MonoidalCategoryStruct.tensorObj
- SSet.Subcomplex.toSSet
How is a type an instance?
Loading the hierarchy index…
Assumed by23
- SSet.dim_lt_of_nonDegenerate
- SSet.degenerate_eq_univ_of_hasDimensionLT
- SSet.nonDegenerate_eq_empty_of_hasDimensionLT
- SSet.PtSimplex.comp_map_eq_const
- SSet.finite_of_hasDimensionLT
- SSet.hasDimensionLT_of_mono
- SSet.hasDimensionLT_of_epi
- SSet.hasDimensionLT_of_le
- SSet.hasDimensionLT_prod
- SSet.HasDimensionLT.degenerate_eq_top
- SSet.exactAt_chainComplex_of_hasDimensionLT
- SSet.isZero_normalizedChainComplex_X_of_hasDimensionLT
- SSet.Subcomplex.le_iff_of_hasDimensionLT
- SSet.Subcomplex.instHasDimensionLTToSSet
- SSet.degenerate_eq_top_of_hasDimensionLT
- SSet.isZero_homology_of_hasDimensionLT
- SSet.instHasDimensionLTHAddNat
- SSet.instHasDimensionLTToSSetRange
- SSet.instHasDimensionLTTensorObjHAddNat
- SSet.nonDegenerate_eq_bot_of_hasDimensionLT
- SSet.Subcomplex.eq_top_iff_of_hasDimensionLT
- SSet.Subcomplex.hasDimensionLT_of_le
- SSet.PtSimplex.comp_map_eq_const_assoc
Ancestors0
No ancestors.