mathlib3

c1936c1f - feat(order/basic): define `is_top` and `is_bot` (#9493)

feat(order/basic): define `is_top` and `is_bot` (#9493) These predicates allow us to formulate & prove some theorems simultaneously for the cases `[order_top α]` and `[no_top_order α]`.