DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-03

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.

Continuously differentiable maps, local inverses, and local diffeomorphisms

Definition

Let $U \subseteq R^{m}$ be open and $f : U \to R^{n}$ . The map $f$ is continuously differentiable, or of class $C^{1}$ , when it is totally differentiable at every point of $U$ and the entries of its derivative matrix are continuous functions on $U$ .

For an open $U \subseteq R^{n}$ and $a \in U$ , a local inverse of $f$ at $a$ is a function $g : W \to V$ for open neighbourhoods $a \in V \subseteq U$ and $f (a) \in W \subseteq R^{n}$ such that $f ∣_{V} : V \to W$ is bijective and $g = (f ∣_{V})^{- 1}$ . If both $f ∣_{V}$ and $g$ are $C^{1}$ , this restriction is a local diffeomorphism at $a$ .

Depends on

Dependency tree · 2 levels

Sources

Tillmann, Notes of Lectures on Multivariable Calculus, Inverse and Implicit Function Theorems