Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-25 16:34 27f315c5

View on Github →

feat(analysis/calculus/cont_diff): Prove that fderiv_within is C^n for functions with parameters (#16946)

Prove that fderiv_within is C^n (at a point within a set) for a function with parameters
There are some inconvenient side-conditions needed for the lemmas, feel free to recommend improvements
set.diag_image is not used, but a (useful) left-over used before a refactor.
This is useful for lemmas about mfderiv and the smooth vector bundle refactor
From the sphere eversion project

Estimated changes

Modified src/analysis/calculus/cont_diff.lean

added theorem cont_diff.clm_apply

added theorem cont_diff.fderiv

added theorem cont_diff.fderiv_apply

added theorem cont_diff.smul_right

added theorem cont_diff_at.cont_diff_at_fderiv

added theorem cont_diff_on.clm_apply

modified theorem cont_diff_on_fderiv_within_apply

added theorem cont_diff_within_at.fderiv_within''

modified theorem cont_diff_within_at.fderiv_within'

modified theorem cont_diff_within_at.fderiv_within

added theorem cont_diff_within_at.fderiv_within_apply

added theorem cont_diff_within_at.fderiv_within_right

added theorem cont_diff_within_at.has_fderiv_within_at_nhds

added theorem continuous.fderiv

Modified src/data/set/prod.lean

added theorem set.diag_image