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 boundary of a positive-dimensional manifold is a closed embedded smooth (n-1)-manifold
Statement
If has dimension , the restrictions of boundary charts to their faces give the structure of a closed embedded smooth boundaryless -manifold. For , .
Facts & Assumptions
Given: A smooth -manifold with boundary.
The boundary and interior defined in boundary charts are intrinsic (Smooth invariance of the manifold boundary).
Boundary-chart transition maps are smooth in the local-extension sense (Smooth charts, atlases, and structures with boundary).
A submanifold with boundary is embedded when its inclusion into the ambient manifold is a smooth embedding (Embedded smooth submanifolds with boundary).
Proof
Suppose . Restrict each boundary chart to the face . By [L1] these restrictions cover exactly . Their images are open subsets of , and [L2] makes their transition maps smooth restrictions of extensions of the ambient transitions. They therefore define a smooth boundaryless -manifold structure on .
In a boundary chart the inclusion is the coordinate map , so it is a smooth injective immersion and a homeomorphism onto its subspace image. Thus it is a smooth embedding, and [L3] gives the asserted embedded submanifold. The complement is locally , hence open, so is closed. When , the boundary is empty by the stated convention.
Depends on
Used by
- Neat submanifolds of a manifold with boundary Definition
- Smooth collars of a manifold boundary Definition
- The double of a smooth manifold with boundary Definition
- The boundary tangent space is the boundary-tangent hyperplane Proposition
- Boundary-tangent fields have boundary-preserving local two-sided flows Theorem
- Morse-Sard for maps from manifolds with boundary Theorem
Dependency tree · two levels
10 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
- Ioan Mărcuț, Manifolds (2017 lecture notes), §§14.5, 15.1 (standard reference, not scraped)
- Will Merry, Differential Geometry (2021), Lecture 24 (standard reference, not scraped)