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.

$C^{1}$ local diffeomorphisms preserve null sets locally

Statement

Let $F : M \to N$ be a $C^{1}$ local diffeomorphism. For every point $p \in M$ there is an open neighbourhood $U$ of $p$ such that $F ∣_{U} : U \to F (U)$ is a diffeomorphism and, for every $A \subseteq U$ ,

$A is null in M ⟺ F (A) is null in N .$

Facts & Assumptions

Given: A $C^{1}$ local diffeomorphism $F : M \to N$ and a point $p \in M$ .

[F1]

A local diffeomorphism restricts near $p$ to a diffeomorphism onto an open neighbourhood of $F (p)$ (Diffeomorphisms and local diffeomorphisms of manifolds).

[F2]

On a $0$ -manifold, the only null subset is the empty set (Null subsets of a smooth manifold).

[L1]

On compact coordinate pieces, a $C^{1}$ map is locally Lipschitz (A $C^{1}$ map is locally Lipschitz on compact coordinate subsets).

[L2]

Lipschitz maps send Euclidean null sets to Euclidean null sets (A Lipschitz map $R^{m} \to R^{m}$ sends null sets to null sets).

Proof

technique · direct

1.1

By [F1], shrink around $p$ to a neighbourhood $U_{0}$ on which $F$ is a diffeomorphism onto an open set $V_{0}$ .

F1givenchoose

2.1

If $\dim M = 0$ , then $U_{0}$ and $V_{0}$ are $0$ -manifolds. [F2, step 1.1, cases, algebra] By [F2], a subset of $U_{0}$ is null exactly when it is empty, and the same holds in $V_{0}$ ; because $F ∣_{U_{0}}$ is bijective, $A \subseteq U_{0} is null ⟺ A = \emptyset ⟺ F (A) = \emptyset ⟺ F (A) is null .$ So the claim is proved in this case. Assume henceforth that $\dim M > 0$ , and let $A \subseteq U_{0}$ .

F2step 1.1casesalgebra

3.1

Cover $A$ by relatively compact source-chart neighbourhoods $W \subseteq U_{0}$ whose images lie in target charts on $V_{0}$ . [L1, L2, step 2.1, algebra] By [L1], the coordinate representatives of $F ∣_{W}$ and $(F ∣_{W})^{- 1}$ are Lipschitz on smaller compact closures. Therefore [L2] implies $B \subseteq W is null ⟺ F (B) \subseteq F (W) is null$ for each such piece $B$ .

L1L2step 2.1algebra

4.1

The manifold definition of nullity checks exactly these chart images, so [step 3.1] the equivalence in step 3.1 globalizes over $U : = U_{0}$ . Hence $A$ is null in $M$ exactly when $F (A)$ is null in $N$ .

step 3.1∎

Depends on

Used by

The null-set definition is independent of the smooth atlas Proposition

Dependency tree · two levels

20 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)

C1C1 local diffeomorphisms preserve null sets locally