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
.