PropositionStatement: Literature-sourcedProof: AI-adapted

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 null-set definition is independent of the smooth atlas

Statement

Assume countable choice ${A C}_{ω}$ . If $A$ and $B$ are smooth atlases on the same smooth manifold $M$ , then a subset $E \subseteq M$ is $A$ -null if and only if it is $B$ -null.

Facts & Assumptions

Given: Countable choice and smooth atlases $A$ and $B$ on a smooth manifold $M$ , and a subset $E \subseteq M$ .

[F1]

In positive dimension, a set is atlas-null when every chart image in that atlas is Euclidean null; in dimension zero atlas-nullity means the set is empty (Null subsets of a smooth manifold).

[L1]

For a $C^{1}$ map and prescribed source and target charts, each point of a compact source set has a neighbourhood on whose closure the coordinate representative is Lipschitz (A $C^{1}$ map is locally Lipschitz on compact coordinate subsets).

[F2]

Charts belonging to the same smooth structure have smooth transition maps in their displayed coordinates; in particular the identity map has $C^{1}$ coordinate representatives (Smooth manifolds and their smooth charts, Smoothly compatible charts and the smoothness of Euclidean transition maps).

[F3]

An open subset of a smooth manifold carries its restricted smooth structure (An open subset of a smooth manifold has a canonical restricted smooth structure).

[L4]

Global Lipschitz maps $R^{m} \to R^{m}$ preserve Euclidean null sets, and Euclidean nullity passes to subsets (A Lipschitz map $R^{m} \to R^{m}$ sends null sets to null sets, Measure zero and content zero in $R^{m}$ by countable and finite cube covers).

[L2]

Under countable choice, every manifold open cover has a countable subordinate coordinate-ball cover (Every open cover of a manifold has a countable relatively compact coordinate-ball subcover).

[A1]

Countable choice selects one witness from each set in a countable family of nonempty witness sets; in particular it selects cube-cover sequences for countable null families (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[L3]

A double sequence can be flattened and the geometric budgets $ε 2^{- j - 1}$ sum to $ε$ ( $N \times N \approx N$ , For $∣ r ∣ < 1$ , $\sum_{k \geq 0} r^{k} = 1 / (1 - r)$ , and for $∣ r ∣ \geq 1$ the series diverges).

Proof

technique · direct

1.1F1F2L1givencaseschooseconstruct

If $\dim M = 0$ , [F1] says that either atlas declares $E$ null exactly when $E = \emptyset$ , proving the equivalence. Assume now $m = \dim M \geq 1$ , that $E$ is $A$ -null, and fix $(V, ψ) \in B$ . For $(U, φ) \in A$ and $p \in U \cap V$ , set $T = ψ \circ φ^{- 1}$ on $φ (U \cap V)$ . By [F2], $T$ is $C^{1}$ . Apply [L1] to the identity of $M$ , the restricted source chart $(U \cap V, φ)$ , the target chart $(V, ψ)$ , and the compact set ${p}$ . It supplies an open neighbourhood $O$ of $p$ in $U \cap V$ on whose coordinate closure $T$ is Lipschitz. Choose a closed cube $Q \subseteq φ (O)$ with $φ (p)$ in its interior and put $W = φ^{- 1} (int Q)$ . These $W$ , with all their displayed chart and cube witnesses, form an open cover of $V$ .

2.1F1L4step 1.1constructalgebra

Write $Q = \prod_{i < m} [a_{i}, b_{i}]$ and define $r_{Q} : R^{m} \to Q$ by $(r_{Q} (x))_{i} = \min {b_{i}, \max {a_{i}, x_{i}}}$ . Each scalar clamp changes distances by at most the original distance; summing the squares gives $∥ r_{Q} (x) - r_{Q} (y) ∥_{2} \leq ∥ x - y ∥_{2}$ . Thus $T \circ r_{Q}$ is a global Lipschitz map and agrees with $T$ on $φ (W)$ . Since $φ (E \cap W)$ is a subset of the null set $φ (E \cap U)$ , [L4] gives that $ψ (E \cap W) = (T \circ r_{Q}) (φ (E \cap W))$ is null in the prescribed $ψ$ coordinates.

3.1F3L2A1L4step 1.1step 2.1choose

View $V$ as an open smooth manifold by [F3]. Apply [L2] to its cover from step 1.1, obtaining a finite or countable subordinate coordinate-ball cover $(W_{j})_{j \geq 0}$ , with the empty or finite case handled by empty sets after the last term. Use [A1] to select a containing member $W$ and its chart and cube witnesses for each nonempty $W_{j}$ . By step 2.1 and the subset clause of [L4], $C_{j} = ψ (E \cap W_{j})$ is Euclidean null. Since these sets cover $E \cap V$ , $ψ (E \cap V) = ⋃_{j \geq 0} C_{j}$ .

4.1A1L3step 1.1step 3.1∎

Fix $ε > 0$ . Each null $C_{j}$ admits a sequence of closed-cube covers with total volume at most $ε 2^{- j - 1}$ . Use [A1] to choose these sequences simultaneously. Flatten them by [L3]; the resulting sequence covers $⋃_{j} C_{j}$ and has total volume at most $\sum_{j} ε 2^{- j - 1} = ε$ . Thus $ψ (E \cap V)$ is null. Since $(V, ψ)$ was arbitrary, $E$ is $B$ -null. Interchanging $A$ and $B$ gives the reverse implication; step 1.1 already covers dimension zero.

The null-set definition is independent of the smooth atlas

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources