Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-12 14:15 a5ccba6b

View on Github →

feat(analysis/calculus): generalize has_strict_fderiv_at.map_nhds_eq (#6193) Generalize has_strict_fderiv_at.map_nhds_eq to a function that satisfies assumptions of the implicit function theorem.

Estimated changes

Modified src/analysis/calculus/implicit.lean

added theorem has_strict_fderiv_at.implicit_function_apply_image

added theorem has_strict_fderiv_at.implicit_function_of_complemented_apply_image

added theorem has_strict_fderiv_at.map_nhds_eq

added theorem has_strict_fderiv_at.map_nhds_eq_of_complemented

added theorem has_strict_fderiv_at.tendsto_implicit_function

added theorem implicit_function_data.map_nhds_eq

Modified src/analysis/calculus/inverse.lean

deleted theorem has_strict_fderiv_at.map_nhds_eq

added theorem has_strict_fderiv_at.map_nhds_eq_of_equiv

deleted theorem open_map_of_strict_fderiv

added theorem open_map_of_strict_fderiv_equiv