Set of well-order codes (source code)

= Set of well-order codes
{title2=$\mathrm{WF}$}

The set $\mathrm{WF}\subseteq\omega^\omega$ consists of the reals coding <well-order>[well-orders] of $\omega$. For $x\in\mathrm{WF}$, the norm $\lVert x\rVert$ is the <order type> of the well-order coded by $x$.