Structures · Order
IsSuccArchimedean
A SuccOrder is succ-archimedean if one can go from any two comparable elements by iterating
succ
- Defined in
- Mathlib.Order.SuccPred.Archimedean
- Shape
- One type argument · adds exists_succ_iterate_of_le
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances6
- Int
- Nat
- OrderDual
- Set.Elem
- Multiplicative
- Additive
How is a type an instance?
Loading the hierarchy index…
Assumed by98
- toZ
- IsSuccArchimedean.exists_succ_iterate_of_le
- reflTransGen_of_succ
- toZ_of_ge
- reflTransGen_of_succ_of_le
- strictMonoOn_of_lt_succ
- LE.le.exists_succ_iterate
- toZ_of_lt
- StrictMonoOn.Iic_id_le
- monotoneOn_of_le_succ
- iterate_pred_toZ
- strictMonoOn_Iic_of_lt_succ
- toZ_le_toZ
- reflTransGen_of_succ_of_ge
- strictMonoOn_of_lt_add_one
- toZ_strictMono
- transGen_of_succ_of_ne
- Order.IsSuccPrelimit.isMin
- Order.IsSuccPrelimit.isMin_of_noMax
- antitoneOn_of_succ_le
- toZ_of_eq
- strictAntiOn_of_succ_lt
- transGen_of_succ_of_refl
- StrictMono.not_bddAbove_range_of_isSuccArchimedean
- iterate_succ_toZ
- Succ.rec_iff
- transGen_of_succ_of_gt
- strictAntiOn_Iic_of_succ_lt
- SuccOrder.forall_ne_bot_iff
- injective_toZ
- toZ_neg
- strictMono_of_lt_succ
- toZ_iterate_succ_of_not_isMax
- strictAntiOn_of_add_one_lt
- toZ_nonneg
- Succ.rec_bot
- antitone_of_succ_le
- biUnion_Ici_Ioc_map_succ
- toZ_iterate_pred_of_not_isMin
- monotone_of_le_succ
- Order.isSuccPrelimit_iff_isMin
- toZ_lt_toZ
- biUnion_Ici_Ico_map_succ
- strictAnti_of_succ_lt
- IsPreconnected.biUnion_of_chain
- Order.not_isSuccLimit_of_isSuccArchimedean
- SimpleGraph.hasse_preconnected_of_succ
- le_total_of_codirected
- transGen_of_succ_of_lt
- Order.not_isSuccPrelimit_of_isSuccArchimedean
Ancestors0
No ancestors.