Let $n$ be a \reftext{def:natural-numbers-2026a}{natural number}, let $U$ be an \reftext{def:open-subset-euclidean-space-2026a}{open} subset of \reftext{def:euclidean-space-rn-2026a}{Euclidean space} $\mathbb{R}^n$, and let $f:U\to\mathbb{R}^n$ be a \reftext{def:c1-map-euclidean-open-set-2026a}{$C^1$ map}. Let $a\in U$, and suppose that the \reftext{def:jacobian-determinant-euclidean-open-set-2026a}{Jacobian determinant} satisfies $\det J_f(a)\ne 0$. Then $f$ is a \reftext{def:locally-invertible-c1-map-euclidean-open-set-2026a}{local $C^1$ diffeomorphism} at $a$.