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.
Smooth singular simplex
Definition
Let be a smooth manifold, possibly with boundary. For , put A smooth singular -simplex in is a map for which there are an open set containing and a smooth map with . The simplex and its face maps are The standard topological simplex and its affine face maps. Smoothness into a boundary target is that of Smooth maps between manifolds with boundary.
The extension takes values in on all of , including points outside the simplex. Merely extending its chart coordinates to a Euclidean space with values outside does not suffice. Nor is separate smoothness of the face restrictions the definition. For a boundaryless target this is the usual neighbourhood-extension convention.
Write for this set of maps; the extension itself is not additional simplex data. Every such map is continuous. At , is a point, so every point of is a smooth zero-simplex. Constant maps are smooth in every degree, including maps to a boundary point, and degenerate parametrizations are allowed. The empty manifold has no simplices. No simultaneous choice of extensions is part of this definition.
Depends on
Used by
- A continuous nowhere differentiable singular one simplex Counterexample
- Smooth singular chain and cochain complexes Definition
- Smooth singular simplices in a coordinate ball Example
- Every continuous singular simplex is smooth False statement
- Compatible smooth simplex faces have a neighbourhood extension Lemma
- Relative smoothing of a continuous simplex along its faces Lemma
Dependency tree · two levels
4 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
- DG-16 design; Hatcher/Park control (standard reference, not scraped)