LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 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.

Slice-chart restrictions form a smooth atlas

Statement

Let $S \subseteq M^{m}$ be an embedded $k$ -submanifold. For each slice chart $φ : U \to φ (U)$ , restrict $φ$ to $U \cap S$ and identify $φ (U) \cap (R^{k} \times {0})$ with an open subset of $R^{k}$ by projection onto the first $k$ coordinates. These restricted charts are smoothly compatible and generate exactly the subspace topology on $S$ .

Facts & Assumptions

Given: An embedded $k$ -submanifold $S \subseteq M^{m}$ .

[F1]

In a slice chart, $S$ is cut out by the coordinate slice $R^{k} \times {0}$ (Embedded submanifolds and slice charts).

[F2]

The topology on $S$ is the subspace topology inherited from $M$ (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).

[L1]

Chart maps are homeomorphisms onto open Euclidean sets (Chart maps are diffeomorphisms onto Euclidean open sets).

Proof

technique · direct

1.1

Let $φ : U \to φ (U)$ and $ψ : V \to ψ (V)$ be slice charts. By [F1], after projecting away the zero normal coordinates, the overlap transition on $S$ is $x \mapsto π_{k} ⁣ (ψ \circ φ^{- 1} (x, 0))$ , where $π_{k}$ denotes projection onto the first $k$ coordinates. Because $ψ \circ φ^{- 1}$ is a smooth map between open Euclidean sets and restriction to $(x, 0)$ plus projection are smooth, the restricted transition maps are smooth.

F1L1given

2.1

The restricted charts cover $S$ because the slice charts do. Their images are open in $R^{k}$ : indeed $φ (U) \cap (R^{k} \times {0})$ equals $(π_{k} (φ (U) \cap (R^{k} \times {0})), 0)$ , and the slice condition in [F1] says that every point of this set has an ambient product neighbourhood whose first-factor projection stays inside the image.

F1step 1.1

3.1

By [L1], each ambient chart map $φ$ is a homeomorphism, so its restriction identifies $U \cap S$ with $φ (U) \cap (R^{k} \times {0})$ . Therefore the restricted charts make $U \cap S$ open exactly when it is open in the subspace topology from [F2]. The atlas therefore generates precisely the subspace topology on $S$ .

F2L1step 2.1

4.1

Steps 1.1-3.1 prove smooth compatibility and the topology claim.

step 1.1step 2.1step 3.1∎

Depends on

Used by

Smoothness into an embedded submanifold is an initial property Proposition
The inclusion of an embedded submanifold is a smooth embedding Proposition
The smooth structure of an embedded submanifold is unique Proposition

Cited to discharge well-definedness by Embedded submanifolds and slice charts.

Dependency tree · two levels

13 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, Proposition 6.7 (standard reference, not scraped)
John M. Lee, Introduction to Smooth Manifolds, Embedded Submanifolds (standard reference, not scraped)