LemmaStatement: 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.

The tangent space of a regular level set is the kernel of the constraint derivative

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $X$ be a real Banach space, let $U \subseteq X$ be open, let $G : U \to R^{m}$ 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 the set of derivatives $γ^{'} (0)$ of $C^{1}$ curves $γ : (- ε, ε) \to X$ with $γ (0) = u$ and $G \circ γ$ constant equals $\ker D G (u)$ ; that is, $\ker D G (u)$ is exactly the tangent space of the level set $G^{- 1} (G (u))$ at $u$ .

Facts & Assumptions

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

[F1]

Chain sum product and composition rules for Banach derivatives, C k map between Banach spaces: if $γ$ is $C^{1}$ near $0$ with $γ (0) = u$ and $G$ is $C^{1}$ near $u$ , then $G \circ γ$ is differentiable at $0$ with $(G \circ γ)^{'} (0) = D G (u) γ^{'} (0)$ ; a constant function has derivative $0$ , and a bounded linear map is its own derivative.

[F2]

Regular constraint directions are realised by level-set curves: under AC, given the chart $Y, A, B, φ$ of A split surjective derivative parametrises its level set (which requires $m \geq 1$ ), every $h \in \ker D G (u)$ is realised by a $C^{1}$ curve $c (t) = u + t h + φ (t h)$ with $c (0) = u$ , $c^{'} (0) = h$ and $G (c (t)) = G (u)$ .

[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$ : $R^{0}$ is the zero space, so every map into it is constant.

Proof

technique · direct

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

1.1givenF1

Let $γ : (- ε, ε) \to X$ be $C^{1}$ with $γ (0) = u$ and $G \circ γ$ constant. Then $G \circ γ$ has derivative $0$ at every $t$ , and the chain rule [F1] gives $0 = (G \circ γ)^{'} (0) = D G (u) γ^{'} (0)$ ; hence $γ^{'} (0) \in \ker D G (u)$ .

1.2givenF1F2F3choose

Conversely, let $h \in \ker D G (u)$ . If $m = 0$ , then $G$ is constant by [F3] and $\ker D G (u) = X$ . Choose $r > 0$ with $B (u, r) \subseteq U$ and set $ε = r / (2 (1 + ∥ h ∥))$ ; the affine curve $c (t) = u + t h$ lies in $U$ for $∣ t ∣ < ε$ , is $C^{1}$ , and has $c^{'} (0) = h$ by [F1]. If $m \geq 1$ , surjectivity and AC give the chart $Y, A, B, φ$ of the implicit-function theorem in [F2]; applying the realization lemma to this chart gives a $C^{1}$ curve $c$ with $c (0) = u$ , $c^{'} (0) = h$ and $G \circ c$ constant. In either case $h$ is a derivative of the required kind.

2.1step 1.1step 1.2F2∎

Step 1.1 shows that every such derivative lies in $\ker D G (u)$ and step 1.2 shows that every element of $\ker D G (u)$ occurs, so the two sets are equal; this is the assertion, and the Axiom of Choice was used only through the chart and realization lemma in the case $m \geq 1$ [F2].

Depends on

Used by

The differential annihilates the tangent kernel at a constrained extremum Lemma

Dependency tree · two levels

49 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

Gerald Teschl, Partial Differential Equations: From Classical to Modern (2026 author manuscript; complete 392-page archived text) (standard reference, not scraped)
Riccardo Cristoferi, Calculus of Variations: Lecture Notes, Carnegie Mellon University 2016 (complete 133-page notes) (standard reference, not scraped)