Theorems · Theorem · order theory
lt_of_le_not_ge
∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ≤ b → ¬b ≤ a → a < b- Defined in
- Mathlib.Order.Defs.PartialOrder
- Cited by
- 33 results in Mathlib
- Foundations
- Depth 4 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
- lt_iff_le_not_geproof · cited by 35
Cited by33
Results whose statement or proof uses this declaration.
- lt_of_lt_of_leproof · cited by 438
- lt_of_le_of_ltproof · cited by 432
- lt_of_not_geproof · cited by 374
- lt_of_le_of_neproof · cited by 230
- lt_of_le_of_ne'proof · cited by 149
- Filter.Ioi_mem_atTopproof · cited by 36
- LE.le.lt_of_not_geproof · cited by 21
- lt_of_lt_of_le'proof · cited by 15
- lt_of_le_of_lt'proof · cited by 11
- Filter.Iio_mem_atBotproof · cited by 7
- Decidable.lt_or_eq_of_leproof · cited by 6
- Decidable.lt_or_eq_of_le'proof · cited by 5