function): add lemmas about `set.restrict` (#15605)

Commit

3 years ago

feat(data/set/function): add lemmas about `set.restrict` (#15605) From the sphere eversion project. Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>

Author

urkud

Parents

8ad82e4b

mathlib3 6b93ea7e - feat(data/set/function): add lemmas about `set.restrict` (#15605)

mathlib3
6b93ea7e - feat(data/set/function): add lemmas about `set.restrict` (#15605)