Theorems · Theorem · order theory
IsPredArchimedean.exists_pred_iterate_of_le
∀ {α : Type u_3} {inst : Preorder α} {inst_1 : PredOrder α} [self : IsPredArchimedean α] {a b : α},
a ≤ b → ∃ n, Order.pred^[n] b = aIf a ≤ b then one can get to b from a by iterating pred
- Defined in
- Mathlib.Order.SuccPred.Archimedean
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses no axioms
- Assumes
- IsPredArchimedean
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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
- Nat.iteratestatement · cited by 740
- PredOrderstatement and proof · cited by 334
- Order.predstatement · cited by 273
- IsPredArchimedeanstatement and proof · cited by 66
Cited by11
Results whose statement or proof uses this declaration.
- LE.le.exists_pred_iterateproof · cited by 6
- toZ_of_ltstatement · cited by 4
- iterate_pred_toZproof · cited by 3
- strictMonoOn_of_pred_ltproof · cited by 3
- monotoneOn_of_pred_leproof · cited by 3
- toZ_iterate_pred_of_not_isMinproof · cited by 1
- toZ_iterate_pred_geproof · cited by 0
- IsPredArchimedean.of_orderIsoproof · cited by 0
- PredOrder.forall_ne_top_iffproof · cited by 0
- exists_pred_iterate_iff_leproof · cited by 0
- exists_pred_iterate_orproof · cited by 0