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 exponential domain is open and the exponential map is smooth
Statement
Assume . The exponential domain is an open subset of containing the zero section, and is smooth. Consequently every fibre domain is open in and is smooth.
Facts & Assumptions
Given: The exponential domain and map of a boundaryless smooth manifold with an affine connection.
Domain and exponential map of a connection defines and under .
Under The Axiom of Countable Choice (), Existence uniqueness and smooth dependence of geodesics says that is open in and that is smooth on .
Proof
The map , , is smooth. By [F1] and [F2], , so is open in . Every zero vector lies in because its maximal geodesic is the constant curve on .
The restriction is smooth, and [F1] gives . Hence is smooth. For fixed , is the inverse image of the open set under the smooth linear inclusion and is therefore open in ; the restriction is smooth.
If is empty, then , , and the zero section are empty, and openness and smoothness are vacuous. In dimension zero, is the zero section and ; in dimension one the same slice and composition arguments apply unchanged. The zero-vector case was checked in step 1.1, and time is an interior point of each relevant open interval. The stated is used only through [F1] and [F2] to obtain the global smooth tangent-bundle/geodesic construction; taking a preimage and restricting a map require no further choice.
Depends on
Used by
- Existence of geodesically convex neighborhoods Theorem
- Existence of normal neighborhoods Theorem
- Gauss lemma Theorem
- Hopf–Rinow theorem Theorem
- The differential of exp at zero is the identity Theorem
Dependency tree · two levels
12 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
- Ved Datar, Lectures on Riemannian Geometry, Proposition 17.1.4(1), p.128 (standard reference, not scraped)