Commit 2025-07-05 02:43 ab509a4d

View on Github →

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

Estimated changes

deleted theorem Set.compl_ne_eq_singleton
deleted theorem Set.compl_singleton_eq
deleted theorem Set.diff_insert_of_notMem
deleted theorem Set.insert_diff_insert
deleted theorem Set.insert_diff_of_mem
deleted theorem Set.insert_diff_of_notMem
deleted theorem Set.insert_diff_singleton
deleted theorem Set.insert_erase_invOn
deleted theorem Set.mem_diff_singleton
deleted theorem Set.pair_diff_left
deleted theorem Set.pair_diff_right
deleted theorem Set.subset_diff_singleton
deleted theorem Set.subset_insert_iff
modified theorem Set.subset_pair_iff_eq
added theorem Set.compl_singleton_eq
added theorem Set.insert_diff_insert
added theorem Set.insert_diff_of_mem
added theorem Set.insert_erase_invOn
added theorem Set.mem_diff_singleton
added theorem Set.pair_diff_left
added theorem Set.pair_diff_right
added theorem Set.subset_insert_iff