PropositionStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-09-01

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.

A proper injective immersion is a smooth embedding

Statement

Let $F : M \to N$ be a proper injective immersion of smooth manifolds. Then $F$ is a smooth embedding.

Facts & Assumptions

Given: A proper injective immersion $F : M \to N$ .

[F1]

A smooth embedding is an injective immersion that is a homeomorphism onto its image with the subspace topology (Smooth embeddings).

[L1]

Every immersion is locally an embedding (Every immersion is locally an embedding).

[L2]

Smooth maps are continuous, and manifolds are locally compact Hausdorff spaces (Smooth maps are continuous, In a locally compact Hausdorff space every point has a neighbourhood base of compact sets, every open subspace and every closed subspace is locally compact, every open set around a point contains an open set with compact closure inside it, and every compact set sits inside an open set with compact closure).

Proof

technique · direct

1.1

By [L1], each point $p \in M$ has a neighbourhood $U_{p}$ such that $F ∣_{U_{p}}$ is an embedding onto an embedded submanifold of $N$ . In particular, the image of a closed subset of $U_{p}$ is closed in $F (U_{p})$ .

L1given

1.2

By [L2], $F$ is continuous and $M$ is locally compact while $N$ is Hausdorff. A proper continuous map from a locally compact Hausdorff space to a Hausdorff space is closed, so $F$ sends closed sets in $M$ to closed sets in $N$ . Therefore the corestriction $F : M \to F (M)$ is a closed continuous bijection.

L2given

2.1

A closed continuous bijection onto a subspace is a homeomorphism. Thus the corestriction $F : M \to F (M)$ is a homeomorphism, while step 1.1 already gives the local embedded-submanifold model coming from the immersion. By [F1], $F$ is a smooth embedding.

F1step 1.1step 1.2∎

Depends on

Used by

FALSE: every injective immersion is a proper embedding False statement
The weak Whitney proper embedding theorem Theorem

Dependency tree · two levels

26 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

John M. Lee, Introduction to Smooth Manifolds, 2nd ed., Embeddings (standard reference, not scraped)