Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-09 00:14 a380a130

View on Github →

feat(order/bounded_order): turn monotone.with_bot_map etc into iff lemmas (#17121)

Estimated changes

Modified src/order/bounded_order.lean

added theorem with_bot.coe_mono

added theorem with_bot.monotone_iff

added theorem with_bot.monotone_map_iff

added theorem with_bot.strict_mono_iff

added theorem with_bot.strict_mono_map_iff

added theorem with_top.coe_mono

added theorem with_top.monotone_iff

added theorem with_top.monotone_map_iff

added theorem with_top.strict_mono_iff

added theorem with_top.strict_mono_map_iff