mathlib

8df86df8 - feat(order/ideal, data/set/lattice): when order ideals are a complete lattice (#9084)

feat(order/ideal, data/set/lattice): when order ideals are a complete lattice (#9084) - Added the `ideal_Inter_nonempty` property, which states that the intersection of all ideals in the lattice is nonempty. - Proved that when a preorder has the above property and is a `semilattice_sup`, its ideals are a complete lattice - Added some lemmas about empty intersections in set/lattice, akin to #9033