Structures · Algebra
SuccAddOrder
A typeclass for succ x = x + 1.
- Defined in
- Mathlib.Algebra.Order.SuccPred
- Shape
- One type argument · adds succ_eq_add_one
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances5
- Int
- Nat
- ENat
- PNat
- Ordinal
How is a type an instance?
Loading the hierarchy index…
Assumed by109
- Order.succ_eq_add_one
- Order.one_le_iff_ne_zero
- Order.one_le_iff_pos
- Order.lt_one_iff
- Order.lt_add_one_iff
- Order.add_one_le_of_lt
- Order.le_one_iff
- Finset.Ico_add_one_right_eq_Icc
- Order.add_one_le_iff
- Finset.insert_Ico_right_eq_Ico_add_one
- Order.lt_two_iff
- WithBot.succ_natCast
- Finset.insert_Ico_add_one_left_eq_Ico
- Order.le_of_lt_add_one
- Finset.Icc_add_one_left_eq_Ioc
- Order.add_one_le_iff_of_not_isMax
- strictMonoOn_of_lt_add_one
- partialSups_add_one
- Order.lt_one_iff_nonpos
- Finset.prod_Iio_add_one_comm
- Order.lt_add_one_iff_of_not_isMax
- Order.IsSuccLimit.add_natCast_lt
- Order.IsSuccLimit.add_one_lt
- Finset.sum_Iio_add_zero_comm
- Order.IsSuccPrelimit.add_one_lt
- Finset.Iio_add_one_eq_Iic
- WithBot.one_le_iff_pos
- Order.covBy_iff_add_one_eq
- Set.insert_Ioc_right_eq_Ioc_add_one_of_not_isMax
- Order.le_two_iff
- Monotone.disjointed_add_one_sup
- Finset.Ico_add_one_add_one_eq_Ioc
- Finset.prod_Iic_add_one_comm
- strictAntiOn_of_add_one_lt
- Finset.insert_Ioc_right_eq_Ioc_add_one_of_not_isMax
- Finset.sum_Iic_add_zero_comm
- Order.succ_iterate
- Finset.prod_Ico_mul_eq_prod_Ico_add_one
- Order.IsSuccPrelimit.add_natCast_lt
- Order.IsSuccLimit.natCast_lt
- Monotone.disjointed_add_one
- SuccAddOrder.succ_eq_add_one
- Order.add_one_le_iff_of_not_isMax'
- Order.lt_add_one_iff_of_not_isMax'
- Set.insert_Ioc_add_one_left_eq_Ioc
- Set.Icc_add_one_sub_one_eq_Ioo
- Order.add_one_inj
- Set.Ico_add_one_right_eq_Icc_of_not_isMax
- Set.Ioo_add_one_right_eq_Ioc
- Finset.Ioo_add_one_right_eq_Ioc