Mathlib v3 is deprecated. Go to Mathlib v4

Theorem eq.not_gt

Modification history

2022-04-21 12:10
src/order/basic.lean
feat(order/basic): Simple shortcut lemmas (#13421) …
Modified eq.not_gtView on Github →
2022-04-14 06:30
src/order/basic.lean
chore(*): suggestions from the generalisation linter (#13092) …
Modified eq.not_gtView on Github →
2021-10-08 07:33
src/algebra/order/basic.lean
move(order/*): move from `algebra.order.` the files that aren't about algebra (#9562) …
Modified eq.not_gtView on Github →
2021-08-27 08:03
src/algebra/order.lean
refactor(*): use `is_empty` instead of `not (nonempty α)` (#8858) …
Added eq.not_gtView on Github →