TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-22

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.

Implicit function theorem for Banach spaces

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $X$ , $Y$ , $Z$ be real Banach spaces, let $U \subseteq X \times Y$ be open for the product metric, let $F : U \to Z$ be of class $C^{k}$ with $k \geq 1$ (C k map between Banach spaces), and let $(a, b) \in U$ with $F (a, b) = 0$ . Let $D_{X} F (a, b) : = D F (a, b) \circ i_{X}$ and $D_{Y} F (a, b) : = D F (a, b) \circ i_{Y}$ be the partial derivatives, where $i_{X} (x) : = (x, 0)$ and $i_{Y} (y) : = (0, y)$ . If $D_{Y} F (a, b) : Y \to Z$ is a bounded linear isomorphism, then there are open neighbourhoods $A \subseteq X$ of $a$ and $B \subseteq Y$ of $b$ and a unique map $g : A \to B$ of class $C^{k}$ such that

${(x, y) \in A \times B : F (x, y) = 0} = {(x, g (x)) : x \in A},$

and along the graph $D g$ satisfies $D g (x) = - D_{Y} F (x, g (x))^{- 1} D_{X} F (x, g (x)) (x \in A) .$ In particular $g (a) = b$ .

Facts & Assumptions

Given: AC, real Banach spaces $X, Y, Z$ , an open $U \subseteq X \times Y$ , a $C^{k}$ map $F : U \to Z$ with $k \geq 1$ , a point $(a, b) \in U$ with $F (a, b) = 0$ , and a bounded linear isomorphism $L : = D_{Y} F (a, b) : Y \to Z$ .

[L1]

Fréchet derivative, partial derivatives as restrictions of $D F$ to the coordinate axes, and the derivative of a bounded linear map (Fréchet derivative between Banach spaces); the product norm $∥ (x, y) ∥_{\max} = \max {∥ x ∥, ∥ y ∥}$ is a norm on $X \times Y$ (The standard product norms on a finite product of normed spaces).

[L2]

Chain rule and sum rule (Chain sum product and composition rules for Banach derivatives).

[L3]

Inverse function theorem: a $C^{k}$ map ( $k \geq 1$ ) between real Banach spaces whose derivative at a point is a bounded linear isomorphism restricts to a $C^{k}$ diffeomorphism between open neighbourhoods of that point and its image (Inverse function theorem for Banach spaces); AC is assumed there and here.

[L4]

Neumann perturbation: an operator close enough to an invertible one is invertible with a norm bound on its inverse (Neumann series and small perturbations of bounded inverses).

[L5]

$C^{k}$ for $k \geq 1$ includes differentiability and continuity of the derivative (C k map between Banach spaces).

[L6]

A closed subset of a complete metric space is complete; a Banach space is complete (Closed subspaces of complete metric spaces are complete; the converse under countable choice, Banach space).

[L7]

The operator norm satisfies $∥ T u ∥ \leq ∥ T ∥ ∥ u ∥$ and $∥ S T ∥ \leq ∥ S ∥ ∥ T ∥$ (The operator norm as the least bound and as the unit-sphere or unit-ball supremum, The spaces (\mathcal B(X,Y)) and (\mathcal B(X)) of bounded linear operators).

Proof

technique · direct

1.1

The product $X \times Y$ with the max norm is complete: a Cauchy sequence in $X \times Y$ has Cauchy coordinate sequences, which converge in the Banach spaces $X$ and $Y$ , and the coordinatewise limit is a limit in the product metric; similarly $X \times Z$ is complete. Hence these products are real Banach spaces, and $U$ is an open subset of the Banach space $X \times Y$ .

L1L6algebra

1.2

Define $Φ : U \to X \times Z$ by $Φ (x, y) : = (x, F (x, y))$ . Its first component is the (bounded, linear) projection $(x, y) \mapsto x$ , and its second is $F$ ; the derivative of a bounded linear map is the map itself by [L1], so $D Φ (a, b) (h, k) = (h, D_{X} F (a, b) h + D_{Y} F (a, b) k)$ , and $D Φ (a, b)$ is a bounded linear isomorphism with inverse $(u, w) \mapsto (u, L^{- 1} (w - D_{X} F (a, b) u))$ .

L1L7algebra

2.1

Since $F$ is of class $C^{k}$ , so is $Φ$ : for $k = 1$ this is the chain rule applied to the two components $x$ and $F$ , and for higher $k$ the same computation differentiates each component, the components of $D^{j} Φ$ being those of $D^{j} x$ and $D^{j} F$ for $j \leq k$ ; continuity of the top derivative is inherited from that of $D^{k} F$ together with the constant derivatives of the linear first component. Also $Φ (a, b) = (a, 0)$ .

step 1.2L2L5algebra

3.1

By [L3] applied to the $C^{k}$ map $Φ$ at $(a, b)$ , whose derivative is the isomorphism of [step 1.2], there are open sets $U_{0} ∋ (a, b)$ and $V_{0} ∋ (a, 0)$ such that $Φ ∣_{U_{0}} : U_{0} \to V_{0}$ is a bijection with $C^{k}$ inverse $Ψ : V_{0} \to U_{0}$ .

step 1.2step 2.1L3

4.1

Because $Φ$ preserves the first coordinate, so does $Ψ$ : if $(x, z) = Φ (x^{'}, y^{'})$ then $x = x^{'}$ , hence $Ψ (x, z) = (x, H (x, z))$ for the $C^{k}$ map $H : = {p r}_{2} \circ Ψ$ ; and $Ψ$ being an inverse of $Φ$ means $F (x, H (x, z)) = z$ for all $(x, z) \in V_{0}$ .

step 3.1algebra

5.1

Choose open $A \subseteq X$ and $B \subseteq Y$ with $A \times B \subseteq U_{0}$ and such that $(a, 0) \in A \times {0} \subseteq V_{0}$ : possible because $U_{0}$ and $V_{0}$ are open and contain $(a, b)$ respectively $(a, 0)$ , and the set ${x : (x, 0) \in V_{0}}$ is an open neighbourhood of $a$ . Shrinking $A$ if necessary we may also assume $g (A) \subseteq B$ : $g$ is continuous at $a$ with $g (a) = b \in B$ and $B$ is open, so some neighbourhood $A_{0}$ of $a$ satisfies $H (A_{0} \times {0}) \subseteq B$ , and we replace $A$ by $A \cap A_{0}$ . Define $g (x) : = H (x, 0)$ for $x \in A$ , so $g$ is of class $C^{k}$ with values in $B$ , $g (a) = b$ , and $F (x, g (x)) = 0$ for every $x \in A$ by [step 4.1].

step 4.1algebra

6.1

Conversely, if $(x, y) \in A \times B$ has $F (x, y) = 0$ , then $Φ (x, y) = (x, 0) \in V_{0}$ , so $(x, y) = Ψ (x, 0) = (x, g (x))$ by [step 4.1] and [step 5.1], and hence $y = g (x)$ . Thus the zero set of $F$ in $A \times B$ is exactly the graph of $g$ , which proves existence and uniqueness of $g$ on $A$ .

step 5.1step 4.1algebra

7.1

For $x \in A$ , differentiate the identity $F (x, g (x)) = 0$ using the chain rule [L2]: $D_{X} F (x, g (x)) + D_{Y} F (x, g (x)) D g (x) = 0$ ; the operator $D_{Y} F (x, g (x))$ is invertible for $x$ close to $a$ by continuity of $D_{Y} F$ at $(a, b)$ (from [L5]) and [L4], and shrinking $A$ if necessary we may assume this holds for all $x \in A$ ; then $D g (x) = - D_{Y} F (x, g (x))^{- 1} D_{X} F (x, g (x))$ , which with [step 6.1] is the displayed formula.

step 5.1step 6.1L2L4L5algebra∎

Depends on

Used by

Dependency tree · two levels

46 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

Zuoqin Wang, Lecture 6 — §3.3 (implicit theorem via the map (x,y) ↦ (x,F(x,y))) (standard reference, not scraped)