Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-14 05:36 00004975

View on Github →

feat(order/basic, order/bounded_order): Generalized preorder to has_lt (#10695) This is a continuation of #10664.

Estimated changes

modified theorem no_bot
modified theorem no_top
added theorem with_bot.not_lt_none
modified theorem with_bot.well_founded_lt
added theorem with_top.not_none_lt
modified theorem with_top.well_founded_lt