mathlib

947c3c6d - refactor(order/locally_finite): Allow `finset.Iix`/`finset.Ixi` on empty types (#14430)

refactor(order/locally_finite): Allow `finset.Iix`/`finset.Ixi` on empty types (#14430) Define `locally_finite_order_top` and `locally_finite_order_bot` are redefine `Ici`, `Ioi`, `iic`, `Iio` using them. Those new typeclasses are the same as `locally_finite_order` + `order_top`/`order_bot`, except that they allow the empty type, which is a surprisingly useful feature.