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.
and smooth maps between smooth manifolds
Definition
Let and be smooth manifolds, let be a map, let and let , where . For and an open set , a map is of class as follows. When , every such map is declared . When , each component with must be in the sense of maps and multi-index derivative notation in Euclidean space; when this component condition is vacuous. Suppose is continuous at . Then is of class at when there are smooth charts of at and of at with such that the coordinate representative
(The coordinate representation of a map between manifolds) is of class on a neighbourhood of in this componentwise Euclidean sense. By Chart independence of smoothness ↗, this condition is independent of the chosen charts: if one such representative is , then every one is, so "some charts" may be read as "any charts". A map is on an open set when it is continuous on and at every point of . A map that is for every finite — equivalently — is called smooth; the term map between smooth manifolds is reserved for the case where is continuous and the representative condition holds at every point of .
Remarks
-
Continuity is part of the hypothesis, not a consequence, at this point. The representative is only a map between open Euclidean sets when is continuous, as The coordinate representation of a map between manifolds records; that Smooth maps are continuous later derives continuity from the representative condition does not change the definition.
-
The choice of charts is discharged. The well-definedness obligation — that testing one chart pair agrees with testing every chart pair — is discharged by Chart independence of smoothness ↗, which is why that lemma is named in
justified_byrather thandeps.