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

Used by

Backpropagation through a finite shared-parameter recurrence Algorithm
Finite-budget bracketing and zoom for a strong Wolfe step Algorithm
Finite-budget direct preference optimization by mini-batch gradient descent Algorithm
Finite-budget forward-difference Newton for a square vector residual Algorithm
Finite-budget inexact Newton–Krylov with a descent safeguard Algorithm
Finite-budget Levenberg-Marquardt with a trust-ratio safeguard Algorithm
Finite-budget multidimensional Krawczyk root certification Algorithm
Finite-budget Newton and chord solves with scheduled factorization reuse Algorithm
Finite-budget Newton for a square vector residual Algorithm
Finite-budget residual-merit damped Newton Algorithm
Fletcher–Reeves and safeguarded Polak–Ribière nonlinear conjugate gradients Algorithm
Forward-difference Jacobian on an open domain Algorithm
Implicit stiff time stepping with a branch and residual ledger Algorithm
Randomized coordinate gradient descent Algorithm
Randomized proximal coordinate descent with certified inner solves Algorithm
Change of variables on bounded open Jordan sets when both integrands are bounded and Riemann integrable Corollary
The finite-basis projector energy model supplies a C1 Hermitian response map Corollary
An invertible derivative at one point does not give a local inverse without C¹ regularity Counterexample
The real complex-squaring map is locally but not globally invertible off the origin Counterexample
x↦ x³ is a C¹ bijection whose inverse is not differentiable at zero Counterexample
A normalizing flow and its base density Definition
C¹ codimension-one regular foliations and transverse orientation Definition
C¹ germs of local diffeomorphisms at a point Definition
Certified differentiable IVP approximation interface for shooting Definition
Cᵏ Euclidean maps and diffeomorphisms Definition
Continuous linearized BVP operator and its conditioning Definition
Finite nonlinear observation designs, local identifiability, and weighted information Definition
Finite parameterized state-step graphs and objectives Definition
Finite straight-line computational programs and real-arithmetic tapes Definition
Real boxes and interval Jacobian enclosures Definition
Smooth bilevel stationary problems and their hypergradients Definition
Smooth hybrid ODE modes, guards, resets, and deterministic event priority Definition
Strictly hyperbolic conservation systems and characteristic families Definition
The Jacobian determinant of a square-dimensional C¹ map is the determinant of its Jacobian matrix Definition
The regular locus of a square-dimensional C¹ map Definition
Wolfe and strong Wolfe line-search conditions Definition
One Robertson reaction step: Newton work and the chord reuse tradeoff Example
The unit circle is locally a C¹ graph at every point Example
FALSE: an everywhere-invertible derivative gives a global inverse False statement
FALSE: an invertible derivative at one point gives a local inverse False statement

…and 40 more results.

Dependency tree · two levels

12 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

Tillmann, Notes of Lectures on Multivariable Calculus, Inverse and Implicit Function Theorems (standard reference, not scraped)