Commit 2025-07-03 15:35 2ae2c8e8

View on Github →

chore: move BooleanAlgebra material on Set out of Data (#26665) Eventually, all order properties should move out, but this is a good first step that will, among others, unblock #23177.

Estimated changes

deleted theorem Set.compl_def
deleted theorem Set.compl_diff
deleted theorem Set.compl_empty
deleted theorem Set.compl_empty_iff
deleted theorem Set.compl_eq_univ_diff
deleted theorem Set.compl_inter
deleted theorem Set.compl_inter_self
deleted theorem Set.compl_ne_univ
deleted theorem Set.compl_setOf
deleted theorem Set.compl_subset_comm
deleted theorem Set.compl_subset_compl
deleted theorem Set.compl_union
deleted theorem Set.compl_union_self
deleted theorem Set.compl_univ
deleted theorem Set.compl_univ_iff
deleted theorem Set.diff_compl
deleted theorem Set.diff_diff
deleted theorem Set.diff_diff_cancel_left
deleted theorem Set.diff_diff_comm
deleted theorem Set.diff_diff_right
deleted theorem Set.diff_diff_right_self
deleted theorem Set.diff_empty
deleted theorem Set.diff_eq_compl_inter
deleted theorem Set.diff_eq_empty
deleted theorem Set.diff_inter
deleted theorem Set.diff_inter_diff
deleted theorem Set.diff_inter_right_comm
deleted theorem Set.diff_inter_self
deleted theorem Set.diff_nonempty
deleted theorem Set.diff_self
deleted theorem Set.diff_self_inter
deleted theorem Set.diff_subset
deleted theorem Set.diff_subset_comm
deleted theorem Set.diff_subset_compl
deleted theorem Set.diff_subset_diff
deleted theorem Set.diff_subset_diff_left
deleted theorem Set.diff_subset_iff
deleted theorem Set.diff_union_inter
deleted theorem Set.diff_union_of_subset
deleted theorem Set.diff_union_self
deleted theorem Set.diff_univ
deleted theorem Set.empty_diff
deleted theorem Set.inter_compl_self
deleted theorem Set.inter_diff_assoc
deleted theorem Set.inter_diff_right_comm
deleted theorem Set.inter_diff_self
deleted theorem Set.inter_sdiff_left_comm
deleted theorem Set.inter_subset
deleted theorem Set.inter_subset_ite
deleted theorem Set.inter_union_compl
deleted theorem Set.inter_union_diff
deleted theorem Set.ite_compl
deleted theorem Set.ite_diff_self
deleted theorem Set.ite_empty
deleted theorem Set.ite_empty_left
deleted theorem Set.ite_empty_right
deleted theorem Set.ite_eq_of_subset_left
deleted theorem Set.ite_inter
deleted theorem Set.ite_inter_compl_self
deleted theorem Set.ite_inter_inter
deleted theorem Set.ite_inter_of_inter_eq
deleted theorem Set.ite_inter_self
deleted theorem Set.ite_left
deleted theorem Set.ite_mono
deleted theorem Set.ite_right
deleted theorem Set.ite_same
deleted theorem Set.ite_subset_union
deleted theorem Set.ite_univ
deleted theorem Set.mem_compl
deleted theorem Set.mem_of_mem_diff
deleted theorem Set.nonempty_compl
deleted theorem Set.notMem_compl_iff
deleted theorem Set.notMem_diff_of_mem
deleted theorem Set.notMem_of_mem_compl
deleted theorem Set.notMem_of_mem_diff
deleted theorem Set.sdiff_sep_self
deleted theorem Set.subset_compl_comm
deleted theorem Set.subset_diff_union
deleted theorem Set.subset_ite
deleted theorem Set.union_compl_self
deleted theorem Set.union_diff_cancel'
deleted theorem Set.union_diff_cancel
deleted theorem Set.union_diff_distrib
deleted theorem Set.union_diff_left
deleted theorem Set.union_diff_right
deleted theorem Set.union_diff_self
added theorem Set.compl_def
added theorem Set.compl_diff
added theorem Set.compl_empty
added theorem Set.compl_empty_iff
added theorem Set.compl_eq_univ_diff
added theorem Set.compl_inter
added theorem Set.compl_inter_self
added theorem Set.compl_ne_univ
added theorem Set.compl_setOf
added theorem Set.compl_subset_comm
added theorem Set.compl_subset_compl
added theorem Set.compl_union
added theorem Set.compl_union_self
added theorem Set.compl_univ
added theorem Set.compl_univ_iff
added theorem Set.diff_compl
added theorem Set.diff_diff
added theorem Set.diff_diff_comm
added theorem Set.diff_diff_right
added theorem Set.diff_empty
added theorem Set.diff_eq_empty
added theorem Set.diff_inter
added theorem Set.diff_inter_diff
added theorem Set.diff_inter_self
added theorem Set.diff_nonempty
added theorem Set.diff_self
added theorem Set.diff_self_inter
added theorem Set.diff_subset
added theorem Set.diff_subset_comm
added theorem Set.diff_subset_compl
added theorem Set.diff_subset_diff
added theorem Set.diff_subset_iff
added theorem Set.diff_union_inter
added theorem Set.diff_union_self
added theorem Set.diff_univ
added theorem Set.empty_diff
added theorem Set.inter_compl_self
added theorem Set.inter_diff_assoc
added theorem Set.inter_diff_self
added theorem Set.inter_subset
added theorem Set.inter_subset_ite
added theorem Set.inter_union_compl
added theorem Set.inter_union_diff
added theorem Set.ite_compl
added theorem Set.ite_diff_self
added theorem Set.ite_empty
added theorem Set.ite_empty_left
added theorem Set.ite_empty_right
added theorem Set.ite_inter
added theorem Set.ite_inter_inter
added theorem Set.ite_inter_self
added theorem Set.ite_left
added theorem Set.ite_mono
added theorem Set.ite_right
added theorem Set.ite_same
added theorem Set.ite_subset_union
added theorem Set.ite_univ
added theorem Set.mem_compl
added theorem Set.mem_of_mem_diff
added theorem Set.nonempty_compl
added theorem Set.notMem_compl_iff
added theorem Set.notMem_diff_of_mem
added theorem Set.notMem_of_mem_diff
added theorem Set.sdiff_sep_self
added theorem Set.subset_compl_comm
added theorem Set.subset_diff_union
added theorem Set.subset_ite
added theorem Set.union_compl_self
added theorem Set.union_diff_cancel'
added theorem Set.union_diff_cancel
added theorem Set.union_diff_distrib
added theorem Set.union_diff_left
added theorem Set.union_diff_right
added theorem Set.union_diff_self