basic): `insert a s = s ↔ a ∈ s` (#15493)

Commit

3 years ago

feat(data/{finset,set}/basic): `insert a s = s ↔ a ∈ s` (#15493) and `s.erase a = s ↔ a ∉ s`.

Author

YaelDillies

Parents