Structures · Order
NoMaxOrder
Order without maximal elements. Sometimes called cofinal.
- Defined in
- Mathlib.Order.Max
- Shape
- One type argument · adds exists_gt
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances12
- Nat
- PNat
- Ordinal
- Cardinal
- Subtype
- Prod
- OrderDual
- Set.Elem
- Lex
- WithBot
- Colex
- Sum
How is a type an instance?
Loading the hierarchy index…
Assumed by364
- NoMaxOrder.exists_gt
- not_isMax
- Order.lt_succ
- interior_Icc
- Order.lt_succ_iff
- Order.succ_le_iff
- exists_seq_strictAnti_tendsto
- SSet.Subcomplex.Pairing.RankFunction.b
- Order.lt_add_one_iff
- mem_nhds_iff_exists_Ioo_subset
- closure_Ioi
- Set.nonempty_Ioi
- Finset.Ico_add_one_right_eq_Icc
- interior_Ioc
- Filter.atTop_basis_Ioi
- SSet.Subcomplex.Pairing.RankFunction.Cell.mapToSucc
- nhdsGT_basis
- Order.add_one_le_iff
- Finset.insert_Ico_right_eq_Ico_add_one
- cocompact_eq_atBot_atTop
- interior_Iic
- Order.covBy_succ
- Set.Ioi_infinite
- IsOrderBornology.cobounded_eq
- Order.lt_two_iff
- SSet.Subcomplex.Pairing.RankFunction.mapN
- atTop_le_cocompact
- Nat.exists_strictMono'
- Order.not_isSuccPrelimit_iff_mem_range_succ
- Order.coheight_of_noMaxOrder
- Order.succ_le_succ_iff
- Order.Iio_succ
- nhds_basis_Ioo_pos
- Filter.not_isBoundedUnder_of_tendsto_atTop
- IsOrderBornology.atTop_le_cobounded
- Filter.exists_lt_of_tendsto_atTop
- csInf_Ioi
- SSet.Subcomplex.Pairing.RankFunction.w
- frontier_Iic
- Order.IsSuccPrelimit.succ_ne
- Order.succ_eq_iff_covBy
- SuccOrder.nhds_eq_pure
- Finset.Icc_add_one_left_eq_Ioc
- SuccOrder.isOpen_singleton_iff
- SSet.Subcomplex.Pairing.RankFunction.Cell.ι_b
- mem_nhdsGT_iff_exists_Ioo_subset
- locallyFinite_Icc_of_tendsto
- Order.krullDim_of_noMaxOrder
- SSet.Subcomplex.Pairing.RankFunction.Cell.ι_b_app_apply
- ProbabilityTheory.Kernel.indep_limsup_atTop_self
Ancestors0
No ancestors.