LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-01

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.

Sard on the nonflat critical strata

Statement

Let $n \geq 1$ , let $U \subseteq R^{m}$ be open, let $f : U \to R^{n}$ be $C^{r}$ , and for $j \geq 1$ define

C_{j} : = {x \in U : D^{α} f (x) = 0 for every multi-index 1 \leq ∣ α ∣ \leq j} .

If $1 \leq j < r$ , $K \subseteq C_{j} ∖ C_{j + 1}$ is compact, and the Morse-Sard conclusion is already known for $C^{r - j}$ maps from open subsets of $R^{m - 1}$ to $R^{n}$ , then $f (K)$ is null.

Facts & Assumptions

Given: An integer $n \geq 1$ , a $C^{r}$ map $f : U \to R^{n}$ , an integer $1 \leq j < r$ , and a compact set $K \subseteq C_{j} ∖ C_{j + 1}$ .

[L1]

If a Euclidean map has invertible derivative at a point, it becomes a coordinate there after shrinking (The Euclidean inverse function theorem).

Proof

technique · direct

1.1

Fix $x \in K$ . [L1, given, choose] Because $x \notin C_{j + 1}$ , some partial derivative of order $j + 1$ of some component of $f$ is nonzero at $x$ . After reordering coordinates and components, choose a multi-index $α$ with $∣ α ∣ = j$ and a component $f^{μ}$ such that, for

g : = D^{α} f^{μ},

one has $\partial g / \partial x^{1} (x) \neq 0$ . Since $g$ is $C^{r - j}$ , [L1] applied to

Φ_{x} (y) : = (g (y), y^{2}, \dots, y^{m})

gives a neighbourhood $W_{x}$ of $x$ and a $C^{r - j}$ diffeomorphism from $W_{x}$ onto an open set $I_{x} \times Ω_{x} \subseteq R \times R^{m - 1}$ .

L1givenchoose

2.1

Every point of $K \cap W_{x}$ lies in $C_{j}$ , so $g$ vanishes there by definition of $C_{j}$ . [step 1.1, algebra] Hence

Φ_{x} (K \cap W_{x}) \subseteq {0} \times Ω_{x} .

Define

h_{x} : Ω_{x} \to R^{n}, h_{x} (u) : = f ⁣ (Φ_{x}^{- 1} (0, u)) .

This map is $C^{r - j}$ . If $q = Φ_{x}^{- 1} (0, u) \in K \cap W_{x}$ , then $q \in C_{j}$ and $j \geq 1$ , so $D f_{q} = 0$ . Therefore

D h_{x} (u) = D f_{q} \circ D (Φ_{x}^{- 1} ∣_{{0} \times Ω_{x}})_{u} = 0,

so $u$ is a critical point of $h_{x}$ . The induction hypothesis therefore gives that

f (K \cap W_{x}) = h_{x} (Φ_{x} (K \cap W_{x}))

is a null subset of $R^{n}$ .

step 1.1algebra

3.1

Finitely many neighbourhoods $W_{x}$ cover the compact set $K$ , so $f (K)$ is a finite union of null sets and therefore null.

step 2.1givenchoose∎

Depends on

The Euclidean inverse function theorem

Used by

Morse-Sard for Euclidean maps Theorem

Dependency tree · two levels

12 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

Marco Gualtieri, Topology I: Smooth Manifolds, cumulative notes (standard reference, not scraped)