cont_diff): extra lemmas about cont_diff_within_at (#15309)

Commit

3 years ago

feat(analysis/calculus/cont_diff): extra lemmas about cont_diff_within_at (#15309) * Also some lemmas about `fderiv_within` and `nhds_within`. * From the sphere eversion project

Author

fpvandoorn

Parents

51f76d05

mathlib 25f60b46 - feat(analysis/calculus/cont_diff): extra lemmas about cont_diff_within_at (#15309)

mathlib
25f60b46 - feat(analysis/calculus/cont_diff): extra lemmas about cont_diff_within_at (#15309)