CorollaryStatement: Literature-sourcedProof: Literature-sourcedprecheck passjudge pass (gpt-6.1-sol)

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 an embedding

Statement

A proper injective immersion between smooth manifolds is a smooth embedding; this general criterion is choice-free. Assume ${A C}_{ω}$ for the following high-codimension consequences. If $f : M^{m} \to X^{n}$ is a proper self-transverse immersion with $n > 2 m$ , then $f$ is a smooth embedding; if in addition $M$ is closed, self-transversality with $n > 2 m$ alone suffices, properness being automatic.

Facts & Assumptions

Given: The published criterion for proper injective immersions, and (for the stated consequences) countable choice and a self-transverse immersion $f : M^{m} \to X^{n}$ with $n > 2 m$ .

[F1]

A proper injective immersion between smooth manifolds is a smooth embedding (A proper injective immersion is a smooth embedding).

[F2]

A smooth embedding is an injective immersion that is a homeomorphism onto its image with the subspace topology (Smooth embeddings); the phrase is therefore exactly what [F1] concludes for such a map (Immersions, submersions, and constant-rank maps).

[L1]

A self-transverse immersion $f : M^{m} \to X^{n}$ with $n > 2 m$ has empty double point locus and is injective (A self-transverse immersion has no double points when $n > 2 m$ ).

[L2]

A compact subset of a Hausdorff space is closed (In a Hausdorff space a point and a disjoint compact set, and two disjoint compact sets, have disjoint open neighbourhoods; hence every compact subset is closed, and in a compact Hausdorff space the compact subsets are exactly the closed ones).

[L3]

A closed subset of a compact space is compact (A closed subspace of a compact space is compact, and a finite union of compact subspaces is compact).

[L4]

A smooth map of smooth manifolds is continuous (Smooth maps are continuous).

[L5]

A subset is compact when it is compact as a subspace in its own right (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right); a smooth manifold is in particular a Hausdorff topological manifold (Smooth manifolds and their smooth charts).

[A1]

Countable choice is the hypothesis of [L1] and is inherited by the second and third sentences of the statement; the first sentence and the properness computation select nothing (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Proof

technique · direct

1.1F1F2

The general criterion of [F1] is the published proposition cited in [F2]; its conclusion is precisely that a proper injective immersion satisfies the three clauses of [F2] and hence is a smooth embedding.

1.2L2L3L4L5A1

Suppose $M$ is closed, that is, compact without boundary. Every compact subset $K \subseteq X$ is closed by [L2], since a smooth manifold is Hausdorff by [L5]; the preimage $f^{- 1} (K)$ is closed in $M$ because $f$ is continuous by [L4], and a closed subset of the compact space $M$ is compact by [L3]. Hence preimages of compact sets under $f$ are compact, that is, $f$ is proper.

2.1L1A1step 1.1

Assume ${A C}_{ω}$ and let $f : M^{m} \to X^{n}$ be a proper self-transverse immersion with $n > 2 m$ . By [L1] the map $f$ is injective, and $f$ is an immersion and proper by hypothesis, so step 1.1 makes $f$ a smooth embedding.

3.1L1A1step 2.1step 1.2

With $f$ now proper by step 1.2, injective by [L1] and an immersion by hypothesis, step 1.1 applies and shows that a self-transverse immersion $M^{m} \to X^{n}$ with $n > 2 m$ and closed $M$ is a smooth embedding, with no separate properness hypothesis.

4.1step 1.1step 2.1step 3.1∎

The three assertions of the statement are step 1.1, step 2.1 and step 3.1 respectively.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

38 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.