Skip to content

Commit

Permalink
fix(algebra/order): update to lean
Browse files Browse the repository at this point in the history
The new `not_lt_of_lt` in core is not substitutable for this one because it is in the new algebraic hierarchy and mathlib is still on the old one. But this isn't used anywhere, so I'll just remove it instead of renaming.
  • Loading branch information
digama0 committed Nov 20, 2017
1 parent f467c81 commit 40d2b50
Showing 1 changed file with 0 additions and 3 deletions.
3 changes: 0 additions & 3 deletions algebra/order.lean
Expand Up @@ -12,9 +12,6 @@ lemma not_le_of_lt [preorder α] {a b : α} (h : a < b) : ¬ b ≤ a :=

lemma not_lt_of_le [preorder α] {a b : α} (h : a ≤ b) : ¬ b < a
| hab := not_le_of_gt hab h

lemma not_lt_of_lt [linear_order α] {a b : α} (h : a < b) : ¬ b < a :=
lt_asymm h

lemma le_iff_eq_or_lt [partial_order α] {a b : α} : a ≤ b ↔ a = b ∨ a < b :=
le_iff_lt_or_eq.trans or.comm
Expand Down

0 comments on commit 40d2b50

Please sign in to comment.