Sard--Smale residual regular values for Fredholm maps

Let $\mathrm{Crit}(P)$ be the set where $DP$ is not surjective. By [F2], choose sets $(C_j{)}_{j\in J}$, with $J\subseteq \mathbb{N}$, whose interiors cover $\mathcal{X}$, such that each $C_j$ is closed relative to a normal-form neighbourhood $W_j$ and $P{\mathrm{\mid }}_{C_j}:C_j\to V_j$ is proper into a target chart $V_j$. In particular $\mathcal{X}={\bigcup }_{j\in J}{C}_j$. For empty $\mathcal{X}$ take $J=\mathrm{\varnothing }$.

Put $B_j=P(C_j\cap \mathrm{Crit}(P))$. The fixed-index and differentiability hypotheses of [F3] hold, so each $B_j$ is closed relative to $V_j$ and nowhere dense in $\mathcal{Y}$. Global closedness is unnecessary for meagreness.

A value is nonregular exactly when it is the image of a critical point. Every critical point belongs to some $C_j$, and every point of $B_j$ is a critical value. Hence the nonregular values are exactly ${\bigcup }_j{B}_j$, a meagre subset of $\mathcal{Y}$.

By [F4], the complement of that meagre set is residual, and by step 3.1 it is precisely the set of regular values. This also covers $\mathcal{X}=\mathrm{\varnothing }$ and values outside $P(\mathcal{X})$, whose fibres are empty and hence regular.