Theorem 9.8 — the invertible operators form an open set

Proved

Rudin.ch09_invertible_open

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

analysislinear-algebra

Let $\Omega$ be the set of invertible linear operators on $\mathbb{R}^n$ . If $A \in \Omega$ and $\|B - A\|\,\|A^{-1}\| < 1$ then $B \in \Omega$ ; consequently $\Omega$ is open in $L(\mathbb{R}^n)$ , and the map $A \mapsto A^{-1}$ is continuous on $\Omega$ .

Preamble

import Mathlib

open Filter Topology

Formal statement

namespace Rudin

/-- Rudin, Theorem 9.8: the set `Ω` of invertible linear operators on `ℝⁿ` is open — indeed
`B ∈ Ω` whenever `‖B - A‖ ‖A⁻¹‖ < 1` for some `A ∈ Ω` — and inversion is continuous on `Ω`. -/
theorem ch09_invertible_open (n : ℕ)
    (inv : (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n)) →
      (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n)))
    (hinv : ∀ A : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n),
      Function.Bijective A → (∀ x, inv A (A x) = x) ∧ ∀ y, A (inv A y) = y) :
    (∀ A B : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n),
        Function.Bijective A → ‖B - A‖ * ‖inv A‖ < 1 → Function.Bijective B) ∧
    IsOpen {A : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n) | Function.Bijective A} ∧
    ContinuousOn inv {A | Function.Bijective A} := by sorry

end Rudin

Source

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

Read-back

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

Fix $n \in \mathbb{N}$ and work with continuous linear operators on $\mathbb{R}^n$ (with the operator norm). Let $\mathrm{inv}$ be given data: a function assigning to each such operator $A$ another one, subject to the hypothesis that whenever $A$ is bijective, $\mathrm{inv}(A)$ is a two-sided inverse of $A$ , i.e. $\mathrm{inv}(A)(Ax) = x$ for all $x$ and $A(\mathrm{inv}(A)y) = y$ for all $y$ . (For non-bijective $A$ the value $\mathrm{inv}(A)$ is unconstrained.) Then three assertions hold:

For all operators $A,B$ : if $A$ is bijective and $\lVert B - A\rVert \cdot \lVert \mathrm{inv}(A)\rVert < 1$ , then $B$ is bijective;
the set $\{A : A \text{ bijective}\}$ is open in the operator norm topology;
$\mathrm{inv}$ is continuous on that set (relative continuity at each bijective operator).

Bijectivity here is bijectivity of the underlying map. The statement is conditional on the existence of the inverse-assigning function $\mathrm{inv}$ supplied as a hypothesis; nothing is asserted about a canonical choice. The case $n=0$ is included, where the only operator is bijective.

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