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

From the sphere eversion project.

Co-authored-by: Floris van Doorn <04eee3258902297ef5081ba8b0786f6ab1274795@gmail.com>





leanprover-community/mathlib,leanprover-community/mathlib