Theorems · Theorem · order theory
Order.pred_eq_sub_one
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : Sub α] [inst_2 : One α] [inst_3 : PredSubOrder α] (x : α),
Order.pred x = x - 1- Defined in
- Mathlib.Algebra.Order.SuccPred
- Cited by
- 59 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
- Assumes
- PreorderSubOnePredSubOrder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Preorderstatement and proof · cited by 7,952
- Order.predstatement · cited by 273
- PredSubOrderstatement and proof · cited by 68
- PredSubOrder.pred_eq_sub_oneproof · cited by 1
Cited by59
Results whose statement or proof uses this declaration.
- Order.sub_one_lt_iff_of_not_isMinproof · cited by 1
- Set.insert_Ico_left_eq_Ico_sub_one_of_not_isMinproof · cited by 1
- Order.IsPredPrelimit.lt_sub_oneproof · cited by 1
- Order.le_sub_one_iff_of_not_isMinproof · cited by 1
- Finset.insert_Ico_left_eq_Ico_sub_one_of_not_isMinproof · cited by 1
- Finset.insert_Ico_sub_one_right_eq_Icoproof · cited by 0
- Finset.insert_Ioc_left_eq_Ioc_sub_oneproof · cited by 0
- Finset.insert_Ioc_left_eq_Ioc_sub_one_of_not_isMinproof · cited by 0
- Order.sub_one_covByproof · cited by 0
- Order.sub_one_wcovByproof · cited by 0
- Finset.insert_Ioc_sub_one_right_eq_Iocproof · cited by 0
- Finset.Ioc_sub_one_left_eq_Iccproof · cited by 0