PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-09-23 (gpt-6-sol)

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.

An equidimensional $C^{1}$ map sends null sets to null sets

Statement

Assume the Axiom of Countable Choice. Let $F : M^{m} \to N^{m}$ be a $C^{1}$ map between smooth manifolds of the same dimension. If $E \subseteq M$ is null, then $F (E) \subseteq N$ is null.

Facts & Assumptions

Given: The Axiom of Countable Choice, a $C^{1}$ map $F : M^{m} \to N^{m}$ and a null subset $E \subseteq M$ .

[L0]

Under Countable Choice, each smooth manifold admits a countable smooth atlas with relatively compact chart domains (Assuming Countable Choice, every smooth manifold admits a countable smooth atlas with relatively compact domains).

[L1]

Under Countable Choice, countable chart atlases of $M$ and $N$ detect manifold nullity (A countable chart cover detects manifold null sets, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[L2]

A continuous derivative is bounded on each compact Euclidean cube, and the mean-value inequality makes its map Lipschitz there (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value, On a convex open set, a uniform bound $∥ D f (z) v ∥_{2} \leq M ∥ v ∥_{2}$ implies $∥ f (y) - f (x) ∥_{2} \leq M ∥ y - x ∥_{2}$ ).

[L3]

A Lipschitz map of all of $R^{m}$ into $R^{m}$ sends null sets to null sets (A Lipschitz map $R^{m} \to R^{m}$ sends null sets to null sets).

Proof

technique · direct

1.1L0L1givencases

If $m = 0$ , then nullity means emptiness by [L1], so $E = \emptyset$ and the claim follows. Assume $m \geq 1$ . By [L0] under the stated Countable Choice, take countable chart atlases $(U_{j}, φ_{j})$ of $M$ and $(V_{k}, ψ_{k})$ of $N$ . For each pair $(j, k)$ , the set $D_{j k} : = φ_{j} (U_{j} \cap F^{- 1} (V_{k}))$ is open in $R^{m}$ and the coordinate map $f_{j k} : = ψ_{k} \circ F \circ φ_{j}^{- 1}$ is $C^{1}$ on $D_{j k}$ .

2.1L1L2L3step 1.1construct

For every $(j, k)$ , enumerate the nondegenerate closed cubes with rational endpoints whose closures lie in $D_{j k}$ . Their interiors cover $D_{j k}$ , and the family is countable. On each such cube $Q$ , [L2] bounds $∥ D f_{j k} ∥$ and makes $f_{j k} ∣_{Q}$ Lipschitz, since $Q$ is convex. Define $π_{Q} : R^{m} \to Q$ by clamping each coordinate to its interval; each scalar clamp is $1$ -Lipschitz, so $π_{Q}$ is $1$ -Lipschitz in Euclidean norm and fixes $Q$ . Hence $f_{j k} \circ π_{Q}$ is Lipschitz on all of $R^{m}$ . The set $A_{j k Q} : = φ_{j} (E \cap U_{j}) \cap Q$ is null by [L1], so [L3] makes $f_{j k} (A_{j k Q}) = (f_{j k} \circ π_{Q}) (A_{j k Q})$ null.

3.1L1step 1.1step 2.1algebra∎

Fix $k$ . Every point of $ψ_{k} (F (E) \cap V_{k})$ comes from some $p \in E \cap U_{j} \cap F^{- 1} (V_{k})$ , and $φ_{j} (p)$ lies in the interior of one of the cubes from step 2.1. Thus $ψ_{k} (F (E) \cap V_{k})$ is contained in the countable union of the null sets $f_{j k} (A_{j k Q})$ over $j, Q$ . Countable subadditivity makes it null. Since this holds for each $k$ , [L1] detects $F (E)$ as null in $N$ .

Depends on

Used by

The image of a lower-dimensional C¹ manifold is null Proposition
Cut locus of a point has riemannian volume zero Theorem

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

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)

An equidimensional C1C1 map sends null sets to null sets