Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-31 01:56 28e79d48

View on Github →

chore(data/set/basic): add some lemmas to function.surjective (#2876) This way they can be used with dot notation. Also rename set.surjective_preimage to function.surjective.injective_preimage. I think that the old name was misleading.

Estimated changes