Commit 2021-03-19 06:00 62d532a7
View on Github →feat(data/finset): erase is partially injective (#6737)
Show that erase is partially injective, ie that if s.erase x = s.erase y and x is in s, then x = y.
feat(data/finset): erase is partially injective (#6737)
Show that erase is partially injective, ie that if s.erase x = s.erase y and x is in s, then x = y.