Read-back: FredholmBanach.exists_equiv_of_index_eq_zero

Setting. $\mathbb{K} \in \{\mathbb{R}, \mathbb{C}\}$ (RCLike 𝕜). $E, F$ Banach spaces over $\mathbb{K}$ (normed, complete). $u : E \to F$ continuous linear (implicit).

Definitions used.

• IsFredholm (Mathlib): $u$ strict (corestriction onto range is a topological quotient map), closed range, $\dim\ker u < \infty$, algebraic cokernel $F/u(E)$ finite-dimensional, $\ker u$ topologically complemented.
• index u $= \operatorname{finrank}(\ker u) - \operatorname{finrank}(F/u(E))$ in $\mathbb{Z}$ (finrank $=0$ on infinite-dimensional spaces; here both are finite by Fredholmness).
• E ≃L[𝕜] F: a continuous linear equivalence, i.e. a linear bijection that is continuous with continuous inverse (an isomorphism of topological vector spaces).

Hypotheses.

• hu: $u$ is Fredholm.
• h0: $\operatorname{index}(u) = 0$, i.e. $\dim\ker u = \dim F/u(E)$.
• h: $u$ is injective or $u$ is surjective (as a function).

Conclusion. There exists a continuous linear equivalence $e : E \cong F$ whose underlying continuous linear map equals $u$. Equivalently: $u$ itself is bijective and its inverse is continuous.

Degenerate cases.

• $E = F = 0$: trivially true.
• $E, F$ finite-dimensional of equal dimension: index is $0$ for every map; injective or surjective then gives an isomorphism (correct).
• Finite-dimensional spaces of different dimensions: index $\ne 0$, so h0 fails and the statement is vacuous there (fine).

Remarks. The Fredholm hypothesis hu is genuinely needed: without it, an injective non-surjective map with infinite-dimensional cokernel would have junk index $0$ and the conclusion would fail. It is present. The sign convention is irrelevant here since the index is $0$. The conclusion pins $e$ to $u$ (not merely "some isomorphism exists"), which is the intended strength. No mis-formalization observed.