mathlib

7ddb9a3c - refactor(order/ideal): Generalize definition and lemmas (#11421)

refactor(order/ideal): Generalize definition and lemmas (#11421) * Generalize the `order_top` instance to `[nonempty P] [is_directed P (≤)]`. * Delete `order.ideal.ideal_inter_nonempty` in favor of the equivalent condition `is_directed P (swap (≤))`. * Delete `order.ideal.sup`/`order.ideal.inf` in favor of a direct instance declaration. * Generalize defs/lemmas from `preorder` to `has_le` or `partial_order` to `preorder`. * Two more `is_directed` lemmas and instances for `order_bot` and `order_top`.