TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

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.

A split surjective derivative parametrises its level set

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $X$ be a real Banach space (Banach space), let $U \subseteq X$ be open, let $G : U \to R^{m}$ with $m \geq 1$ be of class $C^{1}$ (C k map between Banach spaces, Fréchet derivative between Banach spaces), let $u \in U$ , and suppose $D G (u) : X \to R^{m}$ is surjective. Then there is a finite-dimensional subspace $Y \subseteq X$ such that $X = \ker D G (u) \oplus Y$ is a topological direct sum with $D G (u) ∣_{Y} : Y \to R^{m}$ a bounded linear isomorphism and the coordinate projection onto $Y$ along $\ker D G (u)$ bounded (A complemented closed subspace of a normed space, A closed subspace is complemented exactly when it is the range of a bounded projection). Moreover there are an open $A \subseteq \ker D G (u)$ with $0 \in A$ , an open $B \subseteq Y$ with $0 \in B$ , and a unique $C^{1}$ map $φ : A \to B$ with $φ (0) = 0$ and $D φ (0) = 0$ such that ${z \in u + (A + B) : G (z) = G (u)} = {u + a + φ (a) : a \in A} .$

Facts & Assumptions

Given: A real Banach space $X$ , an open set $U \subseteq X$ , a $C^{1}$ map $G : U \to R^{m}$ with surjective derivative $D G (u)$ at a point $u \in U$ , and the standard unit vectors $e_{0}, \dots, e_{m - 1}$ of $R^{m}$ .

[A1]

The Axiom of Choice: the Axiom of Choice, consumed through the published implicit function theorem, which assumes it; the selections made here itself are finite.

[F1]

Implicit function theorem for Banach spaces: for real Banach spaces $X_{0}, Y, Z$ , an open $W \subseteq X_{0} \times Y$ , a $C^{k}$ map $F : W \to Z$ with $k \geq 1$ , a point $(a_{0}, b_{0}) \in W$ with $F (a_{0}, b_{0}) = 0$ whose partial derivative $D_{Y} F (a_{0}, b_{0}) : Y \to Z$ is a bounded linear isomorphism, there are open $A \subseteq X_{0}$ with $a_{0} \in A$ , $B \subseteq Y$ with $b_{0} \in B$ , and a unique $C^{k}$ map $g : A \to B$ with $g (a_{0}) = b_{0}$ and ${F = 0} \cap (A \times B) = {(a, g (a)) : a \in A}$ ; along the graph $D g (x) = - D_{Y} F (x, g (x))^{- 1} D_{X} F (x, g (x))$ .

[F2]

Fréchet derivative between Banach spaces, C k map between Banach spaces, A bounded linear operator between normed spaces: the Fréchet derivative $D G (u)$ is a bounded linear operator $X \to R^{m}$ , bounded linear operators are continuous, and restrictions of bounded linear operators to subspaces are bounded and linear.

[F3]

The standard list $e : n \to F^{n}$ with $e_{i} (i) = 1_{F}$ and $e_{i} (j) = 0_{F}$ for $j \neq i$ is an ordered basis of $F^{n}$ ; hence $\dim_{F} F^{n} = n$ , and $F^{0}$ is the zero space with basis $\emptyset$ and dimension $0$ , Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis, Linear combination of a finite list, and the span $span (S)$ as the smallest linear subspace containing $S$ : the standard unit vectors $e_{0}, \dots, e_{m - 1}$ form an ordered basis of the function space $R^{m}$ , so every vector of $R^{m}$ is a unique linear combination $\sum_{i < m} a_{i} e_{i}$ , and $R^{m}$ is finite dimensional; the span of a finite list is the set of its linear combinations.

[F4]

Every natural-number-indexed list of nonempty sets has a choice function on its family of values: a finite family of nonempty sets indexed by a natural number has a choice function.

[F5]

A linear map from a finite-dimensional normed space is bounded: a linear map whose domain admits an ordered basis of finite length is bounded.

[F6]

A finite-dimensional normed subspace is closed, Every finite-dimensional normed space is Banach: a finite-dimensional subspace of a normed space is closed, and a finite-dimensional normed space is complete.

[F7]

A closed subspace of a Banach space is Banach, For a map of spaces the following agree: continuity at every point, preimages of open sets open, preimages of closed sets closed, preimages of subbasic open sets open, and $f (\overline{A}) \subseteq \overline{f (A)}$ : a closed subspace of a Banach space is a Banach space, and a continuous map pulls closed sets back to closed sets.

[F8]

A complemented closed subspace of a normed space, A closed subspace is complemented exactly when it is the range of a bounded projection: a closed subspace $M$ is complemented when there is a closed subspace $N$ with unique decomposition $x = m + n$ and both coordinate maps bounded; equivalently there is a bounded linear projection $P$ with $P^{2} = P$ and $ran (P) = M$ .

[F9]

Chain sum product and composition rules for Banach derivatives: sums, scalar multiples, compositions of $C^{1}$ maps and derivatives of affine maps are computed by the chain and sum rules, the derivative of a bounded linear map being the map itself.

[F10]

Finite products of Banach spaces are Banach, The standard product norms on a finite product of normed spaces: a finite product of Banach spaces, with a product norm, is a Banach space.

Proof

technique · direct

Given: A real Banach space $X$ , open $U \subseteq X$ , a $C^{1}$ map $G : U \to R^{m}$ with $D G (u)$ surjective at $u \in U$ .

1.1givenF2F3F4F5F6choosealgebra

(Construction of the complement) For each $i < m$ the set $D G (u)^{- 1} ({e_{i}})$ is nonempty by surjectivity, so finite choice [F4] selects $u_{0}, \dots, u_{m - 1} \in X$ with $D G (u) u_{i} = e_{i}$ ; put $Y : = span {u_{0}, \dots, u_{m - 1}}$ [F3]. The $u_{i}$ are linearly independent: if $\sum_{i < m} c_{i} u_{i} = 0$ , then $\sum_{i < m} c_{i} e_{i} = D G (u) 0 = 0$ and the uniqueness of coordinates in the standard basis forces every $c_{i} = 0$ [F3]. Hence $\dim Y = m$ and $D G (u) ∣_{Y} : Y \to R^{m}$ is a linear bijection, bounded as a restriction of the bounded operator $D G (u)$ [F2]; its inverse is a linear map on the finite-dimensional space $R^{m}$ and is bounded by [F5]. Moreover $Y$ is closed in $X$ and complete by [F6].

2.1step 1.1F2F3F7F8algebra

(Topological splitting and the bounded projection) Since $D G (u) ∣_{Y}$ is injective, $\ker D G (u) \cap Y = {0}$ ; since $R^{m}$ is spanned by the $e_{i}$ [F3], every $x \in X$ has $D G (u) x = \sum_{i < m} a_{i} e_{i}$ for unique $a_{i}$ , and with $y : = \sum_{i < m} a_{i} u_{i} \in Y$ one has $D G (u) (x - y) = 0$ , so $x = (x - y) + y \in \ker D G (u) + Y$ ; the sum is therefore direct. The kernel $\ker D G (u)$ is closed, being the preimage of the closed set ${0}$ under the continuous operator $D G (u)$ [F2, F7], hence is a Banach space by [F7]. Define $P : = (D G (u) ∣_{Y})^{- 1} \circ D G (u) : X \to X$ ; it is linear and bounded by step 1.1, it takes values in $Y$ , restricts to the identity on $Y$ , and $\ker P = \ker D G (u)$ , so $P^{2} = P$ and $ran (P) = Y$ . By [F8], $Y$ is complemented by $\ker D G (u)$ with both coordinate projections bounded, so $X = \ker D G (u) \oplus Y$ is a topological direct sum and the coordinate projection onto $Y$ along $\ker D G (u)$ is bounded.

2.2step 1.1F2F9F10construct

(The auxiliary map) The set $W : = {(a, y) \in \ker D G (u) \times Y : u + a + y \in U}$ is open in the Banach space $\ker D G (u) \times Y$ by [F7, F10] and contains $(0, 0)$ because $u \in U$ . Define $F : W \to R^{m}$ , $F (a, y) : = G (u + a + y) - G (u)$ ; the map $(a, y) \mapsto u + a + y$ is affine and $C^{1}$ with derivative $(h, k) \mapsto h + k$ , so $F$ is $C^{1}$ with $F (0, 0) = 0$ and $D F (0, 0) (h, k) = D G (u) (h + k)$ by the chain and sum rules [F9, F2]; the partial derivative in the $y$ -variable is therefore $D_{Y} F (0, 0) = D G (u) ∣_{Y}$ , a bounded linear isomorphism by step 1.1.

3.1step 2.1step 2.2F1algebra

(Applying the implicit function theorem) Apply [F1] with $X_{0} = \ker D G (u)$ , $Y$ , $Z = R^{m}$ , the map $F$ , and the point $(0, 0)$ : by step 2.2 its hypotheses hold, and it provides open $A \subseteq \ker D G (u)$ with $0 \in A$ , open $B \subseteq Y$ with $0 \in B$ , and a unique $C^{1}$ map $φ : A \to B$ with $φ (0) = 0$ and ${F = 0} \cap (A \times B) = {(a, φ (a)) : a \in A}$ . Since $F (a, y) = 0$ means exactly $G (u + a + y) = G (u)$ , the graph identity reads ${z \in u + (A + B) : G (z) = G (u)} = {u + a + φ (a) : a \in A}$ .

4.1step 2.1step 3.1F9algebra

(The derivative at zero vanishes) The graph identity gives $G (u + a + φ (a)) = G (u)$ for every $a \in A$ . The map $h (a) : = u + a + φ (a)$ is $C^{1}$ with $D h (0) = {i d}_{\ker D G (u)} + D φ (0)$ [F9], so the chain rule [F9] gives $D G (u) \circ (i d + D φ (0)) = D (G \circ h) (0) = 0$ as a map $\ker D G (u) \to R^{m}$ . For $a \in \ker D G (u)$ this reads $D φ (0) a \in \ker D G (u)$ because $D G (u) a = 0$ ; as $D φ (0)$ takes values in $Y$ and $\ker D G (u) \cap Y = {0}$ by step 2.1, $D φ (0) a = 0$ for every $a$ , that is $D φ (0) = 0$ .

5.1step 2.1step 3.1step 4.1F1A1∎

(Conclusion) Step 1.1 and step 2.1 supply the finite-dimensional subspace $Y$ with $X = \ker D G (u) \oplus Y$ a topological direct sum, $D G (u) ∣_{Y}$ a bounded linear isomorphism and the coordinate projection onto $Y$ bounded; step 3.1 supplies the open sets $A$ and $B$ and the map $φ$ together with the parametrisation identity; step 4.1 supplies $D φ (0) = 0$ ; and the uniqueness assertion follows because any other $C^{1}$ map with the same set identity satisfies $F (a, ψ (a)) = 0$ on $A$ and hence equals the unique map $φ$ of [F1]. This proves the statement, the Axiom of Choice having been used only through [F1] [A1].

Depends on

Used by

Dependency tree · two levels

81 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

Thomas C. Sideris, Ordinary Differential Equations and Dynamical Systems (complete author-hosted book text) (standard reference, not scraped)
Gerald Teschl, Partial Differential Equations: From Classical to Modern (2026 author manuscript; complete 392-page archived text) (standard reference, not scraped)