Commit 2023-05-28 23:39 4052cafd

View on Github →

feat: port Analysis.Calculus.Deriv.Inverse (#4438)

Estimated changes

Modified Mathlib.lean

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

added theorem HasDerivAt.eventually_ne

added theorem HasDerivAt.hasFDerivAt_equiv

added theorem HasDerivAt.of_local_left_inverse

added theorem HasDerivAt.tendsto_punctured_nhds

added theorem HasStrictDerivAt.hasStrictFDerivAt_equiv

added theorem HasStrictDerivAt.of_local_left_inverse

added theorem LocalHomeomorph.hasDerivAt_symm

added theorem LocalHomeomorph.hasStrictDerivAt_symm

added theorem not_differentiableAt_of_local_left_inverse_hasDerivAt_zero

added theorem not_differentiableWithinAt_of_local_left_inverse_hasDerivWithinAt_zero