Commit 2026-05-19 17:03 51113ff8

View on Github →

feat: generalize HasFDerivAt.of_local_left_inverse etc (#39488)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Calculus/ContDiff/Operations.lean

Modified Mathlib/Analysis/Calculus/Deriv/Inverse.lean

added theorem HasDerivAt.of_comp_left

Modified Mathlib/Analysis/Calculus/FDeriv/Equiv.lean

deleted theorem HasFDerivAt.of_local_left_inverse

deleted theorem HasFDerivWithinAt.of_local_left_inverse

deleted theorem HasStrictFDerivAt.of_local_left_inverse

deleted theorem OpenPartialHomeomorph.hasFDerivAt_symm

deleted theorem OpenPartialHomeomorph.hasStrictFDerivAt_symm

Created Mathlib/Analysis/Calculus/FDeriv/OfCompLeft.lean

added theorem HasFDerivAt.of_comp_of_isEmbedding

added theorem HasFDerivAt.of_comp_of_leftInverse

added theorem HasFDerivAt.of_local_left_inverse

added theorem HasFDerivAtFilter.of_comp_of_isEmbedding

added theorem HasFDerivAtFilter.of_comp_of_leftInverse

added theorem HasFDerivWithinAt.of_comp_of_isEmbedding

added theorem HasFDerivWithinAt.of_comp_of_leftInverse

added theorem HasFDerivWithinAt.of_local_left_inverse

added theorem HasStrictFDerivAt.of_comp_of_isEmbedding

added theorem HasStrictFDerivAt.of_comp_of_leftInverse

added theorem HasStrictFDerivAt.of_local_left_inverse

added theorem OpenPartialHomeomorph.hasFDerivAt_symm

added theorem OpenPartialHomeomorph.hasStrictFDerivAt_symm

Modified Mathlib/Analysis/Calculus/InverseFunctionTheorem/FDeriv.lean