bounded): Bounded order homomorphisms (#11806)

Commit

4 years ago

feat(order/hom/bounded): Bounded order homomorphisms (#11806) Define `bounded_order_hom` in `order.hom.bounded` and move `top_hom`, `bot_hom` there.

Author

YaelDillies

Parents