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

Estimated changes

Modified src/algebra/support.lean

Modified src/analysis/convex/stone_separation.lean

Modified src/analysis/normed_space/riesz_lemma.lean

Modified src/data/set/basic.lean

modified theorem set.compl_subset_comm

modified theorem set.compl_subset_compl

added theorem set.disjoint_compl_left_iff_subset

added theorem set.disjoint_compl_right_iff_subset

modified theorem set.subset_compl_comm

added theorem set.subset_compl_iff_disjoint_left

added theorem set.subset_compl_iff_disjoint_right

Modified src/data/set/lattice.lean

added theorem set.disjoint_Union₂_left

added theorem set.disjoint_Union₂_right

deleted theorem set.disjoint_iff_subset_compl_left

deleted theorem set.disjoint_iff_subset_compl_right

added theorem set.disjoint_sUnion_left

added theorem set.disjoint_sUnion_right

Modified src/group_theory/free_product.lean

Modified src/logic/equiv/embedding.lean

Modified src/order/boolean_algebra.lean

added theorem disjoint_compl_left_iff

added theorem disjoint_compl_right_iff

deleted theorem disjoint_iff_le_compl_left

deleted theorem disjoint_iff_le_compl_right

added theorem le_compl_iff_disjoint_left

added theorem le_compl_iff_disjoint_right

Modified src/order/complete_boolean_algebra.lean

added theorem disjoint_supr₂_iff

added theorem supr₂_disjoint_iff

Modified src/order/filter/bases.lean

Modified src/topology/basic.lean

Modified src/topology/metric_space/hausdorff_distance.lean