Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-11 20:09 b1ca33e0

View on Github →

feat(analysis/calculus/times_cont_diff, analysis/calculus/inverse): smooth inverse function theorem (#4407) The inverse function theorem, in the C^k and smooth categories.

Estimated changes

Modified src/analysis/calculus/fderiv.lean

added theorem has_fderiv_at.of_local_homeomorph

Modified src/analysis/calculus/inverse.lean

added theorem times_cont_diff_at.image_mem_to_local_homeomorph_target

added def times_cont_diff_at.local_inverse

added theorem times_cont_diff_at.local_inverse_apply_image

added theorem times_cont_diff_at.mem_to_local_homeomorph_source

added def times_cont_diff_at.to_local_homeomorph

added theorem times_cont_diff_at.to_local_homeomorph_coe

added theorem times_cont_diff_at.to_local_inverse

Modified src/analysis/calculus/times_cont_diff.lean

added theorem times_cont_diff_at.has_strict_fderiv_at'

added theorem times_cont_diff_at.of_local_homeomorph

added theorem times_cont_diff_at_zero

added theorem times_cont_diff_within_at_zero