LemmaStatement: 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.

Compact transverse complementary intersections are finite

Statement

Let $f : X^{x} \to M^{n}$ be smooth with $X$ compact, let $Z \subseteq M$ be a closed embedded submanifold, and suppose $f$ is transverse to $Z$ with $x + \dim Z = n$ . Then $f^{- 1} (Z)$ is finite (possibly empty), so $# f^{- 1} (Z)$ is a well-defined nonnegative integer. Likewise, if $A^{a}, B^{b} \subseteq M$ are transverse embedded submanifolds of $M$ with $a + b = n$ and one of $A, B$ is compact while the other is closed, then $A \cap B$ is finite. Both compactness of the relevant source and closedness of the other factor are used: a zero-dimensional manifold is discrete, and a compact discrete space is finite.

Facts & Assumptions

Given: A smooth map $f : X^{x} \to M^{n}$ with $X$ compact, $Z \subseteq M$ a closed embedded submanifold, $f ⋔ Z$ and $x + \dim Z = n$ ; and the corresponding submanifold situation.

[F1]

Under these hypotheses $f^{- 1} (Z)$ is identified with $X \times_{M} Z$ by $p \mapsto (p, f (p))$ ; projection to $X$ is its inverse. It is a $0$ -dimensional embedded submanifold of $X$ by The transverse preimage theorem; in a slice chart with $k = 0$ each point is an isolated point of $f^{- 1} (Z)$ , with the subspace topology (Transverse complementary-dimensional intersection sets, Embedded submanifolds and slice charts, Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace).

[F2]

Preimages of closed sets under continuous maps are closed; the points of $X$ with $f (x) \in Z$ form the preimage of the closed set $Z$ (For a map of spaces the following agree: continuity at every point, preimages of open sets open, preimages of closed sets closed, preimages of subbasic open sets open, and $f (\overline{A}) \subseteq \overline{f (A)}$ ).

[F3]

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

[F4]

A compact discrete topological space is finite: its singleton open cover has a finite subcover, whose union is a finite set equal to the whole space; the discrete topology on an infinite set is not compact (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right).

Proof

technique · direct, from discreteness and compactness

1.1F1given

By [F1] the set $f^{- 1} (Z)$ is a $0$ -dimensional embedded submanifold of $X$ , hence discrete in its subspace topology: each of its points has a slice chart in which it is the only point of the set in that chart.

2.1F2F3F4step 1.1given

The set $f^{- 1} (Z)$ is the preimage of the closed set $Z$ under the continuous map $f$ , since smooth maps are continuous, hence closed in $X$ by [F2], hence compact by compactness of $X$ and [F3]. A compact discrete space is finite by [F4], so $# f^{- 1} (Z)$ is a well-defined nonnegative integer; the empty case is included.

3.1step 2.1givenalgebra∎

For the submanifold case, apply the map case to the inclusion of the compact factor: if $A$ is compact and $B$ is closed in $M$ , then the inclusion $i_{A} : A \to M$ is smooth with $A$ compact, $i_{A} ⋔ B$ because $A ⋔ B$ , and $i_{A}^{- 1} (B) = A \cap B$ , so 2.1 gives that $A \cap B$ is finite; the roles of $A$ and $B$ may be exchanged. No choice axiom is used.

Depends on

Used by

The mod 2 intersection number Definition
The oriented intersection number Definition
The mod 2 intersection number is homotopy invariant Theorem

Dependency tree · two levels

28 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)