Theorems · Theorem · order theory
not_lt_of_ge
∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ≤ b → ¬b < a- Defined in
- Mathlib.Order.Defs.PartialOrder
- Cited by
- 52 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
- Assumes
- Preorder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Preorderstatement and proof · cited by 7,952
- not_le_of_gtproof · cited by 97
Cited by52
Results whose statement or proof uses this declaration.
- not_ltproof · cited by 306
- LE.le.not_gtproof · cited by 189
- Polynomial.modByMonic_eq_zero_iff_dvdproof · cited by 15
- Nat.finiteMultiplicity_iffproof · cited by 13
- CauSeq.le_of_existsproof · cited by 9
- isLUB_Iooproof · cited by 7
- isGLB_Iooproof · cited by 5
- MvPowerSeries.mul_invOfUnitproof · cited by 4
- Set.pi_univ_Iio_subsetproof · cited by 3
- Set.pi_univ_Ioi_subsetproof · cited by 3
- Filter.IsCobounded.frequently_geproof · cited by 3
- Filter.IsCobounded.frequently_leproof · cited by 3