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 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∎

Depends on

Used by

Dependency tree · two levels

24 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.6 (standard reference, not scraped)