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 be a positive-dimensional smooth manifold, let be a smooth atlas on , and let be -null in the sense of Null subsets of a smooth manifold. Then is dense in . In particular, under Countable Choice the conclusion holds for any manifold-null set .
Facts & Assumptions
Given: A positive-dimensional smooth manifold , a smooth atlas , and an -null set .
For every chart of , the image is Euclidean null (Null subsets of a smooth manifold).
Every subset of a Euclidean null set is null (Subsets and countable unions of null subsets of are null).
Proof
Suppose were not dense. Then some nonempty open set would satisfy . Choose and a chart containing , and put . Then is a nonempty open subset of , where .
Since , [L1] and [L2] make null. But contains a closed cube of positive side length, which has positive -dimensional volume and cannot be null. Contradiction.
Hence every nonempty open subset of meets , so is dense. Under Countable Choice, a manifold-null set has a fixed atlas for which it is -null by Null subsets of a smooth manifold, so the same conclusion applies.
Depends on
Used by
- A smooth map from lower to higher dimension cannot be surjective Corollary
- Regular values have null complement and are dense Corollary
- Transitive smooth actions identify M with G/H Corollary
- A collared Whitney disk can avoid an entire compact immersed image Lemma
- A generic linear projection preserves injectivity and immersion Lemma
- A small regular homotopy removes triple images and preserves transverse branch pairs Lemma
- Algebraic open inclusions surject on fundamental groups Lemma
- Every bordism class is realized by an embedded collapse Lemma
- Finite general position for a leafwise loop Lemma
- General position makes a Whitney disk embedded and interior-disjoint in the stable range Lemma
- Metastable approximation of maps by embeddings Lemma
- Moving a sphere off a lower-dimensional submanifold Lemma
- The mod-two degree is well defined and homotopy invariant Lemma
- Transverse based homotopies give normal cobordisms Lemma
- Relative transversality preserves a map on a closed good region Proposition
- Surgery below the middle dimension improves connectivity Proposition
- Every smooth function admits arbitrarily fine strong-topology perturbations whose differential is transverse to zero, supported away from a closed set where transversality already holds Theorem
Dependency tree · two levels
18 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
- John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (standard reference, not scraped)