mathlib3

e1db9093 - feat(order/filter): add lattice instance to order.ideal (#5937)

feat(order/filter): add lattice instance to order.ideal (#5937) Add lattice instance to `order.ideal P` when the preorder `P` is actually a `semilattice_sup_bot` (that is, when `P` is a partial order with all finite suprema).