set.erase

Stream: Is there code for X?

[Kevin Buzzard]

We have finset.erase -- do we not have set.erase? Is it called something else? I know I can do S \ {a} but is this not a thing?

[Yakov Pechersky]

docs#set.insert_diff_singleton

[Yakov Pechersky]

This is likely due to the fact that while set and finset seem similar in how we think about them mathematically, they're constructed entirely differently, either by chaining predicates (set) or by quotienting finite lists of elements by permutations. And erase comes from the {list,multiset}.erase