CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-24

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 regular level set is locally a $C^{k}$ graph of dimension $m - n$

Statement

Let $f : U \subseteq R^{m} \to R^{n}$ be $C^{k}$ , $k \geq 1$ , and let $c$ be a regular value. Near each point, a regular level set is a $C^{k}$ graph over $\ker D f (a)$ of dimension $m - n$ .

More precisely, for $a \in f^{- 1} (c)$ put $K = \ker D f (a)$ and $E = K^{⊥}$ , so $R^{m} = K \oplus E$ . There are neighbourhoods $P \subseteq K$ of $0$ and $Q \subseteq E$ of $0$ and a $C^{k}$ map $g : P \to Q$ with $g (0) = 0$ and $D g (0) = 0$ such that, near $a$ , $f^{- 1} (c) = {a + u + g (u) : u \in P} .$ The empty fibre satisfies the regular-value convention vacuously, and when $m = n$ the local graph has zero-dimensional domain and is the isolated point $a$ .

Facts & Assumptions

Given: The stated map, regular value $c$ , and a point $a \in f^{- 1} (c)$ .

[L1]

Surjectivity of $D f (a)$ persists nearby, and a constant-rank level is locally a coordinate slice (Regular and critical points, regular and critical values, and level sets, Differential rank is lower semicontinuous, A constant-rank level set is locally a coordinate slice).

[L2]

If $K$ is a subspace of the finite-dimensional Euclidean inner-product space $R^{m}$ , then $R^{m} = K \oplus K^{⊥}$ ; rank-nullity gives $\dim K = m - n$ , and the inverse function theorem turns an invertible derivative into a local $C^{1}$ diffeomorphism whose inverse is $C^{k}$ when the original map is $C^{k}$ (For a subspace $W$ of a finite-dimensional inner product space, $V = W \oplus W^{⊥}$ , Rank-nullity: $\dim_{F} V = nullity T + rank T$ , The Euclidean inverse function theorem, A local inverse of a $C^{k}$ regular map is $C^{k}$ ).

Proof

technique · direct

1.1givenL1L2construct

By [L1], $f$ has constant rank $n$ near $a$ , and its fibre is a $C^{k}$ coordinate slice. By [L2], put $E = K^{⊥}$ , so $R^{m} = K \oplus E$ and $\dim K = m - n$ .

2.1step 1.1L2algebra

The projection of that slice to $K$ along $E$ has derivative equal to the identity at $a$ : its tangent there is $K$ , because differentiating the normal-form slice and undoing the source coordinates gives $\ker D f (a)$ . By [L2], this projection is a local $C^{k}$ diffeomorphism.

3.1step 2.1algebra

Inverting the projection writes the slice uniquely as $a + u + g (u)$ . Its derivative at $0$ takes values both in $E$ and in the tangent $K$ , so $D g (0) = 0$ ; the zero-dimensional case is the same statement with $P = {0}$ .

4.1step 3.1∎

This gives the asserted graph and dimension at every point of a nonempty regular fibre, while the empty-fibre case is vacuous.

Depends on

Used by

Dependency tree · two levels

36 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. M. Lee, Introduction to Smooth Manifolds, Regular Level Set Theorem (standard reference, not scraped)
L. W. Tu, An Introduction to Manifolds, Section 11.2 (standard reference, not scraped)

A regular level set is locally a CkCk graph of dimension m−nm−n