Alphabeta MathHow 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.
Regular values have null complement and are dense
Statement
Assume the Axiom of Countable Choice. For a smooth map , the complement of the regular values is a null subset of . In particular, the regular values are dense in .
Facts & Assumptions
Given: Countable Choice and a smooth map .
The complement of the regular values is the critical value set (The critical locus and critical value set).
The critical value set is null (Morse-Sard for smooth manifolds).
In a positive-dimensional manifold, a null set has dense complement (A null set has dense complement in a positive-dimensional manifold).
Proof
By [F1] and [L1] under the stated Countable Choice, the complement of the regular values is null in .
If , [L2] implies that the complement of that null set is dense. If , then is discrete and every value is regular because the target tangent spaces are zero, so the regular-value set is all of and is certainly dense.
Therefore regular values have null complement and are dense.
Depends on
Used by
- Regular values form a dense G_δ set Corollary
- An isolated fixed point splits under perturbation, preserving its index Lemma
- Open manifolds admit exhaustions with no caps Lemma
- Positive smooth collars for strictly plurisubharmonic negative sets Lemma
- Regular exhaustion and Dirichlet solutions on relatively compact surface domains Lemma
- Smooth strict plurisubharmonic regularization of a psh exhaustion Lemma
- The index sum of an outward field is the Gauss degree Lemma
- The local index is additive under a transverse perturbation Lemma
Dependency tree · two levels
16 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
- Encyclopedia of Mathematics, Sard theorem (standard reference, not scraped)