Commit 2025-07-04 10:05 5d5acbe3

View on Github →

chore(Data/Set/Disjoint): move BooleanAlgebra material to Order (#26724) Eventually, all order properties should move out, but this is a good second step that will, among others, unblock #23177.

Estimated changes

Modified Mathlib/Data/Set/Disjoint.lean

deleted theorem HasSubset.Subset.diff_ssubset_of_nonempty

deleted theorem Set.diff_ssubset_left_iff

deleted theorem Set.disjoint_compl_left_iff_subset

deleted theorem Set.disjoint_compl_right_iff_subset

deleted theorem Set.disjoint_of_subset_iff_left_eq_empty

deleted theorem Set.disjoint_sdiff_inter

deleted theorem Set.disjoint_sdiff_left

deleted theorem Set.disjoint_sdiff_right

deleted theorem Set.subset_compl_iff_disjoint_left

deleted theorem Set.subset_compl_iff_disjoint_right

deleted theorem Set.subset_diff

Modified Mathlib/Order/BooleanAlgebra/Set.lean

added theorem HasSubset.Subset.diff_ssubset_of_nonempty

added theorem Set.diff_ssubset_left_iff

added theorem Set.disjoint_compl_left_iff_subset

added theorem Set.disjoint_compl_right_iff_subset

added theorem Set.disjoint_of_subset_iff_left_eq_empty

added theorem Set.disjoint_sdiff_inter

added theorem Set.disjoint_sdiff_left

added theorem Set.disjoint_sdiff_right

added theorem Set.subset_compl_iff_disjoint_left

added theorem Set.subset_compl_iff_disjoint_right

added theorem Set.subset_diff