mathlib3

18dce134 - feat(data/finset/interval): Bounded intervals in locally finite orders are finite (#9960)

feat(data/finset/interval): Bounded intervals in locally finite orders are finite (#9960) A set which is bounded above and below is finite. A set which is bounded below in an `order_top` is finite. A set which is bounded above in an `order_bot` is finite. Also provide the `order_dual` constructions for `bdd_stuff` and `locally_finite_order`.