PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-01

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 globally one-to-one transverse-fibre submanifold is a graph

Statement

Let $S \subseteq M \times N$ be an embedded submanifold. Assume:

for every $x \in M$ , the vertical fibre ${x} \times N$ meets $S$ in exactly one point; and
$S$ is transverse to every vertical fibre it meets.

Then there is a unique smooth map $f : M \to N$ with $S = Γ_{f}$ .

Facts & Assumptions

Given: An embedded submanifold $S \subseteq M \times N$ satisfying the two displayed hypotheses.

[L1]

The transverse intersection theorem controls the dimension of the intersection with a vertical fibre (Transverse embedded submanifolds intersect in the expected codimension).

[L2]

Once $\dim S = \dim M$ , the local graph proposition applies to each vertical fibre intersection (An $m$ -dimensional submanifold transverse to vertical fibres is locally a graph).

[L3]

A diffeomorphism is a bijective smooth map with smooth inverse (Diffeomorphisms and local diffeomorphisms of manifolds).

Proof

technique · direct

1.1

Let $(x, y) \in S$ . The fibre hypothesis gives $S \cap ({x} \times N) = {(x, y)}$ . Because that intersection is a single point, it is $0$ -dimensional. The vertical fibre has codimension $\dim M$ in $M \times N$ , so [L1] forces ${codim}_{M \times N} S = \dim N$ , hence $\dim S = \dim M$ .

L1givenalgebra

2.1

Let $π_{M} : S \to M$ be the restriction of the first projection. By the fibre hypothesis, $π_{M}$ is bijective. Since step 1.1 gives $\dim S = \dim M$ and $S$ is transverse to every vertical fibre it meets, [L2] shows that every point of $S$ has a neighbourhood on which $π_{M}$ is a diffeomorphism onto an open set of $M$ .

L2step 1.1given

3.1

The local inverses from step 2.1 agree on overlaps because $π_{M}$ is globally one-to-one. Therefore they glue to a smooth inverse $π_{M}^{- 1} : M \to S$ , so [L3] makes $π_{M}$ a diffeomorphism.

L3step 2.1

4.1

Define $f : = π_{N} \circ π_{M}^{- 1} : M \to N$ . Then every point of $S$ has the form $(x, f (x))$ , and uniqueness of the point in each fibre shows that no other point lies over $x$ . Hence $S = Γ_{f}$ , uniquely.

step 3.1construct∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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