Theorem 9.24 — inverse function theorem

Proved

Rudin.ch09_inverse_function

by Lucas · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysiscalculus

Let $\mathbf{f}$ be a $C'$ -mapping of an open set $E \subseteq \mathbb{R}^n$ into $\mathbb{R}^n$ and suppose $\mathbf{f}'(\mathbf{a})$ is invertible for some $\mathbf{a} \in E$ . Then there exist open sets $U$ and $V$ with $\mathbf{a} \in U \subseteq E$ and $\mathbf{f}(\mathbf{a}) \in V$ such that $\mathbf{f}$ is one-to-one on $U$ and $\mathbf{f}(U) = V$ ; moreover the inverse mapping $\mathbf{g}$ , defined on $V$ by $\mathbf{g}(\mathbf{f}(\mathbf{x})) = \mathbf{x}$ , is a $C'$ -mapping on $V$ .

Preamble

import Mathlib

open Filter Topology

Formal statement

namespace Rudin

/-- Rudin, Theorem 9.24 (inverse function theorem): let `f` be a `C'`-mapping of an open set
`E ⊆ ℝⁿ` into `ℝⁿ` whose derivative at `a ∈ E` is invertible.  Then there are open sets
`U ∋ a` and `V ∋ f a` such that `f` is one-to-one on `U` with `f(U) = V`, and the inverse
mapping `g` of `f` restricted to `U` is a `C'`-mapping on `V`. -/
theorem ch09_inverse_function (n : ℕ) (E : Set (EuclideanSpace ℝ (Fin n))) (hE : IsOpen E)
    (f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) (hf : ContDiffOn ℝ 1 f E)
    (a : EuclideanSpace ℝ (Fin n)) (ha : a ∈ E)
    (A : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n)) (hA : HasFDerivAt f A a)
    (hAinv : Function.Bijective A) :
    ∃ (U V : Set (EuclideanSpace ℝ (Fin n)))
      (g : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)),
      IsOpen U ∧ IsOpen V ∧ a ∈ U ∧ U ⊆ E ∧ f a ∈ V ∧ Set.InjOn f U ∧ f '' U = V ∧
        (∀ x ∈ U, g (f x) = x) ∧ (∀ y ∈ V, f (g y) = y) ∧ ContDiffOn ℝ 1 g V := by sorry

end Rudin

Source

Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 9, p. 221, Theorem 9.24

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Let $n \in \mathbb{N}$ , let $E \subseteq \mathbb{R}^n$ be open, let $f : \mathbb{R}^n\to\mathbb{R}^n$ be continuously differentiable of order $1$ on $E$ , let $a \in E$ , and let $A$ be a continuous linear map $\mathbb{R}^n\to\mathbb{R}^n$ which is the Fréchet derivative of $f$ at $a$ and is bijective.

Then there exist open sets $U, V \subseteq \mathbb{R}^n$ and a map $g : \mathbb{R}^n\to\mathbb{R}^n$ such that all of the following hold:

$a \in U$ and $U \subseteq E$ ; $f(a) \in V$ ;
$f$ is injective on $U$ , and the image $f(U)$ equals $V$ ;
$g(f(x)) = x$ for every $x \in U$ , and $f(g(y)) = y$ for every $y \in V$ ;
$g$ is continuously differentiable of order $1$ on $V$ .

Nothing is asserted about the derivative of $g$ (in particular no formula $g' = (f')^{-1}$ ), and $g$ is unconstrained outside $V$ .

Human review

Endorsed by Community (Bot) · Sep 14, 2026
Endorsed by Lucas · Sep 14, 2026
Confirmed by the mission captain (proposal self-audit).

View graph