Theorem finset.sup_le_of_le_directed

refactor(*): split `order_{top,bot}` from `lattice` hierarchy (#9891) …

feat(order/complete_well_founded, data/finset/lattice): introduce compact elements of a complete lattice and characterize compact lattices as those with all elements compact (#5825) …