mathlib3
28e79d48
- chore(data/set/basic): add some lemmas to `function.surjective` (#2876)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
5 years ago
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.
Author
urkud
Parents
297806e6
Loading