Structures · Topology
SSet.Subcomplex.PairingCore.IsProper
The condition that h : A.PairingCore is proper, i.e. for each s : h.ι,
the type (II) simplex h.type₂ s is uniquely a 1-codimensional
face of the type (I) simplex h.type₁ s.
- Shape
- One type argument · adds isUniquelyCodimOneFace
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Forgetful instances
Provided automatically by
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 by10
- SSet.Subcomplex.PairingCore.isUniquelyCodimOneFace
- SSet.Subcomplex.PairingCore.isUniquelyCodimOneFace_index
- SSet.Subcomplex.PairingCore.IsProper.isUniquelyCodimOneFace
- SSet.Subcomplex.PairingCore.isRegular_iff_nonempty_rankFunction
- SSet.Subcomplex.PairingCore.isUniquelyCodimOneFace_index_coe
- SSet.Subcomplex.PairingCore.isRegular_iff_nonempty_weakRankFunction
- SSet.Subcomplex.PairingCore.RankFunction.isRegular
- SSet.Subcomplex.PairingCore.instIsProperPairingOfIsProper
- SSet.Subcomplex.PairingCore.WeakRankFunction.isRegular
- SSet.Subcomplex.PairingCore.instIsInnerPairingOfIsInner
Ancestors0
No ancestors.