DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-31
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 embeddings
Definition
Let be a smooth map. Then is a smooth embedding when
- is injective,
- is an immersion (Immersions, submersions, and constant-rank maps), and
- is a homeomorphism, where carries the subspace topology from (Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological, Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace).
Depends on
- Immersions, submersions, and constant-rank maps
- Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological
- Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace
Used by
- An injective immersion from a compact manifold is an embedding Corollary
- An injective immersion need not be an embedding False statement
- The image of a smooth embedding is an embedded submanifold Proposition
- The inclusion of an embedded submanifold is a smooth embedding Proposition
- The smooth structure of an embedded submanifold is unique Proposition
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
- Will J. Merry, Differential Geometry, Definition 6.1 (standard reference, not scraped)
- John M. Lee, Introduction to Smooth Manifolds, Embeddings (standard reference, not scraped)