mathlib

a16a5b5b - chore(order/lattice_intervals): review (#11416)

chore(order/lattice_intervals): review (#11416) * use `@[reducible] protected def`; * add `is_least.order_bot` and `is_greatest.order_top`, use them; * weaken TC assumptions on `set.Ici.bounded_order` and `set.Iic.bounded_order`.