mathlib

e8cf0cfe - 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/compactly_generated): For any `b`, there exists a set of independent atoms `s` such that `Sup s` is the complement of `b`. (#8475) This new lemma is carved out of the proof that atomistic lattices are complemented. Also provide directed versions of the interaction between suprema and disjointness. Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>