Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-16 17:33 018e9b57

View on Github →

chore(order/bounded_order): Match the with_bot and with_top API (#13419) The API for with_top and the API for with_bot somehow evolved independently from each other, which created frustating disparity in lemmas and argument implicitness. This synchronizes everything (including the layout), generalize a few lemmas from preorder/partial_order to has_le/has_lt, and removes the duplicated is_total (with_bot α) (≤)/is_total (with_top α) (≤) instances.

Estimated changes

modified theorem with_bot.bot_lt_coe
modified theorem with_bot.bot_ne_coe
modified theorem with_bot.coe_eq_coe
modified theorem with_bot.coe_le
modified theorem with_bot.coe_le_coe
added theorem with_bot.coe_le_iff
modified theorem with_bot.coe_lt_coe
modified theorem with_bot.coe_ne_bot
modified theorem with_bot.coe_unbot
added theorem with_bot.le_coe_iff
added theorem with_bot.lt_coe_iff
modified theorem with_bot.ne_bot_iff_exists
added theorem with_bot.none_le
modified theorem with_bot.none_lt_some
modified theorem with_bot.not_coe_le_bot
modified theorem with_bot.not_lt_none
modified theorem with_bot.some_le_some
modified theorem with_bot.some_lt_some
modified theorem with_bot.unbot_coe
modified theorem with_bot.well_founded_lt
modified theorem with_top.coe_eq_coe
modified theorem with_top.coe_le_coe
modified theorem with_top.coe_le_iff
modified theorem with_top.coe_lt_coe
modified theorem with_top.coe_lt_iff
modified theorem with_top.coe_lt_top
modified theorem with_top.coe_max
modified theorem with_top.coe_min
modified theorem with_top.coe_ne_top
modified theorem with_top.coe_untop
modified theorem with_top.le_coe
modified theorem with_top.le_coe_iff
modified theorem with_top.le_none
modified theorem with_top.lt_iff_exists_coe
modified theorem with_top.ne_top_iff_exists
modified theorem with_top.not_none_lt
modified theorem with_top.not_top_le_coe
modified theorem with_top.some_le_some
modified theorem with_top.some_lt_none
modified theorem with_top.some_lt_some
modified theorem with_top.top_ne_coe
modified theorem with_top.well_founded_lt