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

The image of a lower-dimensional $C^{1}$ manifold is null

Statement

Let $P^{m}$ and $N^{n}$ be smooth manifolds with $m < n$ , and let $F : P \to N$ be a $C^{1}$ map. Then $F (P) \subseteq N$ is a null subset of $N$ .

Facts & Assumptions

Given: A $C^{1}$ map $F : P^{m} \to N^{n}$ with $m < n$ .

[L1]

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

[L2]

A countable chart cover detects manifold nullity (A countable chart cover detects manifold null sets).

[L3]

Every smooth manifold admits a countable smooth atlas with relatively compact domains (Every smooth manifold admits a countable smooth atlas with relatively compact domains).

Proof

technique · direct

1.1

Choose countable smooth atlases ${(U_{i}, φ_{i})}$ on $P$ and ${(V_{j}, ψ_{j})}$ on $N$ as in [L3], and replace each $U_{i}$ by the countable family of intersections $U_{i} \cap F^{- 1} (V_{j})$ . It is enough to show that $F (U)$ is null for each resulting chart domain $U$ , because those domains still cover $P$ and $F (P)$ is the countable union of the sets $F (U)$ .

L3givenchoose

2.1

Fix such a chart $U$ with coordinates $φ : U \to Ω \subseteq R^{m}$ and with $F (U) \subseteq V$ for some target chart $(V, ψ)$ . Define $\tilde{F} : Ω \times R^{n - m} \to R^{n}, \tilde{F} (u, z) : = (ψ \circ F \circ φ^{- 1}) (u) .$ The slice $Ω \times {0}$ is a null subset of $R^{n}$ , and $\tilde{F}$ is $C^{1}$ . By [L1], $\tilde{F} (Ω \times {0}) = ψ (F (U))$ is null.

L1step 1.1construct

3.1

Therefore $F (U)$ is null in the target chart $V$ . Since the atlas on $N$ from step 1.1 detects nullity by [L2], each set $F (U)$ is null in $N$ , and then the countable union from step 1.1 shows that $F (P)$ is null in $N$ .

L2step 1.1step 2.1∎

Depends on

Used by

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)

The image of a lower-dimensional C1C1 manifold is null