Structures · Order
PredOrder
Order equipped with a sensible predecessor function.
- Defined in
- Mathlib.Order.SuccPred.Basic
- Shape
- One type argument · adds pred, pred_le, min_of_le_pred, le_pred_of_lt
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances11
- Int
- Nat
- RootedTree.α
- OrderDual
- Set.Elem
- Fin
- Shrink
- WithTop
- WithBot
- Multiplicative
- Additive
How is a type an instance?
Loading the hierarchy index…
Assumed by361
- Order.pred
- toZ
- Order.pred_le
- Order.le_pred_of_lt
- Order.le_pred_iff_of_not_isMin
- Order.pred_lt_iff_of_not_isMin
- Order.pred_lt_of_not_isMin
- Order.pred_covBy_of_not_isMin
- Order.pred_eq_iff_isMin
- CovBy.pred_eq
- WithTop.pred
- PredOrder.pred
- IsPredArchimedean.findAtom
- Order.IsPredPrelimit.isMin
- IsMin.pred_eq
- Order.pred_iterate_le
- LE.le.exists_pred_iterate
- toZ_of_ge
- Order.pred_le_pred
- PredOrder.prelimitRecOn
- Set.Ioo_pred_left_eq_Ioc_of_not_isMin
- Order.IsPredPrelimit.lt_pred
- Set.Icc_pred_right_eq_Ico_of_not_isMin
- PredOrder.colimitRecOn
- Order.pred_covBy
- Order.pred_lt_iff
- Order.pred_lt_of_le_of_not_isMin
- PredOrder.hasBasis_nhds_Ico_of_exists_gt
- Order.isPredLimitRecOn
- toZ_of_lt
- Order.pred_lt_iff_not_isMin
- strictMonoOn_of_pred_lt
- Set.Ioc_pred_right_eq_Ioo
- Set.Ioc_pred_pred_eq_Ico_of_not_isMin
- PredOrder.nhdsLT
- iterate_pred_toZ
- Set.insert_Ioc_left_eq_Ioc_pred_of_not_isMin
- Set.Ioi_pred_eq_Ici_of_not_isMin
- Order.pred_bot
- Order.min_of_le_pred
- Order.pred_le_iff_eq_or_le
- Order.le_pred_iff_isMin
- Order.IsPredPrelimit.pred_ne
- Set.Iic_pred_eq_Iio_of_not_isMin
- Order.Iic_pred_of_not_isMin
- Order.isPredPrelimitRecOn
- monotoneOn_of_pred_le
- toZ_le_toZ
- Order.not_isPredPrelimit_iff_pred_eq
- Order.pred_eq_pred_iff_of_not_isMin
Ancestors0
No ancestors.