LemmaStatement: Literature-sourcedProof: AI-generatedverified 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 tubular target produces a submersive finite-dimensional perturbation family

Statement

Assume the Axiom of Countable Choice ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $f : M \to N$ be smooth. Then there exist an open ball $B \subseteq R^{m}$ containing $0$ and a smooth family of maps $F : M \times B \to N$ such that $F_{0} = f$ and, for every $p \in M$ , the parameter map $F_{p} : B \to N, a ⟼ F (p, a),$ is a submersion. In particular, the evaluation map $F$ is a submersion, so it is transverse to every closed embedded submanifold $Z \subseteq N$ .

Facts & Assumptions

Given: ${A C}_{ω}$ and a smooth map $f : M \to N$ between smooth boundaryless manifolds.

[L1]

Under ${A C}_{ω}$ , the target $N$ admits a proper smooth Euclidean embedding $e : N ↪ R^{d}$ (The weak Whitney proper embedding theorem).

[L2]

Under ${A C}_{ω}$ , an embedded Euclidean submanifold has a smooth tubular neighbourhood; the normal-addition diffeomorphism makes its bundle projection a smooth submersion (The Euclidean tubular neighbourhood theorem).

[L3]

Under ${A C}_{ω}$ , a smooth partition of unity subordinate to any indexed open cover exists (Smooth partitions of unity exist on manifolds).

[F1]

A smooth family is its evaluation map on the product (Smooth families of maps and their evaluation maps), and a submersion is transverse to every embedded submanifold (A submersion is transverse to every embedded submanifold).

Proof

technique · direct

1.1L1L2given

If $M = \emptyset$ , take the singleton open ball $B = R^{0}$ and the unique empty map $F : M \times B \to N$ ; all assertions are vacuous. Otherwise $N \neq \emptyset$ . Choose a proper embedding $e : N ↪ R^{d}$ by [L1]. Let $U \subseteq R^{d}$ be the open tubular neighbourhood of $e (N)$ from [L2]. The normal-addition diffeomorphism and bundle projection give a smooth retraction $r : U \to N$ with $r \circ e = {id}_{N}$ . Because the normal-bundle projection is a submersion, $r$ is a submersion at every point of $U$ .

2.1L3step 1.1

If $U = R^{d}$ , put $D (p) = 1$ for every $p \in M$ ; otherwise set $D (p) = dist (e (f (p)), R^{d} ∖ U)$ . The complement is closed and $e (f (p)) \in U$ , so $D : M \to (0, \infty)$ is continuous. For each integer $k \geq 1$ put $V_{k} = {p : D (p) > 1 / k}$ . These open sets cover $M$ . Apply [L3] to obtain a locally finite subordinate partition $(ϕ_{k})_{k \geq 1}$ , and set $ε (p) = \sum_{k \geq 1} ϕ_{k} (p) / (2 k)$ . It is smooth and positive because the partition is locally finite and sums to one. If $ϕ_{k} (p) > 0$ , then $p \in V_{k}$ , so $1 / k < D (p)$ ; hence $0 < ε (p) < D (p) / 2$ .

3.1F1step 1.1step 2.1

Take the open unit ball $B \subseteq R^{d}$ and define $F (p, a) = r (e (f (p)) + ε (p) a)$ . For $∣ a ∣ < 1$ , the perturbation has norm less than $D (p) / 2$ , so its argument lies in $U$ ; when $U = R^{d}$ this is automatic. Thus $F$ is smooth on all of $M \times B$ , and $F (p, 0) = r (e (f (p))) = f (p)$ . At every $(p, a)$ the derivative in the parameter direction is $ε (p) d r_{e (f (p)) + ε (p) a}$ , which is surjective because $ε (p) > 0$ and $r$ is a submersion. Hence each parameter map $F_{p}$ and the evaluation map $F$ are submersions.

4.1F1step 1.1step 3.1∎

By [F1], the evaluation map is transverse to every embedded $Z \subseteq N$ , in particular every closed embedded $Z$ . This proves the stated family, including the empty-source case.

Depends on

Used by

Dependency tree · two levels

27 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

Marco Gualtieri, Topology I: Smooth Manifolds, Part 10, Corollary 3.27 (standard reference, not scraped)