PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 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.

An $m$ -dimensional submanifold transverse to vertical fibres is locally a graph

Statement

Let $S \subseteq M \times N$ be an embedded submanifold with $\dim S = \dim M$ , and let $(x_{0}, y_{0}) \in S$ . If $S$ is transverse at $(x_{0}, y_{0})$ to the vertical fibre ${x_{0}} \times N$ , then there exist neighbourhoods $U \subseteq M$ of $x_{0}$ and $V \subseteq N$ of $y_{0}$ and a smooth map $f : U \to V$ such that

S \cap (U \times V) = {(x, f (x)) : x \in U} .

Facts & Assumptions

Given: An embedded submanifold $S \subseteq M \times N$ with $\dim S = \dim M$ , transverse to the vertical fibre ${x_{0}} \times N$ at $(x_{0}, y_{0}) \in S$ .

[F1]

Transversality of embedded submanifolds means that their tangent spaces span the ambient tangent space at the intersection point (Transverse embedded submanifolds).

[L1]

A smooth map with invertible differential at a point is a local diffeomorphism there (The smooth inverse function theorem on manifolds).

Proof

technique · direct

1.1

Let $π_{M} : M \times N \to M$ be the first projection. A tangent vector $v \in T_{(x_{0}, y_{0})} S$ lies in the kernel of $d (π_{M} ∣_{S})_{(x_{0}, y_{0})}$ exactly when it is tangent to the vertical fibre ${x_{0}} \times N$ . By [F1], transversality gives $T_{(x_{0}, y_{0})} S + T_{(x_{0}, y_{0})} ({x_{0}} \times N) = T_{x_{0}} M \times T_{y_{0}} N,$ so $d (π_{M} ∣_{S})_{(x_{0}, y_{0})}$ is surjective. Because $\dim T_{(x_{0}, y_{0})} S = \dim T_{x_{0}} M$ , this surjective linear map is an isomorphism.

F1givenalgebra

2.1

Therefore [L1] gives neighbourhoods $W \subseteq S$ of $(x_{0}, y_{0})$ and $U \subseteq M$ of $x_{0}$ such that $π_{M} ∣_{W} : W \to U$ is a diffeomorphism. Shrinking in the product if necessary, write $W = S \cap (U \times V)$ for some neighbourhood $V$ of $y_{0}$ .

L1step 1.1choose

3.1

Define $f : = π_{N} \circ (π_{M} ∣_{W})^{- 1} : U \to V$ . Then $W = {(x, f (x)) : x \in U},$ so $S$ is locally the graph of $f$ .

step 2.1construct∎

Depends on

Used by

A globally one-to-one transverse-fibre submanifold is a graph Proposition

Dependency tree · two levels

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

An mm-dimensional submanifold transverse to vertical fibres is locally a graph