Existing in Mathlib · Analysis
Inverse Function Theorem
If f has an invertible strict Fréchet derivative f' at a, then Mathlib's constructed local-inverse function has the inverse continuous linear equivalence f'.symm as its strict derivative at f a.
- strict Fréchet differentiability
- continuous linear equivalence
- local inverse
- open partial homeomorphism
- derivative of an inverse
- complete normed spaces
Exact theorem
Exact Mathlib statement
theorem HasStrictFDerivAt.to_localInverse {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} (hf : HasStrictFDerivAt f (f' : E →L[𝕜] F) a) : HasStrictFDerivAt (hf.localInverse f f' a) (f'.symm : F →L[𝕜] E) (f a)The theorem at a glance
Inverse function theorem at a glance
A visual guide to the theorem's hypotheses, structure, and conclusion; the exact statement gives the formal detail.
Inverse function theorem at a glance
Detailed visual description
The theorem card records the nontrivially normed scalar field, normed spaces, completeness of E, f, a, the continuous linear equivalence f', the strict derivative hypothesis, and g := hf.localInverse f f' a : F → E. Two bounded tangent windows distinguish the forward nonlinear map from the returning local-inverse function. The lower route traces strict approximation, OpenPartialHomeomorph construction, its symmetric function, and differentiation at f a, while the footer rules out a global-diffeomorphism reading.
Statement structure
From hypotheses to conclusion
This map summarizes the statement's structure; the exact Mathlib declaration remains authoritative.
A local inverse between bounded neighborhoods
Detailed visual description
A bounded green source patch and bounded cobalt target patch contain matching circles, squares, triangles, and diamonds around one highlighted point each. Several dashed emerald strands travel from source to target. A separate broad antique-gold ribbon curves from the highlighted target point back to the highlighted source point. Dashed guides enlarge those points into lower source and target tangent fans joined by two opposed gold arrows. The ambient plane remains unpaired outside the bounded patches, and no global inverse, surjectivity, text, formula, or status mark appears.
Why it matters
A mathematical landmark
This declaration isolates a central analytic conclusion of the inverse function theorem in a general normed-space setting: after Mathlib constructs its local-inverse function from strict approximation and an open partial homeomorphism, the inverse function's strict derivative at the image point is exactly the inverse continuous linear equivalence.
ProofAtlas record
What has been checked
Mathlib is the source of the theorem; the local Lean replay and page review are separate.
Claim boundary
No new theorem is claimed
This page indexes Mathlib's strict-derivative conclusion for its constructed local inverse. Over a nontrivially normed field, for normed spaces E and F with E complete, a strict Fréchet derivative of f at a given by a continuous linear equivalence f' implies that hf.localInverse f f' a : F → E has strict Fréchet derivative f'.symm at f a. Nearby definitions construct that function through an OpenPartialHomeomorph; the selected declaration itself does not assert a global inverse, global bijectivity, a global diffeomorphism, or inverse differentiability beyond f a.
- The selected declaration concludes a strict derivative formula for the already-constructed function hf.localInverse f f' a at the single point f a; it is not itself a global inverse-existence theorem.
- It does not assert that f is globally injective or surjective, that f is a global diffeomorphism, or that hf.localInverse is a two-sided inverse outside the local source construction.
- It does not assert differentiability of the inverse away from f a, a ContDiff conclusion, or a derivative formula throughout an explicitly quantified open set.
- It assumes a continuous linear equivalence f' and completeness of E; it is not a finite-dimensional determinant-only or real-only formulation.
- ProofAtlas is indexing an existing Mathlib theorem, and generated explanations and visuals are not proof evidence.
Source and local evidence
Where the theorem comes from
- Existing declaration
HasStrictFDerivAt.to_localInversein mathlib- Relationship
- The checked artifact is the upstream declaration itself
- Local Lean evidence
artifact.library.mathlib.inverse-function-theorem.v001