Structures · Order
IsPredArchimedean
A PredOrder is pred-archimedean if one can go from any two comparable elements by iterating
pred
- Defined in
- Mathlib.Order.SuccPred.Archimedean
- Shape
- One type argument · adds exists_pred_iterate_of_le
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances7
- Int
- Nat
- RootedTree.α
- OrderDual
- Set.Elem
- Multiplicative
- Additive
How is a type an instance?
Loading the hierarchy index…
Assumed by69
- IsPredArchimedean.exists_pred_iterate_of_le
- IsPredArchimedean.findAtom
- LE.le.exists_pred_iterate
- strictMonoOn_of_pred_lt
- monotoneOn_of_pred_le
- IsPredArchimedean.findAtom_bot
- Order.IsPredPrelimit.isMax
- IsPredArchimedean.findAtom.congr_simp
- antitoneOn_of_le_pred
- le_total_of_directed
- Order.isPredPrelimit_iff_isMax
- Order.IsPredPrelimit.isMax_of_noMin
- strictAntiOn_of_lt_pred
- lt_or_le_of_directed
- Order.not_isPredLimit_of_isPredArchimedean
- monotone_of_pred_le
- Pred.rec_iff
- Order.not_isPredPrelimit_of_isPredArchimedean
- Order.isPredPrelimit_iff_of_noMin
- strictAnti_of_lt_pred
- IsPredArchimedean.pred_findAtom
- transGen_of_pred_of_refl
- IsPredArchimedean.isAtom_findAtom
- antitone_of_le_pred
- StrictMono.not_bddBelow_range_of_isPredArchimedean
- strictMono_of_pred_lt
- reflTransGen_of_pred
- IsPredArchimedean.findAtom_eq_bot
- Order.not_isPredLimit_of_noMin
- instIsPredArchimedeanAdditive
- strictAnti_of_lt_sub_one
- Pred.rec_linear
- Set.OrdConnected.isPredArchimedean
- transGen_of_pred_of_lt
- strictAntiOn_of_lt_sub_one
- strictMono_of_sub_one_lt
- BddBelow.exists_isLeast_of_nonempty
- transGen_of_pred_of_gt
- IsPredArchimedean.findAtom_le
- instIsSuccArchimedeanOrderDualOfIsPredArchimedean
- IsPredArchimedean.isAtom_findAtom_iff
- exists_pred_iterate_or
- Order.not_isPredLimit
- strictMonoOn_Ici_of_pred_lt
- Pred.rec_top
- transGen_of_pred_of_reflexive
- IsPredArchimedean.instIsAtomic
- IsPredArchimedean.findAtom_ne_bot
- antitoneOn_of_le_sub_one
- SimpleGraph.hasse_preconnected_of_pred
Ancestors0
No ancestors.