mathlib
6f59d777 - feat(order/bounded_order): Basic API for `subtype.order_bot` and `subtype.order_top` (#12904)

Commit

3 years ago

feat(order/bounded_order): Basic API for `subtype.order_bot` and `subtype.order_top` (#12904) A few `simp` lemmas that were needed for `subtype.order_bot` and `subtype.order_top`.

Author

Paul-Lez

Parents

5b8bb9b4

mathlib 6f59d777 - feat(order/bounded_order): Basic API for `subtype.order_bot` and `subtype.order_top` (#12904)

mathlib
6f59d777 - feat(order/bounded_order): Basic API for `subtype.order_bot` and `subtype.order_top` (#12904)