Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: Not applicableSession-authored (Fable 5 assisted)audited 2026-08-29
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.

Cr and smooth maps between smooth manifolds

Definition

Let M and N be smooth manifolds, let F:MN be a map, let pM and let rN0{}, where N0={0,1,2,}. For m,qN0 and an open set ERm, a map g:ERq is of class Cr as follows. When m=0, every such map is declared Cr. When m1, each component gl with l<q must be Cr in the sense of Ck maps and multi-index derivative notation in Euclidean space; when q=0 this component condition is vacuous. Suppose F is continuous at p. Then F is of class Cr at p when there are smooth charts (U,φ) of M at p and (V,ψ) of N at F(p) with F(U)V such that the coordinate representative

ψFφ1:φ(U)ψ(V)

(The coordinate representation of a map between manifolds) is of class Cr on a neighbourhood of φ(p) in this componentwise Euclidean sense. By Chart independence of Cr smoothness , this condition is independent of the chosen charts: if one such representative is Cr, then every one is, so "some charts" may be read as "any charts". A map is Cr on an open set WM when it is continuous on W and Cr at every point of W. A map that is Cr for every finite r — equivalently C — is called smooth; the term Cr map between smooth manifolds is reserved for the case where F is continuous and the representative condition holds at every point of M.

Remarks

  • Continuity is part of the hypothesis, not a consequence, at this point. The representative is only a map between open Euclidean sets when F is continuous, as The coordinate representation of a map between manifolds records; that Smooth maps are continuous later derives continuity from the C1 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 Cr smoothness , which is why that lemma is named in justified_by rather than deps.

Depends on

Used by

Dependency tree · two levels

11 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