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

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

Statement

Let $F : M \to N$ be a $C^{1}$ local diffeomorphism. For every $p \in M$ there are coordinate neighbourhoods $(U, φ)$ of $p$ and $(V, ψ)$ of $F (p)$ such that $F ∣_{U} : U \to V$ is a diffeomorphism and, for every $A \subseteq U$ , using the closed-cube nullity of Measure zero and content zero in $R^{m}$ by countable and finite cube covers,

$φ (A) is null in R^{n} ⟺ ψ (F (A)) is null in R^{n} .$

For $n = 0$ , “null” means empty.

Facts & Assumptions

Given: A $C^{1}$ local diffeomorphism $F : M \to N$ and $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]

In dimension zero, the nullity convention in the Statement means emptiness.

[L1]

A $C^{1}$ coordinate map has bounded derivative on a compact cube lying in its domain, hence is Lipschitz there (A $C^{1}$ map is locally Lipschitz on compact coordinate subsets).

[L2]

Global Lipschitz maps of $R^{n}$ preserve closed-cube null sets (A Lipschitz map $R^{m} \to R^{m}$ sends null sets to null sets).

Proof

technique · direct

1.1F1givenchoose

By [F1], shrink around $p$ so that $F ∣_{U} : U \to V$ is a diffeomorphism and both $U$ and $V$ are chart domains. The coordinate map $T = ψ \circ F \circ φ^{- 1}$ is a $C^{1}$ diffeomorphism between open subsets $D = φ (U)$ and $E = ψ (V)$ of $R^{n}$ .

2.1F2step 1.1

If $n = 0$ , $T$ is bijective between subsets of the one-point space $R^{0}$ , so a set is empty exactly when its image is empty. This gives the claim in dimension zero.

2.2L1step 1.1construct

Suppose $n > 0$ . Choose a closed coordinate cube $Q \subseteq D$ around $φ (p)$ and a closed coordinate cube $R \subseteq E$ around $T (φ (p))$ , both with interiors containing those points. Shrink $U$ to the preimage of $int Q \cap T^{- 1} (int R)$ and set $V = F (U)$ . The continuous derivatives of $T$ on $Q$ and $T^{- 1}$ on $R$ are bounded; the mean-value inequality on these convex cubes makes the restrictions Lipschitz, as in [L1].

3.1L2step 2.1step 2.2∎

The coordinatewise clamps $r_{Q} : R^{n} \to Q$ and $r_{R} : R^{n} \to R$ are $1$ -Lipschitz. Thus $T \circ r_{Q}$ and $T^{- 1} \circ r_{R}$ are global Lipschitz maps; the first agrees with $T$ on $φ (U) \subseteq Q$ , and the second agrees with $T^{- 1}$ on $ψ (V) \subseteq R$ . Apply [L2] to each. For every $B \subseteq φ (U)$ , $B$ is null if and only if $T (B)$ is null. Taking $B = φ (A)$ and including step 2.1 proves the claim.

Depends on

Used by

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

Dependency tree · two levels

22 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