top (#15341)

Commit

3 years ago

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.

Author

adomani

Parents

68123285

mathlib3 ced11136 - feat(order/bounded_order): two lemmas about the interaction between monotonicity and map with_bot/top (#15341)

mathlib3
ced11136 - feat(order/bounded_order): two lemmas about the interaction between monotonicity and map with_bot/top (#15341)