Theorem inf_Sup_eq_of_directed_on

feat(order/compactly_generated): For any `b`, there exists a set of independent atoms `s` such that `Sup s` is the complement of `b`. (#8475) …

feat(order/(complete_lattice, compactly_generated)): independent sets in a complete lattice (#5971) …