Theorems · Inductive type · order theory
IsPredArchimedean
(α : Type u_3) → [inst : Preorder α] → [PredOrder α] → Prop
A PredOrder is pred-archimedean if one can go from any two comparable elements by iterating
pred
- Defined in
- Mathlib.Order.SuccPred.Archimedean
- Cited by
- 66 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by75
Results whose statement or proof uses this declaration.
- IsPredArchimedean.exists_pred_iterate_of_lestatement and proof · cited by 11
- IsPredArchimedean.findAtomstatement and proof · cited by 8
- LE.le.exists_pred_iteratestatement and proof · cited by 6
- Pred.recstatement and proof · cited by 4
- strictMonoOn_of_pred_ltstatement and proof · cited by 3
- monotoneOn_of_pred_lestatement and proof · cited by 3
- Order.isPredPrelimit_iff_isMaxstatement and proof · cited by 2
- antitoneOn_of_le_predstatement and proof · cited by 2
- IsPredArchimedean.findAtom_botstatement and proof · cited by 2
- le_total_of_directedstatement and proof · cited by 2
- IsPredArchimedean.findAtom.congr_simpstatement and proof · cited by 2
- Order.IsPredPrelimit.isMaxstatement and proof · cited by 2