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.

✓ 3 results · all verified · 0 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 3 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

The Inverse and Implicit Function Theorems

1 · Prerequisites

2 · Summary

Multivariable differentiation, mixed partial derivatives, Taylor estimates, and Euclidean completeness provide the local analytic tools for these theorems. In particular, continuity of a derivative controls a map by its linearisation, while the contraction principle gives a mechanism for solving a nearby nonlinear equation uniquely.

This core defines $C^{1}$ Euclidean maps, local diffeomorphisms, and invertible linear maps. A quantitative Newton-map lemma supplies both the contraction and nearby-invertibility estimates. It yields the Euclidean inverse function theorem, after which a block-map reduction gives the implicit function theorem and its derivative formula.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-03Open item page →

Continuously differentiable maps, local inverses, and local diffeomorphisms

Definition

Let $U \subseteq R^{m}$ be open and $f : U \to R^{n}$ . The map $f$ is continuously differentiable, or of class $C^{1}$ , when it is totally differentiable at every point of $U$ and the entries of its derivative matrix are continuous functions on $U$ .

For an open $U \subseteq R^{n}$ and $a \in U$ , a local inverse of $f$ at $a$ is a function $g : W \to V$ for open neighbourhoods $a \in V \subseteq U$ and $f (a) \in W \subseteq R^{n}$ such that $f ∣_{V} : V \to W$ is bijective and $g = (f ∣_{V})^{- 1}$ . If both $f ∣_{V}$ and $g$ are $C^{1}$ , this restriction is a local diffeomorphism at $a$ .

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-03Open item page →

Invertible Euclidean linear maps

Definition

Let $n \geq 1$ . A linear map $A : R^{n} \to R^{n}$ (A linear map $L : R^{m} \to R^{n}$ in Euclidean coordinates) is invertible when there is a linear map $B : R^{n} \to R^{n}$ such that

$B (A u) = u and A (B u) = u (u \in R^{n}) .$

The map $B$ is unique: if $C$ has the same two properties, then $C = C \circ (A \circ B) = (C \circ A) \circ B = B$ . It is denoted $A^{- 1}$ .

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-03Open item page →

Newton maps are uniform contractions near a point with invertible derivative

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$ . Suppose $A : = D f (a)$ is invertible and put $B : = A^{- 1}$ . Then there are $R > 0$ , $0 \leq q < 1$ , and $C > 0$ such that $\overline{B} (a, R) \subseteq U$ , $∥ B v ∥_{2} \leq C ∥ v ∥_{2}$ , and, for every $y \in R^{n}$ , the Newton map

$T_{y} (x) : = x + B (y - f (x))$

satisfies

$∥ T_{y} (x) - T_{y} (z) ∥_{2} \leq q ∥ x - z ∥_{2} (x, z \in \overline{B} (a, R)) .$

Moreover $D f (x)$ is invertible for every $x \in \overline{B} (a, R)$ and

$∥ D f (x)^{- 1} v ∥_{2} \leq \frac{C}{1 - q} ∥ v ∥_{2} .$

Facts & Assumptions

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

[L1]

Euclidean linear maps have finite matrices and a global norm bound (Every Euclidean linear map has a unique matrix and satisfies $∥ L h ∥_{2} \leq K ∥ h ∥_{2}$ for some $K \geq 0$ ).

[L2]

The entries of $D f$ are continuous by the definition of $C^{1}$ (Continuously differentiable maps, local inverses, and local diffeomorphisms).

[L3]

Total derivatives obey the linear algebra and chain rules, and a uniform derivative bound on a convex open set gives the corresponding Lipschitz bound (Sums and scalar multiples of totally differentiable maps are totally differentiable with the expected derivatives, The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ , On a convex open set, a uniform bound $∥ D f (z) v ∥_{2} \leq M ∥ v ∥_{2}$ implies $∥ f (y) - f (x) ∥_{2} \leq M ∥ y - x ∥_{2}$ ).

[L4]

Every $R^{n}$ , $n \geq 1$ , is complete, so its contractions have unique fixed points ( $R$ and $R^{n}$ for $n \geq 1$ with the Euclidean metric are complete, componentwise from the Cauchy criterion in $R$ , A contraction of a nonempty complete metric space into itself has exactly one fixed point, the limit of the iterates from any starting point).

[L5]

Metric balls have their open and closed forms, and openness supplies a closed ball about $a$ contained in $U$ (Open ball, closed ball and sphere in a metric space, The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement).

[L6]

The Euclidean norm satisfies the finite-dimensional Cauchy--Schwarz estimate (Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation).

[L7]

Invertibility means having a two-sided linear inverse (Invertible Euclidean linear maps).

Proof

technique · contraction

1.1

By [L1], choose $C > 0$ with $∥ B v ∥_{2} \leq C ∥ v ∥_{2}$ . Matrix-entry continuity [L2], [L6], and [L5] give $R > 0$ such that $\overline{B} (a, R) \subset B (a, 2 R) \subseteq U$ and $∥ B (D f (w) - A) v ∥_{2} \leq \frac{1}{2} ∥ v ∥_{2}$ for $w \in B (a, 2 R)$ and $v \in R^{n}$ . Fix $q : = 1 / 2$ .

L1L2L5L6algebra

2.1

The chain rule gives $D T_{y} (w) = I - B D f (w) = B (A - D f (w))$ , independently of $y$ . The convex open ball $B (a, 2 R)$ contains the closed ball, so [L3] and step 1.1 yield $∥ T_{y} (x) - T_{y} (z) ∥_{2} \leq q ∥ x - z ∥_{2}$ for $x, z \in \overline{B} (a, R)$ .

step 1.1L3

3.1

Fix $w$ in the ball, put $L : = D f (w)$ , and fix $v \in R^{n}$ . The map $S_{v} (u) : = u + B (v - L u)$ is a contraction of the complete space $R^{n}$ with constant $q$ , by the same estimate as step 2.1. By [L4] it has a unique fixed point $u$ , and the fixed-point equation is equivalent to $L u = v$ . Thus $L$ is surjective. If $L u = 0$ , both $u$ and $0$ are fixed by $S_{0}$ , so uniqueness gives $u = 0$ ; hence $L$ is injective. The solution map is linear by uniqueness, so it is $L^{- 1}$ .

step 1.1L4L7

4.1

From $L u = v$ and step 1.1, $∥ u ∥_{2} \leq ∥ u - B L u ∥_{2} + ∥ B v ∥_{2} \leq q ∥ u ∥_{2} + C ∥ v ∥_{2}$ . Therefore $∥ L^{- 1} v ∥_{2} \leq C (1 - q)^{- 1} ∥ v ∥_{2}$ .

step 1.1step 3.1algebra

5.1

Steps 1.1--4.1 give every asserted constant, contraction estimate, invertibility claim, and inverse bound.

step 1.1step 2.1step 3.1step 4.1∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-03Open item page →

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∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-03Open item page →

The Euclidean implicit function theorem with derivative formula

Statement

Let $m, n \geq 1$ , let $U \subseteq R^{m + n}$ be open, and let $F : U \to R^{n}$ be $C^{1}$ . Suppose $(a, b) \in U$ , $F (a, b) = 0$ , and the partial derivative in the second block

$D_{y} F (a, b) : R^{n} \to R^{n}, D_{y} F (a, b) v : = D F (a, b) (0, v),$

is invertible. Put similarly $D_{x} F (a, b) u : = D F (a, b) (u, 0)$ . Then there are open neighbourhoods $P$ of $a$ and $Q$ of $b$ , and a unique $C^{1}$ map $φ : P \to Q$ , such that

$F (x, y) = 0 ⟺ y = φ (x) ((x, y) \in P \times Q) .$

After shrinking $P, Q$ if necessary, $D_{y} F (x, φ (x))$ is invertible and

$D φ (x) = - D_{y} F (x, φ (x))^{- 1} D_{x} F (x, φ (x)) .$

Facts & Assumptions

Given: The dimensions, $C^{1}$ map, base point, zero equation, and invertible second-block derivative in the statement.

[L1]

A $C^{1}$ map with invertible derivative has a local $C^{1}$ inverse $G$ , with $D G (z) = D H (G (z))^{- 1}$ throughout its inverse neighbourhood (The Euclidean inverse function theorem).

[L2]

Total differentiability is a linear approximation with an $o (∥ h ∥_{2})$ remainder, and total derivatives obey the algebra and chain rules (The total (Fréchet) derivative $D f (a)$ as the linear first-order approximation with $o (∥ h ∥_{2})$ remainder, Sums and scalar multiples of totally differentiable maps are totally differentiable with the expected derivatives, The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ ).

[L3]

Euclidean linear maps have their finite matrix descriptions (Every Euclidean linear map has a unique matrix and satisfies $∥ L h ∥_{2} \leq K ∥ h ∥_{2}$ for some $K \geq 0$ ), and invertibility means having a two-sided linear inverse (Invertible Euclidean linear maps).

Proof

technique · reduction

1.1

Define $H : U \to R^{m + n}$ by $H (x, y) : = (x, F (x, y))$ . From [L2], the remainder after the linear map $(u, v) \mapsto (u, D F (x, y) (u, v))$ is $(0, r (u, v))$ , so $H$ is differentiable with $D H (x, y) (u, v) = (u, D_{x} F (x, y) u + D_{y} F (x, y) v) .$ Its matrix entries are continuous because those of $D F$ are, so $H$ is $C^{1}$ . If $B : = D_{y} F (a, b)^{- 1}$ , the displayed derivative at $(a, b)$ has the two-sided inverse $(r, s) \mapsto (r, B (s - D_{x} F (a, b) r))$ . Thus $D H (a, b)$ is invertible.

L2L3givenalgebra

2.1

Apply [L1] to $H$ . It has a $C^{1}$ inverse $G$ between neighbourhoods of $(a, b)$ and $(a, 0)$ . Because the first component of $H$ is $x$ , the identity $H (G (x, z)) = (x, z)$ forces $G (x, z) = (x, ψ (x, z))$ . Define $φ (x) : = ψ (x, 0)$ after shrinking to product neighbourhoods $P, Q$ .

step 1.1L1

3.1

For $(x, y) \in P \times Q$ , the local injectivity of $H$ gives $F (x, y) = 0 ⟺ H (x, y) = (x, 0) ⟺ (x, y) = G (x, 0) ⟺ y = φ (x)$ . This proves existence and local uniqueness; $φ$ is $C^{1}$ as a component of $G$ .

step 2.1

4.1

Differentiate $F (x, φ (x)) = 0$ . By [L2], $D_{x} F (x, φ (x)) + D_{y} F (x, φ (x)) D φ (x) = 0$ . For $(x, φ (x)) = G (x, 0)$ , the derivative formula in [L1] makes $D H (x, φ (x))$ invertible. The block formula of step 1.1 then makes $D_{y} F (x, φ (x))$ invertible: solving $D H (u, v) = (0, s)$ gives $u = 0$ and $D_{y} F v = s$ . Multiplication by its inverse yields the asserted formula.

step 1.1step 2.1step 3.1L1L2L3

5.1

Steps 1.1--4.1 prove all local existence, uniqueness, regularity, and derivative claims.

step 1.1step 2.1step 3.1step 4.1∎

5 · Examples, counterexamples and false statements

None yet.

The Inverse and Implicit Function Theorems

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

Continuously differentiable maps, local inverses, and local diffeomorphisms

Definition

Invertible Euclidean linear maps

Definition

Newton maps are uniform contractions near a point with invertible derivative

Statement

Facts & Assumptions

Proof

The Euclidean inverse function theorem

Statement

Facts & Assumptions

Proof

The Euclidean implicit function theorem with derivative formula

Statement

Facts & Assumptions

Proof

5 · Examples, counterexamples and false statements

Sources