mathlib3
48d831a4 - feat(order/bounded_order): define `with_bot.map` and `with_top.map` (#14163)

Commit

3 years ago

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

Author

urkud

Parents