Theorems · Theorem · order theory
LT.lt.ne_top
∀ {α : Type u} [inst : Preorder α] [inst_1 : OrderTop α] {a b : α}, a < b → a ≠ ⊤Alias of ne_top_of_lt.
- Defined in
- Mathlib.Order.BoundedOrder.Basic
- Cited by
- 34 results in Mathlib
- Foundations
- Depth 9 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Top.topstatement · cited by 9,680
- Preorderstatement · cited by 7,952
- OrderTopstatement · cited by 493
- ne_top_of_ltproof · cited by 50
Cited by34
Results whose statement or proof uses this declaration.
- EReal.add_lt_addproof · cited by 12
- ENNReal.sub_mulproof · cited by 8
- ENNReal.inv_strictAntiproof · cited by 4
- HahnSeries.orderTop_add_eq_leftproof · cited by 4
- meromorphicOrderAt_add_eq_left_of_ltproof · cited by 3
- ENNReal.lt_iff_exists_add_pos_ltproof · cited by 3
- HahnSeries.leadingCoeff_add_eq_leftproof · cited by 3
- meromorphicNFAt_iff_analyticAt_orproof · cited by 3
- tendsto_cobounded_of_meromorphicOrderAt_negproof · cited by 3
- ENNReal.toReal_lt_of_lt_ofRealproof · cited by 3
- ENNReal.le_mul_of_forall_ltproof · cited by 2
- IsSimpleOrder.eq_bot_of_ltproof · cited by 2