Commit 2021-08-05 19:03 52b6516b

refactor(order/disjointed): generalize disjointed to generalized boolean algebras (#8409)

• Split data.set.disjointed into data.set.pairwise and order.disjointed. Change imports accordingly.
• In order.disjointed, change set α to generalized_boolean_algebra α. Redefine disjointed in terms of partial_sups to avoid needing completeness. Keep set notation variants of lemmas for easier unification.
• Rename some lemmas and reorder their arguments to make dot notation functional.
• Generalize some (where some = 2) pairwise lemmas.
• Delete lemmas which are unused and are a straightforward rw away from a simpler one (Union_disjointed_of_mono).