mathlib3
52b6516b - refactor(order/disjointed): generalize `disjointed` to generalized boolean algebras (#8409)

Commit
4 years ago
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`).
Author
Parents
Loading