Stationary partition at a successor cardinal (source code)

= Stationary partition at a successor cardinal
{title2=$S=\bigsqcup_{\xi<\kappa}S_\xi$}

Every stationary subset of a successor cardinal $\lambda^+$ can be partitioned into $\lambda^+$ disjoint stationary subsets. For each $\beta\in[\lambda,\lambda^+)$ choose a bijection $e_\beta:\lambda\to\beta$. For each $\xi<\lambda^+$, the function $\beta\mapsto e_\beta^{-1}(\xi)$ is regressive on the stationary tail with $\beta>\xi$. The <Fodor lemma> gives a stationary fiber with one value $i_\xi<\lambda$. Some value occurs for $\lambda^+$ many indices, whose fibers are pairwise disjoint. Assign any leftover part of $S$ to one fiber.