Def HasStrictFDerivAt.localInverse

Modification history

2023-12-09 02:01

Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean

chore(Calculus/Inverse): split (#8603)

Modified HasStrictFDerivAt.localInverse View on Github →

2023-06-04 17:52

Mathlib/Analysis/Calculus/Inverse.lean

feat: port Analysis.Calculus.Inverse (#4644)

Added HasStrictFDerivAt.localInverse View on Github →