mathlib3

faf5e5c9 - feat(order/bounded_lattice): unbot and untop (#8885)

feat(order/bounded_lattice): unbot and untop (#8885) `unbot` sends non-`⊥` elements of `with_bot α` to the corresponding element of `α`. `untop` does the analogous thing for `with_top`.