Structures · Order
NoTopOrder
Order without top elements.
- Defined in
- Mathlib.Order.Max
- Shape
- One type argument · adds exists_not_le
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- OrderDual
- WithBot
How is a type an instance?
Loading the hierarchy index…
Assumed by44
- Filter.eventually_gt_atTop
- Filter.Ioi_mem_atTop
- Filter.eventually_ne_atTop
- Filter.Tendsto.eventually_gt_atTop
- not_tendsto_atTop_of_tendsto_nhds
- Filter.Tendsto.eventually_ne_atTop
- not_tendsto_nhds_of_tendsto_atTop
- NoTopOrder.exists_not_le
- not_isTop
- disjoint_nhds_atTop
- WithTop.eq_top_iff_forall_ge
- NoTopOrder.to_noMaxOrder
- IsGLB.nonempty
- not_bddAbove_univ
- Filter.atTop_le_cofinite
- tendsto_atTop_of_mapClusterPt
- WithTop.eq_of_forall_coe_le_iff
- tendsto_leftLim_atTop_of_tendsto
- WithTop.forall_coe_le_iff_le
- WithBot.eq_top_iff_forall_ge
- Finset.tendsto_Ico_atBot_prod_atTop
- WithTop.forall_le_coe_iff_le
- Filter.disjoint_pure_atTop
- Finset.tendsto_Ioo_neg_atTop_atTop
- Filter.disjoint_atTop_principal_Iic
- NoTopOrder.upperBounds_univ
- Filter.Tendsto.eventually_ne_atTop'
- Order.one_lt_cof
- Finset.tendsto_Ico_neg_atTop_atTop
- Finset.tendsto_Ioo_atBot_prod_atTop
- Filter.not_tendsto_const_atTop
- Set.unbounded_le_univ
- nhds_inf_atTop
- WithTop.eq_of_forall_le_coe_iff
- Order.cof_ne_one
- SummationFilter.instLeAtTopSymmetricIco
- FirstOrder.Language.realize_noTopOrder
- WithBot.noTopOrder
- IsOrderBornology.neBot_cobounded_of_noTopOrder
- inf_nhds_atTop
- FirstOrder.Language.model_dlo
- SummationFilter.instLeAtTopSymmetricIoo
- Set.unbounded_lt_univ
- OrderDual.noBotOrder
Ancestors0
No ancestors.