Theorems · Inductive type · order theory
IsSuccArchimedean
(α : Type u_3) → [inst : Preorder α] → [SuccOrder α] → Prop
A SuccOrder is succ-archimedean if one can go from any two comparable elements by iterating
succ
- Defined in
- Mathlib.Order.SuccPred.Archimedean
- Cited by
- 88 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 by96
Results whose statement or proof uses this declaration.
- toZstatement and proof · cited by 23
- IsSuccArchimedean.exists_succ_iterate_of_lestatement and proof · cited by 12
- Succ.recstatement and proof · cited by 10
- reflTransGen_of_succstatement and proof · cited by 6
- toZ_of_gestatement and proof · cited by 5
- LE.le.exists_succ_iteratestatement and proof · cited by 4
- strictMonoOn_of_lt_succstatement and proof · cited by 4
- reflTransGen_of_succ_of_lestatement and proof · cited by 4
- toZ_of_ltstatement and proof · cited by 4
- monotoneOn_of_le_succstatement and proof · cited by 3
- strictMonoOn_Iic_of_lt_succstatement and proof · cited by 3
- strictMonoOn_of_lt_add_onestatement and proof · cited by 3