Commit 2026-06-09 08:51 da74387b

View on Github →

chore: rename diff to sdiff (#40184) This PR changes diff to sdiff in identifier names when referring to the SDiff.sdiff operation \. Notes:

  • For subset_image_diff, I made its replacement private, deprecating it to the stronger image_sdiff.
  • There are some names with diff that are a bit mysterious to me, which I did not change in this PR: inverse_add_norm_diff_first_order, inverse_add_norm_diff_second_order, inverse_add_norm_diff_nth_order SimpleGraph.Adj.diff_dist_adj
  • Batteries has the definition List.diff, which maybe should instead be the \ operation?

Estimated changes

deleted theorem Hollom.R_diff_infinite
deleted theorem finprod_mem_mul_diff'
deleted theorem finprod_mem_mul_diff
added theorem finprod_mem_mul_sdiff'
added theorem finprod_mem_mul_sdiff
deleted theorem Set.mulIndicator_diff'
deleted theorem Set.mulIndicator_diff
added theorem Set.mulIndicator_sdiff
deleted theorem Subgroup.closure_diff_one
deleted theorem IsExtreme.convex_diff
added theorem IsExtreme.convex_sdiff
modified theorem Graph.deleteVerts_le
deleted theorem Matroid.Indep.diff
added theorem Matroid.Indep.sdiff
deleted theorem Finset.empty_diffs
added theorem Finset.empty_sdiffs
deleted theorem Finset.card_univ_diff
added theorem Finset.card_univ_sdiff
deleted theorem Set.toFinset_diff
added theorem Set.toFinset_sdiff
deleted theorem List.Nodup.diff_eq_filter
deleted theorem List.Nodup.mem_diff_iff
deleted theorem Set.Nonempty.of_diff
added theorem Set.Nonempty.of_sdiff
deleted theorem Set.encard_diff
added theorem Set.encard_sdiff
deleted theorem Set.le_ncard_diff
added theorem Set.le_ncard_sdiff
deleted theorem Set.ncard_diff'
deleted theorem Set.ncard_diff
deleted theorem Set.ncard_diff_add_ncard
added theorem Set.ncard_sdiff'
added theorem Set.ncard_sdiff
deleted theorem Set.Countable.of_diff
added theorem Set.Countable.of_sdiff
deleted theorem Set.Finite.diff
deleted theorem Set.Finite.of_diff
added theorem Set.Finite.of_sdiff
added theorem Set.Finite.sdiff
modified theorem Set.Finite.symmDiff
deleted theorem Set.Infinite.diff
added theorem Set.Infinite.sdiff
deleted theorem Set.InjOn.image_diff
added theorem Set.InjOn.image_sdiff
deleted theorem Set.image_diff
deleted theorem Set.image_diff_preimage
deleted theorem Set.image_diff_subset
added theorem Set.image_sdiff
added theorem Set.image_sdiff_subset
deleted theorem Set.preimage_diff
added theorem Set.preimage_sdiff
deleted theorem Set.range_diff_image
added theorem Set.range_sdiff_image
deleted theorem Set.subset_image_diff
deleted theorem Set.subset_image_symmDiff
deleted theorem Set.diff_iInter
deleted theorem Set.diff_iUnion
deleted theorem Set.iUnion_diff
added theorem Set.iUnion_sdiff
deleted theorem Set.pi_diff_pi_subset
added theorem Set.pi_sdiff_pi_subset
added theorem Set.sdiff_iInter
added theorem Set.sdiff_iUnion
deleted theorem Set.diff_eq
deleted theorem Set.mem_diff
deleted theorem Set.mem_diff_of_mem
added theorem Set.mem_sdiff
added theorem Set.mem_sdiff_of_mem
added theorem Set.sdiff_eq
deleted theorem Set.prod_diff_prod
added theorem Set.prod_sdiff_prod
deleted theorem Set.sigma_diff_sigma
added theorem Set.sigma_sdiff_sigma
deleted theorem Set.image_val_diff
added theorem Set.image_val_sdiff
deleted theorem Ioc_diff_botSet
added theorem Ioc_sdiff_botSet
deleted theorem Set.compl_diff
deleted theorem Set.compl_eq_univ_diff
added theorem Set.compl_sdiff
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_insert_of_notMem
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_ssubset_left_iff
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
added theorem Set.empty_sdiff
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_diff_subset
deleted theorem Set.inter_diff_assoc
deleted theorem Set.inter_diff_right_comm
deleted theorem Set.inter_diff_self
added theorem Set.inter_sdiff_assoc
added theorem Set.inter_sdiff_self
deleted theorem Set.inter_union_diff
added theorem Set.inter_union_sdiff
deleted theorem Set.ite_diff_self
added theorem Set.ite_sdiff_self
deleted theorem Set.mem_diff_singleton
deleted theorem Set.mem_of_mem_diff
added theorem Set.mem_of_mem_sdiff
deleted theorem Set.notMem_diff_of_mem
deleted theorem Set.notMem_of_mem_diff
deleted theorem Set.pair_diff_left
deleted theorem Set.pair_diff_right
added theorem Set.pair_sdiff_left
added theorem Set.pair_sdiff_right
added theorem Set.sdiff_compl
added theorem Set.sdiff_empty
added theorem Set.sdiff_eq_empty
added theorem Set.sdiff_inter
added theorem Set.sdiff_inter_sdiff
added theorem Set.sdiff_inter_self
added theorem Set.sdiff_nonempty
added theorem Set.sdiff_sdiff
added theorem Set.sdiff_sdiff_comm
added theorem Set.sdiff_sdiff_right
added theorem Set.sdiff_self
added theorem Set.sdiff_self_inter
added theorem Set.sdiff_subset
added theorem Set.sdiff_subset_comm
added theorem Set.sdiff_subset_compl
added theorem Set.sdiff_subset_iff
added theorem Set.sdiff_subset_sdiff
added theorem Set.sdiff_union_inter
added theorem Set.sdiff_union_self
added theorem Set.sdiff_univ
deleted theorem Set.subset_diff
deleted theorem Set.subset_diff_singleton
deleted theorem Set.subset_diff_union
added theorem Set.subset_sdiff
added theorem Set.subset_sdiff_union
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.union_sdiff_cancel
added theorem Set.union_sdiff_left
added theorem Set.union_sdiff_right
added theorem Set.union_sdiff_self
deleted theorem sSup_diff_singleton_bot
deleted theorem Filter.diff_mem
added theorem Filter.sdiff_mem
deleted theorem Ultrafilter.diff_mem_iff
deleted theorem Finset.Icc_diff_Ico_self
deleted theorem Finset.Icc_diff_Ioc_self
deleted theorem Finset.Icc_diff_Ioo_self
deleted theorem Finset.Icc_diff_both
added theorem Finset.Icc_sdiff_both
deleted theorem Finset.Ico_diff_Ico_left
deleted theorem Finset.Ico_diff_Ico_right
deleted theorem Finset.Ico_diff_Ioo_self
deleted theorem Finset.Iic_diff_Ioc
added theorem Finset.Iic_sdiff_Ioc
deleted theorem Finset.Ioc_diff_Ioo_self
deleted theorem Set.Icc_diff_Ico_same
deleted theorem Set.Icc_diff_Ioo_same
deleted theorem Set.Icc_diff_both
deleted theorem Set.Icc_diff_left
added theorem Set.Icc_sdiff_Ico_same
added theorem Set.Icc_sdiff_Ioo_same
added theorem Set.Icc_sdiff_both
added theorem Set.Icc_sdiff_left
deleted theorem Set.Ico_diff_Ioo_same
deleted theorem Set.Ico_diff_left
added theorem Set.Ico_sdiff_Ioo_same
added theorem Set.Ico_sdiff_left
deleted theorem Set.Iic_diff_Iio_same
deleted theorem Set.Iic_diff_right
added theorem Set.Iic_sdiff_Iio_same
added theorem Set.Iic_sdiff_right
deleted theorem Set.Ici_diff_Ici
deleted theorem Set.Ici_diff_Ioi
added theorem Set.Ici_sdiff_Ici
added theorem Set.Ici_sdiff_Ioi
deleted theorem Set.Ico_diff_Iio
added theorem Set.Ico_sdiff_Iio
deleted theorem Set.Iic_diff_Ioc
added theorem Set.Iic_sdiff_Ioc
deleted theorem Set.Ioc_diff_Iic
deleted theorem Set.Ioc_diff_Ioi
added theorem Set.Ioc_sdiff_Iic
added theorem Set.Ioc_sdiff_Ioi
deleted theorem Set.Ioi_diff_Ici
deleted theorem Set.Ioi_diff_Ioc
deleted theorem Set.Ioi_diff_Ioi
added theorem Set.Ioi_sdiff_Ici
added theorem Set.Ioi_sdiff_Ioc
added theorem Set.Ioi_sdiff_Ioi
modified theorem UpperSet.le_erase
modified theorem UpperSet.le_sdiff_left
deleted theorem Cardinal.mk_diff_add_mk
deleted theorem Class.coe_diff
added theorem Class.coe_sdiff
deleted theorem closure_diff_frontier
deleted theorem closure_diff_interior
added theorem closure_sdiff_frontier
added theorem closure_sdiff_interior
deleted theorem diff_subset_closure_iff
deleted theorem self_diff_frontier
added theorem self_sdiff_frontier
deleted theorem closure_diff
added theorem closure_sdiff
deleted theorem diff_mem_nhdsWithin_compl
deleted theorem diff_mem_nhdsWithin_diff
deleted theorem Dense.diff_finite
deleted theorem Dense.diff_finset
deleted theorem Dense.diff_singleton
added theorem Dense.sdiff_finite
added theorem Dense.sdiff_finset
added theorem Dense.sdiff_singleton