Commit 2024-10-04 03:58 435c3d7b
View on Github →chore(Finset): remove old-style spellings (#17327)
Deprecate sdiff_singleton_eq_self in favour of erase_eq_of_not_mem: the spelling s.erase a is preferred over s \ {a}.
Deprecate sdiff_eq_self in favour of sdiff_eq_self_iff_disjoint: the spelling Disjoint s t is preferred over s ∩ t ⊆ ∅.
Deprecate filter_inter_filter_neg_eq in favour of disjoint_filter_filter_neg: the spelling Disjoint s t is preferred over s ∩ t = ∅.
Amend statement of filter_cons to be simpler and match filter_insert more closely.