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

Morse-Sard for smooth manifolds

Statement

Let $F : M \to N$ be a smooth map between smooth manifolds. Then the critical value set of $F$ is a null subset of $N$ .

Facts & Assumptions

Given: A smooth map $F : M \to N$ .

[F1]

The empty fibre case is regular, so if every differential $d F_{p}$ is surjective then every value of $F$ is regular (Regular and critical points and values).

[F2]

The empty subset of any manifold is null (Null subsets of a smooth manifold).

[F3]

The critical value set is the image of the critical locus (The critical locus and critical value set).

[L1]

A countable chart cover detects manifold nullity, and countable unions of manifold null sets are null (A countable chart cover detects manifold null sets, Countable unions and subsets of manifold null sets are null).

[L2]

In Euclidean charts, the critical value set of a smooth map is null (Morse-Sard for Euclidean maps).

Proof

technique · direct

1.1

If $\dim N = 0$ , then every differential [F1, F2, given, cases] $d F_{p} : T_{p} M \to T_{F (p)} N = {0}$ is surjective, so [F1] makes every value of $F$ regular. Thus the critical value set is empty, which is null by [F2]. Assume henceforth that $\dim N > 0$ .

F1F2givencases

2.1

Choose countable smooth atlases ${(U_{i}, φ_{i})}$ on $M$ and [L1, step 1.1, given, choose] ${(V_{j}, ψ_{j})}$ on $N$ detecting nullity by [L1], and refine the source atlas so that each $F (U_{i})$ lies in some $V_{j (i)}$ .

L1step 1.1givenchoose

3.1

For each $i$ , the coordinate representative [L2, step 2.1, algebra]

f_{i} : = ψ_{j (i)} \circ F \circ φ_{i}^{- 1}

is smooth between Euclidean open sets with positive-dimensional target. A point of $U_{i}$ is critical for $F$ exactly when its coordinate representative is critical for $f_{i}$ , because the chart maps have invertible differentials. By [L2], the critical value set of $f_{i}$ is null in $ψ_{j (i)} (V_{j (i)})$ . Therefore $ψ_{j (i)} (F (Crit (F) \cap U_{i}))$ is null for every $i$ .

L2step 2.1algebra

4.1

By [F3], the critical value set of $F$ is the countable union of the sets [F3, L1, step 3.1] $F (Crit (F) \cap U_{i})$ , so [L1] shows that it is null in $N$ .

F3L1step 3.1∎

Depends on

Used by

Regular values have null complement and are dense Corollary
Parametric transversality Theorem

Dependency tree · two levels

19 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

John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (standard reference, not scraped)
Marco Gualtieri, Topology I: Smooth Manifolds, cumulative notes (standard reference, not scraped)