Structures · Order
SuccOrder
Order equipped with a sensible successor function.
- Defined in
- Mathlib.Order.SuccPred.Basic
- Shape
- One type argument · adds succ, le_succ, max_of_succ_le, succ_le_of_lt
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances15
- Int
- Nat
- ENat
- PNat
- Ordinal
- Cardinal
- Ordinal.ToType
- OrderDual
- Set.Elem
- Fin
- Shrink
- WithTop
- WithBot
- Multiplicative
- Additive
How is a type an instance?
Loading the hierarchy index…
Assumed by664
- Order.succ
- Order.le_succ
- CategoryTheory.TransfiniteCompositionOfShape.F
- Order.lt_succ
- Order.succ_le_of_lt
- WithBot.succ
- Order.lt_succ_of_not_isMax
- CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape
- CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape
- toZ
- CategoryTheory.SmallObject.SuccStruct.Iteration.F
- CategoryTheory.TransfiniteCompositionOfShape.incl
- Order.lt_succ_iff
- Order.succ_le_iff
- HomotopicalAlgebra.ReedyStructure.deg
- Order.IsSuccLimit.succ_lt
- Order.lt_succ_iff_of_not_isMax
- HomotopicalAlgebra.RelativeCellComplex.toTransfiniteCompositionOfShape
- Order.succ_le_iff_of_not_isMax
- HomotopicalAlgebra.RelativeCellComplex.attachCells
- SuccOrder.limitRecOn
- CategoryTheory.TransfiniteCompositionOfShape.isoBot
- transfiniteIterate
- SSet.Subcomplex.Pairing.RankFunction.b
- SuccOrder.succ
- HomotopicalAlgebra.ReedyStructure.degHom
- CategoryTheory.SmallObject.SuccStruct.iterationFunctor
- Order.succ_eq_iff_isMax
- CategoryTheory.SmallObject.SuccStruct.extendToSucc
- SSet.Subcomplex.Pairing.RankFunction.Cell.mapToSucc
- Order.le_of_lt_succ
- CategoryTheory.SmallObject.SuccStruct.arrowSucc
- CovBy.succ_eq
- CategoryTheory.Functor.WellOrderInductionData.Extension.val
- Order.covBy_succ_of_not_isMax
- CategoryTheory.Functor.WellOrderInductionData.lift
- CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_le
- CategoryTheory.TransfiniteCompositionOfShape.isColimit
- Order.IsSuccPrelimit.isMax
- Order.IsSuccPrelimit.succ_lt
- CategoryTheory.SmallObject.SuccStruct.extendToSucc.obj
- IsMax.succ_eq
- CategoryTheory.Functor.WellOrderInductionData.succ
- CategoryTheory.SmallObject.SuccStruct.Iteration.mapObj
- Order.succ_le_succ
- SuccOrder.prelimitRecOn
- reflTransGen_of_succ
- CategoryTheory.SmallObject.SuccStruct.extendToSuccObjIso
- Order.max_of_succ_le
- HomotopicalAlgebra.RelativeCellComplex.Cells.j
Ancestors0
No ancestors.