LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passverified 2026-09-23 (gpt-6-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 generic projection can preserve properness

Statement

Let $F = (g, ρ) : M \to R^{N} \times R$ be a smooth embedding such that $g (M)$ is bounded and $ρ$ is proper. If a unit vector $u \in S^{N}$ is not parallel to the last-coordinate axis and lies outside the secant and tangent direction images of $F$ , then the orthogonal projection $P_{u} \circ F$ is a proper injective immersion.

Facts & Assumptions

Given: A smooth embedding $F = (g, ρ) : M \to R^{N} \times R$ with $g (M)$ bounded and $ρ$ proper.

[F1]

Secant directions are normalized differences of distinct image points, and tangent directions are normalized images of nonzero tangent vectors (Secant and tangent direction maps of a Euclidean embedding).

Proof

technique · direct

1.1F1givenalgebra

The kernel of the orthogonal projection $P_{u}$ is $R u$ . If distinct points $p, q$ collapsed, then $F (p) - F (q)$ would be a nonzero scalar multiple of $u$ , making $u$ a secant direction up to sign, contrary to the hypothesis. If the differential killed a nonzero tangent vector $v$ , then $d F_{p} (v)$ would lie in $R u$ ; since $F$ is an immersion, this vector is nonzero and makes $u$ a tangent direction up to sign. Thus $P_{u} \circ F$ is injective and immersive directly from [F1], with no generic-existence theorem invoked.

1.2givenconstructalgebra

Let $e = (0, 1)$ be the last-coordinate unit vector and put $e^{'} : = P_{u} (e)$ . The hypothesis that $u$ is not parallel to $e$ is exactly $e^{'} \neq 0$ . Decompose $u^{⊥} = R e^{'} \oplus (e^{'})^{⊥}$ . Since $P_{u} (F (p)) = P_{u} (g (p), 0) + ρ (p) e^{'},$ its $(e^{'})^{⊥}$ -component is bounded. Its scalar component along $e^{'} / ∥ e^{'} ∥$ is $ρ^{'} (p) = ∥ e^{'} ∥ ρ (p) + b (p),$ where $b$ is bounded.

2.1step 1.2given

The function $ρ^{'}$ is proper. Indeed, if $J \subseteq R$ is compact and $∣ b ∣ \leq B$ , then $ρ^{'} (p) \in J$ forces $ρ (p)$ into a bounded closed interval because $∥ e^{'} ∥ > 0$ . Thus $(ρ^{'})^{- 1} (J)$ is a closed subset of the inverse image under the proper map $ρ$ of a compact interval.

3.1step 1.1step 2.1∎

If $K \subseteq u^{⊥}$ is compact, its image under the linear coordinate along $e^{'}$ is compact. Hence $(P_{u} \circ F)^{- 1} (K)$ is a closed subset of the compact set $(ρ^{'})^{- 1} ({pr}_{e^{'}} K)$ and is compact. Therefore $P_{u} \circ F$ is proper. Together with step 1.1, it is a proper injective immersion.

Depends on

Secant and tangent direction maps of a Euclidean embedding

Used by

The weak Whitney proper embedding theorem Theorem

Dependency tree · two levels

4 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., Lemma 6.14 (standard reference, not scraped)