Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes