Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-27 02:02 48d831a4

View on Github →

feat(order/bounded_order): define with_bot.map and with_top.map (#14163) Also define monotone.with_bot etc.

Estimated changes

added def with_bot.map
modified theorem with_bot.map_bot
modified theorem with_bot.map_coe
added def with_top.map
modified theorem with_top.map_coe
modified theorem with_top.map_top