Structures · Algebra
PredSubOrder
A typeclass for pred x = x - 1.
- Defined in
- Mathlib.Algebra.Order.SuccPred
- Shape
- One type argument · adds pred_eq_sub_one
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- Int
- Nat
How is a type an instance?
Loading the hierarchy index…
Assumed by69
- Order.pred_eq_sub_one
- PredSubOrder.pred_eq_sub_one
- Order.IsPredPrelimit.lt_sub_one
- Set.insert_Ico_left_eq_Ico_sub_one_of_not_isMin
- Order.le_sub_one_iff_of_not_isMin
- Order.sub_one_lt_iff_of_not_isMin
- Finset.insert_Ico_left_eq_Ico_sub_one_of_not_isMin
- Order.IsPredPrelimit.lt_sub_natCast
- strictAnti_of_lt_sub_one
- Finset.Ioc_sub_one_left_eq_Icc
- Set.insert_Icc_left_eq_Icc_sub_one
- Set.Ioc_sub_one_left_eq_Icc_of_not_isMin
- Set.insert_Ico_sub_one_right_eq_Ico
- Set.Icc_add_one_sub_one_eq_Ioo
- Finset.Icc_sub_one_right_eq_Ico
- Order.pred_iterate
- Finset.insert_Ioc_left_eq_Ioc_sub_one_of_not_isMin
- strictAntiOn_of_lt_sub_one
- Set.Ioi_sub_one_eq_Ici
- Set.Iic_sub_one_eq_Iio
- strictMono_of_sub_one_lt
- Set.Iic_sub_one_eq_Iio_of_not_isMin
- Order.IsPredLimit.lt_sub_natCast
- Order.le_of_sub_one_lt
- Finset.insert_Ioc_sub_one_right_eq_Ioc
- Set.Ioc_sub_one_left_eq_Icc
- Set.Ioc_sub_one_sub_one_eq_Ico_of_not_isMin
- Order.covBy_iff_sub_one_eq
- Order.sub_one_lt_iff
- Order.sub_one_wcovBy
- Finset.Ioc_sub_one_sub_one_eq_Ico_of_not_isMin
- Finset.insert_Ioc_left_eq_Ioc_sub_one
- Set.insert_Ioc_sub_one_right_eq_Ioc
- Set.Icc_sub_one_right_eq_Ico_of_not_isMin
- Finset.insert_Ico_left_eq_Ico_sub_one
- antitoneOn_of_le_sub_one
- Finset.insert_Ico_sub_one_right_eq_Ico
- Set.Ioo_sub_one_left_eq_Ioc
- Finset.Ioc_sub_one_left_eq_Icc_of_not_isMin
- Order.IsPredLimit.lt_sub_one
- monotone_of_sub_one_le
- Set.Ioc_sub_one_sub_one_eq_Ico
- Finset.Ioc_sub_one_sub_one_eq_Ico
- Finset.Ioo_sub_one_left_eq_Ioc_of_not_isMin
- Finset.Iic_sub_one_eq_Iio
- Finset.insert_Icc_left_eq_Icc_sub_one
- Set.insert_Ioc_left_eq_Ioc_sub_one_of_not_isMin
- monotoneOn_of_sub_one_le
- Finset.insert_Icc_sub_one_right_eq_Icc
- Finset.Iic_sub_one_eq_Iio_of_not_isMin