Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-13 18:30 25f60b46

View on Github →

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

Estimated changes

Modified src/analysis/calculus/cont_diff.lean

added theorem cont_diff_within_at.congr_of_eventually_eq_insert

added theorem cont_diff_within_at.fderiv_within'

added theorem cont_diff_within_at.fderiv_within

added theorem cont_diff_within_at.has_fderiv_within_at_nhds

added theorem cont_diff_within_at_succ_iff_has_fderiv_within_at_of_mem

Modified src/analysis/calculus/fderiv.lean

added theorem fderiv_within.comp₃

added theorem filter.eventually_eq.fderiv_within_eq_nhds

added theorem has_fderiv_within_at.mono_of_mem

Modified src/topology/continuous_on.lean

added theorem nhds_within_le_iff