Mathlib Map

Theorems · Inductive type · order theory

NoTopOrder

(α : Type u_3) → [LE α] → Prop

Order without top elements.

Defined in
Mathlib.Order.Max
Cited by
50 results in Mathlib
Foundations
Depth 1 from the axioms · uses no axioms
Assumes
LE
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Filter.eventually_gt_atTop · cited by 90Filter.eventually_gt_atTopFilter.Ioi_mem_atTop · cited by 36Filter.Ioi_mem_atTopFilter.eventually_ne_atTop · cited by 35Filter.eventually_ne_atTopFilter.Tendsto.eventually_gt_atTop · cited by 11Tendsto.eventually_gt_atT…not_tendsto_atTop_of_tendsto_nhds · cited by 9not_tendsto_atTop_of_tend…Filter.Tendsto.eventually_ne_atTop · cited by 9Tendsto.eventually_ne_atT…not_tendsto_nhds_of_tendsto_atTop · cited by 7not_tendsto_nhds_of_tends…NoTopOrder.exists_not_le · cited by 5NoTopOrder.exists_not_lenot_isTop · cited by 5not_isTopdisjoint_nhds_atTop · cited by 4disjoint_nhds_atToptopOrderOrNoTopOrder · cited by 4topOrderOrNoTopOrderNoTopOrder.to_noMaxOrder · cited by 3NoTopOrder.to_noMaxOrderIsClub.sInter_of_cof_le_one · cited by 3IsClub.sInter_of_cof_le_o…Filter.atTop_le_cofinite · cited by 3Filter.atTop_le_cofinitetendsto_atTop_of_mapClusterPt · cited by 3tendsto_atTop_of_mapClust…NoTopOrderCITED BYCITES

Cites0

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Nothing in Mathlib beyond the foundations.

Cited by53

Results whose statement or proof uses this declaration.