CorollaryStatement: Literature-sourcedProof: Literature-sourcedPipeline-generatedprecheck 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.

Negative expected dimension forces empty generic intersections

Statement

Let $f : X^{x} \to M^{n}$ and $g : Z^{z} \to M^{n}$ be smooth maps with $x + z < n$ . If $f$ and $g$ are transverse, then $X \times_{M} Z = \emptyset$ . In particular, if $A^{a}, B^{b} \subseteq M^{n}$ are transverse embedded submanifolds with $a + b < n$ , then $A \cap B = \emptyset$ . For the perturbation conclusion assume ${A C}_{ω}$ and fix a closed embedded submanifold $Z \subseteq M$ with $\dim X + \dim Z < n$ . Every strong smooth neighbourhood of $f$ contains a map transverse to $Z$ (Strong Whitney approximation by transverse maps), hence disjoint from $Z$ ; a disjoint homotopic map is supplied by The transversality homotopy theorem. The cited approximation theorem concerns a fixed closed embedded submanifold, not an arbitrary map $g$ .

Facts & Assumptions

Given: Smooth maps $f : X^{x} \to M^{n}$ and $g : Z^{z} \to M^{n}$ with $x + z < n$ , and the transverse case of the statement.

[F1]

$f$ and $g$ are transverse when $d f_{a} (T_{a} X) + d g_{b} (T_{b} Z) = T_{y} M$ at every pair $(a, b)$ with $f (a) = g (b) = y$ (Transverse smooth maps).

[F2]

Embedded submanifolds $A, B \subseteq M$ are transverse when their inclusions are, that is, when $T_{p} A + T_{p} B = T_{p} M$ for every $p \in A \cap B$ (Transverse embedded submanifolds).

[F3]

Assume ${A C}_{ω}$ : every strong smooth neighbourhood of a smooth map $f$ contains a smooth map transverse to a fixed closed embedded submanifold (Strong Whitney approximation by transverse maps).

[F4]

Assume ${A C}_{ω}$ : every smooth map is smoothly homotopic to a smooth map transverse to a fixed closed embedded submanifold (The transversality homotopy theorem, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Proof

technique · direct, by rank counting

1.1F1givenalgebra

Suppose there were $(a, b)$ with $f (a) = g (b) = y$ . Then [F1] gives $T_{y} M = d f_{a} (T_{a} X) + d g_{b} (T_{b} Z)$ ; the right side is the span of the images of vector spaces of dimensions $x$ and $z$ , so its dimension is at most $x + z < n = \dim T_{y} M$ , a contradiction. Hence there are no pairs with $f (a) = g (b)$ and $X \times_{M} Z = \emptyset$ .

2.1F2step 1.1givenalgebra

If $A^{a}, B^{b} \subseteq M$ are transverse embedded submanifolds with $a + b < n$ and $p \in A \cap B$ , then applying 1.1 to the two inclusion maps gives $T_{p} A + T_{p} B = T_{p} M$ with left side of dimension at most $a + b < n$ , a contradiction; hence $A \cap B = \emptyset$ .

3.1F3F4step 1.1step 2.1∎

For the perturbation clause, let a strong neighbourhood of $f$ and a closed embedded $Z$ be given with $\dim X + \dim Z < n$ ; under the stated ${A C}_{ω}$ , by [F3] the neighbourhood contains a smooth map transverse to $Z$ , and by 1.1 that map misses $Z$ , so after an arbitrarily small perturbation the intersection is empty; in the homotopy formulation the transverse representative is supplied by [F4]. The rank count itself uses no choice; ${A C}_{ω}$ is consumed exactly by the approximation and homotopy theorems.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

37 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

Victor Guillemin and Alan Pollack, Differential Topology (Prentice-Hall, 1974; complete 236-page PDF) (standard reference, not scraped)
John Milnor, Topology from the Differentiable Viewpoint (Princeton University Press; complete 76-page PDF, including the appendix Classifying 1-manifolds) (standard reference, not scraped)