Commit 2022-07-16 04:45 ced11136

View on Github →

feat(order/bounded_order): two lemmas about the interaction between monotonicity and map with_bot/top (#15341) Pulled out of #15294, that I ~~plan to~~ closed.

Estimated changes

Modified src/order/bounded_order.lean

added theorem with_bot.map_le_iff

added theorem with_top.map_le_iff

Modified src/order/hom/basic.lean