Read-back: FredholmBanach.isFredholm_comp

Setting. $\mathbb{K} \in \{\mathbb{R}, \mathbb{C}\}$ (RCLike 𝕜). $E, F, G$ are Banach spaces over $\mathbb{K}$ (normed, CompleteSpace). $u : E \to F$ and $v : F \to G$ are continuous linear maps (implicit arguments).

Definition used: IsFredholm (Mathlib). A continuous linear map $w : X \to Y$ is Fredholm iff all five hold: (i) $w$ is strict (the corestriction $X \to w(X)$ is a topological quotient map, i.e. $w$ is open onto its range with the subspace topology); (ii) $w(X)$ is closed in $Y$; (iii) $\ker w$ is finite-dimensional; (iv) the algebraic quotient $Y / w(X)$ is finite-dimensional (range.CoFG); (v) $\ker w$ admits a continuous linear projection $X \to \ker w$ (topologically complemented).

Hypotheses. hu: $u$ is Fredholm. hv: $v$ is Fredholm.

Conclusion. $v \circ u : E \to G$ (v.comp u) is Fredholm, in the full five-field sense above.

Degenerate cases.

• $u$ or $v$ an isomorphism (≃L): reduces to Fredholmness of the other, up to composition with an isomorphism.
• Finite-dimensional $E, F, G$: every map is Fredholm, so the statement is trivially consistent.
• Any of the spaces zero: e.g. $F = 0$ forces $E$ and $G$ finite-dimensional (by the kernel/cokernel conditions), and the composite is $0 : E \to G$, which is Fredholm.

Remarks. The order of composition is $v \circ u$ (first $u$, then $v$), matching the hypothesis types. Completeness is assumed on all three spaces; the five-field definition itself works without it, so these hypotheses may be stronger than needed for this particular assertion, but that only restricts generality, not correctness. Nothing vacuous or mis-formalized observed.