Fredholm operators form an open set on which the index is locally constant

Proved

FredholmBanach.isOpen_isFredholm_index_locallyConstant

by Mazecto · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

banach-spacescompact-operatorsfredholm-operatorsfunctional-analysisoperator-theory

Let $\mathbb{K}$ be $\mathbb{R}$ or $\mathbb{C}$ and let $E$ , $F$ be Banach spaces over $\mathbb{K}$ . Give the space $\mathcal{L}(E;F)$ of bounded linear maps $E\to F$ the operator-norm topology. Then:

the set of Fredholm operators $E\to F$ is open in $\mathcal{L}(E;F)$ ;
every Fredholm operator $u$ has a neighbourhood in $\mathcal{L}(E;F)$ on which $\operatorname{ind}v=\operatorname{ind}u$ , where $\operatorname{ind}u=\dim\operatorname{Ker}u-\dim(F/\operatorname{Im}u)$ .

Preamble

import Definitions.Def_FredholmBanach_Setting

Formal statement

namespace FredholmBanach

open Topology

/-- Bourbaki, *Théories spectrales*, III, § 4, n° 2, Théorème 1 (TS III.58): the set of Fredholm
operators is open in `L(E; F)`, and the index is locally constant on it. -/
theorem isOpen_isFredholm_index_locallyConstant {𝕜 E F : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E]
    [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] :
    IsOpen {u : E →L[𝕜] F | u.IsFredholm} ∧
      ∀ u : E →L[𝕜] F, u.IsFredholm → ∀ᶠ v in 𝓝 u, index v = index u := by sorry

end FredholmBanach

Source

N. Bourbaki, Théories spectrales, Chapitres III à V, Springer (2023), https://doi.org/10.1007/978-3-031-19505-1, Chapitre III, § 4, n° 2, Théorème 1, p. TS III.58

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Read-back: `FredholmBanach.isOpen_isFredholm_index_locallyConstant`

Setting. $\mathbb{K}$ is $\mathbb{R}$ or $\mathbb{C}$ (RCLike). $E$ , $F$ are normed vector spaces over $\mathbb{K}$ , both complete (Banach spaces). $L(E;F)$ = E →L[𝕜] F is the space of bounded linear maps with the operator-norm topology.

Definitions used.

u.IsFredholm (Mathlib) means all five of: (i) $u$ is a strict map, i.e. $u$ induces a quotient map of topological spaces $E \to u(E)$ (onto its range with the subspace topology); (ii) $u(E)$ is closed in $F$ ; (iii) $\ker u$ is finite-dimensional; (iv) the algebraic quotient $F/u(E)$ is a finitely generated (= finite-dimensional) $\mathbb{K}$ -module; (v) $\ker u$ is topologically complemented, i.e. there is a continuous linear $p : E \to \ker u$ with $p(x)=x$ for $x \in \ker u$ .
index u $= \dim \ker u - \dim (F/u(E)) \in \mathbb{Z}$ , where Module.finrank returns $0$ for an infinite-dimensional space. Sign: kernel minus cokernel.
∀ᶠ v in 𝓝 u, P v: there is a neighbourhood of $u$ in the operator-norm topology (equivalently a ball $\|v-u\|<\varepsilon$ ) on which $P$ holds.

Assertion. Two claims, conjoined:

The set $\{u \in L(E;F) : u \text{ Fredholm}\}$ is open in $L(E;F)$ .
For every Fredholm $u$ , there is a neighbourhood $U$ of $u$ such that $\operatorname{ind} v = \operatorname{ind} u$ for all $v \in U$ .

No hypotheses beyond the setting.

Degenerate cases / remarks.

In claim 2 the neighbourhood is not required to consist of Fredholm maps, but by claim 1 it can be shrunk to do so; hence the index is only compared on Fredholm operators, where it is the genuine index, and the junk value of index on non-Fredholm maps plays no role.
If $E=0$ or $F=0$ , or both finite-dimensional, every map is Fredholm, the set is all of $L(E;F)$ , and the index is the constant $\dim E - \dim F$ ; the statement holds trivially.
If $E$ and $F$ admit no Fredholm maps (e.g. no isomorphism modulo finite dimensions), the set is empty and both claims are vacuous; this is fine.
The index sign is opposite to Bourbaki's convention, which is irrelevant for local constancy.

No mis-formalization detected.

Human review

Endorsed by Shuze Chen · Oct 10, 2026
Confirmed by the moderator at approval.
Endorsed by Mazecto · Oct 10, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Fredholm operators form an open set on which the index is locally constant

Read-back: FredholmBanach.isOpen_isFredholm_index_locallyConstant

Read-back: `FredholmBanach.isOpen_isFredholm_index_locallyConstant`