TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-03

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The Euclidean inverse function theorem

Statement

Let $n \geq 1$ , let $U \subseteq R^{n}$ be open, let $f : U \to R^{n}$ be $C^{1}$ , and let $a \in U$ . If $D f (a)$ is invertible, then there are open sets $V, W \subseteq R^{n}$ with $a \in V \subseteq U$ and $f (a) \in W$ such that $f ∣_{V} : V \to W$ is bijective. Its inverse $g : W \to V$ is $C^{1}$ , and

$D g (y) = D f (g (y))^{- 1} (y \in W) .$

Thus $f$ is a local diffeomorphism at $a$ .

Facts & Assumptions

Given: The dimensions, $C^{1}$ map, point, and invertible derivative in the statement.

[L1]

The local Newton lemma supplies a closed ball, a uniform contraction constant, a bound for $D f (a)^{- 1}$ , and invertibility of every nearby derivative with the uniform bound $∥ D f (x)^{- 1} v ∥_{2} \leq C (1 - q)^{- 1} ∥ v ∥_{2}$ (Newton maps are uniform contractions near a point with invertible derivative).

[L2]

A closed subspace of a complete metric space is complete; Euclidean space is complete (Closed subspaces of complete metric spaces are complete; the converse under countable choice, $R$ and $R^{n}$ for $n \geq 1$ with the Euclidean metric are complete, componentwise from the Cauchy criterion in $R$ ).

[L3]

A self-contraction of a nonempty complete metric space has a unique fixed point (A contraction of a nonempty complete metric space into itself has exactly one fixed point, the limit of the iterates from any starting point).

[L4]

Total differentiability gives continuity, continuous maps pull open sets back to open sets, and total derivatives satisfy the chain rule (Total differentiability gives a local $O (∥ h ∥_{2})$ increment bound and therefore continuity, Metric continuity characterisations, with countable choice for the sequential converse, The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ ).

[L5]

Total differentiability means a linear approximation with an $o (∥ h ∥_{2})$ remainder (The total (Fréchet) derivative $D f (a)$ as the linear first-order approximation with $o (∥ h ∥_{2})$ remainder).

Proof

technique · contraction

1.1

Take $R, q, C$ from [L1], and write $A : = D f (a)$ , $B : = A^{- 1}$ . Shrink $R$ if needed without changing the estimates. Choose $ε > 0$ so that $C ε < (1 - q) R$ , and put $W : = B (f (a), ε)$ . For $y \in W$ and $x \in \overline{B} (a, R)$ , $∥ T_{y} (x) - a ∥_{2} \leq q ∥ x - a ∥_{2} + ∥ B (y - f (a)) ∥_{2} < R .$ Thus $T_{y}$ maps the closed ball into itself.

L1algebra

2.1

The closed ball is nonempty and complete by [L2]. Hence [L3] gives a unique fixed point $g (y)$ of $T_{y}$ . The fixed-point equation is exactly $f (g (y)) = y$ , and the strict inequality in step 1.1 puts $g (y)$ in the open ball.

step 1.1L2L3

3.1

If $f (x) = f (z)$ for two points of the closed ball, then both are fixed by $T_{f (x)}$ ; the contraction estimate forces $x = z$ . Define $V : = B (a, R) \cap f^{- 1} [W] .$ It is open by [L4], contains $a$ , and steps 2.1 and 3.1 show that $f ∣_{V} : V \to W$ is bijective with inverse $g$ .

step 2.1L1L4

3.2

For $y, z \in W$ , compare the fixed-point equations to obtain $∥ g (y) - g (z) ∥_{2} \leq q ∥ g (y) - g (z) ∥_{2} + C ∥ y - z ∥_{2} .$ Thus $g$ is Lipschitz, hence continuous.

L1step 2.1algebra

4.1

Fix $y \in W$ , put $x : = g (y)$ and $L : = D f (x)$ . For small $h$ , write $g (y + h) = x + k$ . Step 3.2 gives $∥ k ∥_{2} = O (∥ h ∥_{2})$ , while differentiability of $f$ gives $h = L k + r (k)$ with $∥ r (k) ∥_{2} = o (∥ k ∥_{2})$ . Since [L1] makes $L$ invertible with locally uniform inverse bound, $k = L^{- 1} h - L^{- 1} r (k) = L^{- 1} h + o (∥ h ∥_{2}) .$ Therefore $D g (y) = D f (g (y))^{- 1}$ .

step 3.2L1L5algebra

5.1

The entries of $D f (g (y))$ are continuous. The identity $P^{- 1} - Q^{- 1} = P^{- 1} (Q - P) Q^{- 1}$ , together with the uniform inverse bound in [L1], shows that the entries of $D g$ are continuous. Hence $g$ is $C^{1}$ .

step 3.2step 4.1L1algebra

6.1

Steps 3.1--5.1 give the required local $C^{1}$ inverse and derivative formula, so the final local-diffeomorphism clause is exactly Continuously differentiable maps, local inverses, and local diffeomorphisms.

step 3.1step 3.2step 4.1step 5.1∎

Depends on

Used by

Dependency tree · two levels

62 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

J. Lebl, Basic Analysis II, Theorem 8.5.1 (standard reference, not scraped)