TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-31

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.

The smooth inverse function theorem on manifolds

Statement

Let $F : M \to N$ be a smooth map and let $p \in M$ . If $d F_{p} : T_{p} M \to T_{F (p)} N$ is an isomorphism, then there are open neighbourhoods $U$ of $p$ and $V$ of $F (p)$ such that $F ∣_{U} : U \to V$ is a diffeomorphism.

Facts & Assumptions

Given: A smooth map $F : M \to N$ and a point $p \in M$ with $d F_{p}$ an isomorphism.

[F1]

The differential of a smooth map is the induced linear map on tangent spaces (The differential of a smooth map).

[L1]

Differentials satisfy the chain rule (The chain rule for differentials of smooth maps).

[L2]

In dimension $n \geq 1$ , a Euclidean $C^{1}$ map with invertible derivative at a point has a local $C^{1}$ inverse (The Euclidean inverse function theorem).

[L3]

If the original Euclidean map is smooth, then its local inverse is smooth (A local inverse of a $C^{k}$ regular map is $C^{k}$ ).

[L4]

Chart maps and their inverses are smooth diffeomorphisms onto open Euclidean sets (Chart maps are diffeomorphisms onto Euclidean open sets).

[L5]

The tangent space of a smooth $n$ -manifold has dimension $n$ , including $n = 0$ (The tangent space of an n-manifold has dimension n).

[L6]

A smooth map is continuous and has smooth coordinate representatives on compatible chart neighbourhoods; maps on open subsets of $R^{0}$ are declared smooth ( $C^{r}$ and smooth maps between smooth manifolds).

Proof

technique · direct

1.1L4L5L6givencasesalgebra

By [L5], the isomorphism $d F_{p}$ implies that $M$ and $N$ have the same dimension $n$ . If $n = 0$ , smooth charts at $p$ and $F (p)$ have nonempty open images in the singleton $R^{0}$ , so their domains are the open singletons $U = {p}$ and $V = {F (p)}$ . The restriction $F ∣_{U} : U \to V$ is bijective, and its inverse has the unique map $R^{0} \to R^{0}$ as its coordinate representative, which is smooth by [L6]. Thus the conclusion holds when $n = 0$ . For the remainder assume $n \geq 1$ .

1.2F1L1L4L6given

Choose smooth charts $(U_{0}, φ)$ at $p$ and $(V_{0}, ψ)$ at $F (p)$ with $F (U_{0}) \subseteq V_{0}$ , as permitted by smoothness in [L6], and let $f : = ψ \circ F \circ φ^{- 1}$ . By [L4], the chart maps $φ^{- 1}$ and $ψ$ are diffeomorphisms, so their differentials are linear isomorphisms. Applying [L1] gives $D f (φ (p)) = d ψ_{F (p)} \circ d F_{p} \circ d (φ^{- 1})_{φ (p)} .$ Because $d F_{p}$ is an isomorphism by [F1], the Euclidean differential $D f (φ (p))$ is invertible.

2.1step 1.1step 1.2L2L3

Since $n \geq 1$ , [L2] applies: after shrinking to open neighbourhoods $\tilde{U} \subseteq φ (U_{0})$ and $\tilde{V} \subseteq ψ (V_{0})$ of $φ (p)$ and $ψ (F (p))$ , the restriction $f ∣ \tilde{U} : \tilde{U} \to \tilde{V}$ is a bijection with $C^{1}$ inverse. Since $f$ is smooth, [L3] upgrades that inverse to a smooth one.

3.1step 2.1L4construct

Put $U : = φ^{- 1} (\tilde{U})$ and $V : = ψ^{- 1} (\tilde{V})$ . Then $F ∣_{U} = ψ^{- 1} \circ (f ∣ \tilde{U}) \circ φ$ , so $F ∣_{U} : U \to V$ is bijective. Its inverse is $φ^{- 1} \circ (f ∣ \tilde{U})^{- 1} \circ ψ$ , which is smooth by [L4] and step 2.1.

4.1step 3.1L4∎

Thus $F ∣_{U}$ is a bijective smooth map with smooth inverse, hence a diffeomorphism of neighbourhoods.

The smooth inverse function theorem on manifolds

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources