Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-16 17:33 91a43e71

View on Github →

feat(algebra/order/monoid): Co/contravariant classes for with_bot/with_top (#13369) Add the covariant_class (with_bot α) (with_bot α) (+) (≤) and contravariant_class (with_bot α) (with_bot α) (+) (<) instances, as well as the lemmas that covariant_class (with_bot α) (with_bot α) (+) (<) and contravariant_class (with_bot α) (with_bot α) (+) (≤) almost hold. On the way, match the APIs for with_bot/with_top by adding missing lemmas.

Estimated changes

modified theorem with_bot.add_bot
modified theorem with_bot.add_eq_bot
added theorem with_bot.add_eq_coe
added theorem with_bot.add_ne_bot
modified theorem with_bot.bot_add
added theorem with_bot.bot_lt_add
modified theorem with_bot.coe_add
modified theorem with_bot.coe_bit0
modified theorem with_bot.coe_bit1
modified theorem with_top.add_coe_eq_top_iff
modified theorem with_top.add_eq_coe
modified theorem with_top.add_eq_top
modified theorem with_top.add_lt_top
added theorem with_top.add_ne_top
modified theorem with_top.add_top
modified theorem with_top.coe_add
modified theorem with_top.coe_add_eq_top_iff
modified theorem with_top.coe_bit0
modified theorem with_top.coe_bit1
modified theorem with_top.top_add
modified theorem with_zero.to_mul_bot_le
modified theorem with_zero.to_mul_bot_lt