TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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\ge1$ , let $U\subseteq\mathbb R^{m+n}$ be open, and let $F:U\to\mathbb R^n$ be $C^1$ . Suppose $(a,b)\in U$ , $F(a,b)=0$ , and the partial derivative in the second block

$D_yF(a,b):\mathbb R^n\to\mathbb R^n,\qquad D_yF(a,b)v:=DF(a,b)(0,v),$

is invertible. Put similarly $D_xF(a,b)u:=DF(a,b)(u,0)$ . Then there are open neighbourhoods $P$ of $a$ and $Q$ of $b$ , and a unique $C^1$ map $\varphi:P\to Q$ , such that

$F(x,y)=0\quad\Longleftrightarrow\quad y=\varphi(x)\qquad((x,y)\in P\times Q).$

After shrinking $P,Q$ if necessary, $D_yF(x,\varphi(x))$ is invertible and

$D\varphi(x)=-D_yF(x,\varphi(x))^{-1}D_xF(x,\varphi(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 $DG(z)=DH(G(z))^{-1}$ throughout its inverse neighbourhood (The Euclidean inverse function theorem).

[L2]

Total differentiability is a linear approximation with an $o(\lVert h\rVert_2)$ remainder, and total derivatives obey the algebra and chain rules (The total (Fréchet) derivative $Df(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)=Dg(f(a))\circ Df(a)$ ).

[L3]

Euclidean linear maps have their finite matrix descriptions (Every Euclidean linear map has a unique matrix and satisfies $\|Lh\|_2\le K\|h\|_2$ for some $K\ge0$ ), and invertibility means having a two-sided linear inverse (Invertible Euclidean linear maps).

Proof

technique · reduction

1.1

Define $H:U\to\mathbb R^{m+n}$ by $H(x,y):=(x,F(x,y))$ . From [L2], the remainder after the linear map $(u,v)\mapsto(u,DF(x,y)(u,v))$ is $(0,r(u,v))$ , so $H$ is differentiable with $DH(x,y)(u,v)=(u,D_xF(x,y)u+D_yF(x,y)v).$ Its matrix entries are continuous because those of $DF$ are, so $H$ is $C^1$ . If $B:=D_yF(a,b)^{-1}$ , the displayed derivative at $(a,b)$ has the two-sided inverse $(r,s)\mapsto(r,B(s-D_xF(a,b)r))$ . Thus $DH(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,\psi(x,z))$ . Define $\varphi(x):=\psi(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\iff H(x,y)=(x,0)\iff (x,y)=G(x,0) \iff y=\varphi(x)$ . This proves existence and local uniqueness; $\varphi$ is $C^1$ as a component of $G$ .

step 2.1

4.1

Differentiate $F(x,\varphi(x))=0$ . By [L2], $D_xF(x,\varphi(x))+D_yF(x,\varphi(x))D\varphi(x)=0$ . For $(x,\varphi(x))=G(x,0)$ , the derivative formula in [L1] makes $DH(x,\varphi(x))$ invertible. The block formula of step 1.1 then makes $D_yF(x,\varphi(x))$ invertible: solving $DH(u,v)=(0,s)$ gives $u=0$ and $D_yFv=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

The unit circle is locally a C¹ graph at every point Example

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 105 results over 22 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

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