Mathlib v3 is deprecated. Go to Mathlib v4

Theorem well_founded.not_gt_of_lt

Modification history

2022-07-27 17:03
src/order/well_founded.lean
feat(order/well_founded): typeclasses for well-founded `<` and `>` (#15399) …
Deleted well_founded.not_gt_of_ltView on Github →
2022-05-04 11:10
src/order/well_founded.lean
feat(order/well_founded): Well founded relations are asymmetric and irreflexive (#13692)
Added well_founded.not_gt_of_ltView on Github →