A bounded operator between Banach spaces whose range has finite codimension has closed range

Proved

FredholmBanach.isClosed_range_of_finiteDimensional_coker

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}$ . Let $u:E\to F$ be a bounded linear map such that the quotient $F/\operatorname{Im}u$ is finite-dimensional. Then $\operatorname{Im}u$ is closed in $F$ , and $u$ is a strict map: the induced bijection $E/\operatorname{Ker}u\to\operatorname{Im}u$ is a homeomorphism.

Preamble

import Definitions.Def_FredholmBanach_Setting

Formal statement

namespace FredholmBanach

open Topology

/-- Bourbaki, *Théories spectrales*, III, § 3, n° 5, Lemme 6 (TS III.52), for Banach spaces:
if the range of `u` has finite codimension, then it is closed and `u` is a strict map. -/
theorem isClosed_range_of_finiteDimensional_coker {𝕜 E F : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E]
    [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F]
    (u : E →L[𝕜] F) (hu : FiniteDimensional 𝕜 (F ⧸ u.range)) :
    IsClosed (u.range : Set F) ∧ IsStrictMap 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, § 3, n° 5, Lemme 6, p. TS III.52 (stated there for Fréchet spaces)

Read-back

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

Read-back: `FredholmBanach.isClosed_range_of_finiteDimensional_coker`

Setting. $\mathbb{K} \in \{\mathbb{R}, \mathbb{C}\}$ (RCLike 𝕜). $E$ and $F$ are Banach spaces over $\mathbb{K}$ : normed spaces (NormedAddCommGroup, NormedSpace 𝕜) that are complete (CompleteSpace). $u : E \to F$ is a continuous $\mathbb{K}$ -linear map.

Hypothesis. FiniteDimensional 𝕜 (F ⧸ u.range): the algebraic quotient $F/u(E)$ is a finite-dimensional vector space. Equivalently, $u(E)$ has finite (algebraic) codimension in $F$ . Nothing is assumed about closedness of the range or about the kernel.

Conclusion. Both of the following hold:

$u(E)$ is a closed subset of $F$ .
$u$ is a strict map (Topology.IsStrictMap u, resolved via open Topology). By definition this means: the corestriction $E \to u(E)$ , $x \mapsto u(x)$ , is a quotient map when $u(E)$ carries the subspace topology from $F$ . In other words, a subset $V \subseteq u(E)$ is open in $u(E)$ iff $u^{-1}(V)$ is open in $E$ . For linear maps this amounts to: $u$ is open as a map onto its image, so the induced bijection $E/\ker u \to u(E)$ is a homeomorphism.

In plain words. A bounded operator between Banach spaces whose range has finite codimension automatically has closed range, and is open onto that range.

Degenerate cases.

If $u$ is surjective, the hypothesis is trivially satisfied (quotient is $0$ ); the conclusion is that $F$ is closed (trivial) and $u$ is a quotient/open map, i.e. the open mapping theorem.
If $F$ is finite-dimensional, the hypothesis holds for every $u$ ; the conclusion then says every such $u$ has closed range and is strict.
$E = 0$ : range is $\{0\}$ , hypothesis says $F$ is finite-dimensional; conclusion is immediate.

Remarks. The completeness of both $E$ and $F$ is present, which is necessary (the statement fails for incomplete spaces). The hypothesis is about algebraic codimension, which is the intended (Bourbaki Lemme 6) reading. Nothing looks vacuous or mis-formalized.

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

A bounded operator between Banach spaces whose range has finite codimension has closed range

Read-back: FredholmBanach.isClosed_range_of_finiteDimensional_coker

Read-back: `FredholmBanach.isClosed_range_of_finiteDimensional_coker`