Commit 2022-10-18 05:41 38992f94

feat(analysis/calculus/cont_diff): strengthen lemma (#16933)

• The new cont_diff_within_at_succ_iff_has_fderiv_within_at' generalizes cont_diff_within_at.has_fderiv_within_at_nhds and cont_diff_within_at_succ_iff_has_fderiv_within_at_of_mem
• Prove that has_fderiv_within_at and cont_diff_within_at are not dependent on adding a single point to the set
• Add some more lemmas needed for a follow-up PR
• From the sphere eversion project