Friedman–Moschovakis coding lemma (source code)

= Friedman–Moschovakis coding lemma
{c}

Assume the <axiom of determinacy>. If $\lambda$ is a surjective image of the <Baire space of sequences> and, for every $\xi<\lambda$, the power set $\mathcal P(\xi)$ is a surjective image of that space, then $\mathcal P(\lambda)$ is also a surjective image of it.