mathlib3
7db76670 - feat(order/boolean_algebra): Interaction of disjointness and complements (#14925)

Commit
3 years ago
feat(order/boolean_algebra): Interaction of disjointness and complements (#14925) Prove `disjoint x yᶜ ↔ x ≤ y` and similar, transfer those results to `set`. Lemma renames * `subset_compl_iff_disjoint` → `subset_compl_iff_disjoint_right` * `set.subset_compl_iff_disjoint` → `set.subset_compl_iff_disjoint_right` * `disjoint_iff_le_compl_left` → `le_compl_iff_disjoint_left` * `disjoint_iff_le_compl_right` → `le_compl_iff_disjoint_right`
Author
Parents
Loading