Theorems · Theorem · order theory
LT.lt.ne_bot
∀ {α : Type u} [inst : Preorder α] [inst_1 : OrderBot α] {a b : α}, b < a → a ≠ ⊥Alias of ne_bot_of_gt.
- Defined in
- Mathlib.Order.BoundedOrder.Basic
- Cited by
- 26 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.
- Preorderstatement · cited by 7,952
- Bot.botstatement · cited by 4,720
- OrderBotstatement · cited by 1,055
- ne_bot_of_gtproof · cited by 18
Cited by26
Results whose statement or proof uses this declaration.
- Polynomial.ne_zero_of_degree_gtproof · cited by 13
- Ordinal.veblenWith_veblenWith_of_ltproof · cited by 9
- Ordinal.isSuccLimit_of_isPrincipal_addproof · cited by 4
- ENNReal.inv_strictAntiproof · cited by 4
- IsSimpleOrder.eq_top_of_ltproof · cited by 3
- Polynomial.cyclotomic_coeff_zeroproof · cited by 3
- MeasureTheory.exists_isSigmaFiniteSet_measure_geproof · cited by 3
- EReal.left_distrib_of_nonneg_of_ne_topproof · cited by 2
- Nat.frequently_mod_eqproof · cited by 2
- HasFTaylorSeriesUpToOn.compproof · cited by 2
- MeasureTheory.isTightMeasureSet_singleton_of_innerRegularWRTproof · cited by 2
- Ordinal.opow_le_iff_le_log'proof · cited by 2