Commit 2022-06-28 19:09 7db76670
View on Github →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