Theorems · Definition · real analysis
HasStrictDerivAt.localInverse
{𝕜 : Type u_1} →
[inst : NontriviallyNormedField 𝕜] →
[CompleteSpace 𝕜] → (f : 𝕜 → 𝕜) → (f' a : 𝕜) → HasStrictDerivAt f f' a → f' ≠ 0 → 𝕜 → 𝕜A function that is inverse to f near a.
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 185 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- NontriviallyNormedFieldstatement and proof · cited by 8,742
- CompleteSpacestatement and proof · cited by 2,532
- Units.mk0proof · cited by 181
- HasStrictDerivAtstatement and proof · cited by 163
- HasStrictFDerivAt.localInverseproof · cited by 11
- HasStrictDerivAt.hasStrictFDerivAt_equivproof · cited by 10
- ContinuousLinearEquiv.unitsEquivAutproof · cited by 7
Cited by7
Results whose statement or proof uses this declaration.
- HasStrictDerivAt.eventually_right_inversestatement · cited by 2
- Function.Periodic.differentiableAt_cuspFunctionproof · cited by 2
- meromorphicAt_comp_iff_of_deriv_ne_zeroproof · cited by 2
- AnalyticAt.analyticAt_localInversestatement · cited by 2
- analyticAt_comp_iff_of_deriv_ne_zeroproof · cited by 2
- HasStrictDerivAt.to_localInversestatement · cited by 1
- HasStrictDerivAt.eventually_left_inversestatement · cited by 0