Theorems · Inductive type · order theory
PredSubOrder
(α : Type u_1) → [Preorder α] → [Sub α] → [One α] → Type u_1
A typeclass for pred x = x - 1.
- Defined in
- Mathlib.Algebra.Order.SuccPred
- Cited by
- 68 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Preorderstatement · cited by 7,952
Cited by74
Results whose statement or proof uses this declaration.
- Order.pred_eq_sub_onestatement and proof · cited by 59
- Order.sub_one_lt_iff_of_not_isMinstatement and proof · cited by 1
- Order.le_sub_one_iff_of_not_isMinstatement and proof · cited by 1
- Finset.insert_Ico_left_eq_Ico_sub_one_of_not_isMinstatement and proof · cited by 1
- PredSubOrder.pred_eq_sub_onestatement and proof · cited by 1
- Set.insert_Ico_left_eq_Ico_sub_one_of_not_isMinstatement and proof · cited by 1
- Order.IsPredPrelimit.lt_sub_natCaststatement and proof · cited by 1
- Order.IsPredPrelimit.lt_sub_onestatement and proof · cited by 1
- Order.sub_one_covBystatement and proof · cited by 0
- Order.sub_one_lt_iffstatement and proof · cited by 0
- Order.sub_one_wcovBystatement and proof · cited by 0
- strictMonoOn_of_sub_one_ltstatement and proof · cited by 0