PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)

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.

A null set has dense complement in a positive-dimensional manifold

Statement

Let $M$ be a positive-dimensional smooth manifold, let $A$ be a smooth atlas on $M$ , and let $E \subseteq M$ be $A$ -null in the sense of Null subsets of a smooth manifold. Then $M ∖ E$ is dense in $M$ . In particular, under Countable Choice the conclusion holds for any manifold-null set $E$ .

Facts & Assumptions

Given: A positive-dimensional smooth manifold $M$ , a smooth atlas $A$ , and an $A$ -null set $E \subseteq M$ .

[L1]

For every chart $(V, φ)$ of $A$ , the image $φ (E \cap V)$ is Euclidean null (Null subsets of a smooth manifold).

[L2]

Every subset of a Euclidean null set is null (Subsets and countable unions of null subsets of $R^{m}$ are null).

Proof

technique · direct

1.1givenassume-contrachoose

Suppose $M ∖ E$ were not dense. Then some nonempty open set $O \subseteq M$ would satisfy $O \subseteq E$ . Choose $p \in O$ and a chart $(V, φ) \in A$ containing $p$ , and put $W = V \cap O$ . Then $φ (W)$ is a nonempty open subset of $R^{m}$ , where $m = \dim M \geq 1$ .

2.1L1L2step 1.1contradiction

Since $W \subseteq E \cap V$ , [L1] and [L2] make $φ (W)$ null. But $φ (W)$ contains a closed cube of positive side length, which has positive $m$ -dimensional volume and cannot be null. Contradiction.

3.1discharge-contradiction: dense complementstep 2.1∎

Hence every nonempty open subset of $M$ meets $M ∖ E$ , so $M ∖ E$ is dense. Under Countable Choice, a manifold-null set has a fixed atlas for which it is $A$ -null by Null subsets of a smooth manifold, so the same conclusion applies.

Depends on

Dependency tree · 2 levels

Sources

John M. Lee, Introduction to Smooth Manifolds, 2nd ed.