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.
Positive open-set and metric-ball volume
Statement
Let be positive smooth. Every nonempty open has . If induces the manifold topology, then for every and the ball is Borel and has positive measure. If its closure in is compact, it also has finite measure.
Facts & Assumptions
Given: Assume . Manifolds are Hausdorff, second countable and smooth, with boundary allowed; is allowed unless excluded. Densities are pointwise Borel, , and . Nonempty open set; topology-compatible positive-radius ball.
Positive smooth densities give Radon volume: Positive smooth densities give compact-finite Borel measures.
Intrinsic density measure and its chart restriction: The measure in any chart is its coefficient integral.
A box in with parameters is Lebesgue measurable of measure , whichever of its faces are included: A nondegenerate coordinate box has positive measure, equal to its volume.
Proof
Choose and a chart around it restricted inside . For , continuity and give a relative coordinate neighborhood where . This neighborhood contains a closed nondegenerate Euclidean box in the interior of the half-space: even if is on the face, move its last coordinate a sufficiently small positive distance and choose a still smaller box. Hence .
For the singleton is open with measure , so again . The empty manifold has no nonempty open subset, making this clause vacuous.
If , then and the triangle inequality gives . Thus the ball is open in the metric topology, hence in the manifold topology and Borel. It contains since , so the preceding positivity applies. If is compact, monotonicity and compact-finiteness give .
Depends on
Used by
Dependency tree · two levels
33 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
- Folland, Real Analysis, second edition, §11.4 pp.361–363; Theorems 2.14–2.15 pp.50–51 (standard reference, not scraped)