Cofinality (source code)

= Cofinality
{title2=$\operatorname{cf}(\alpha)$}
{wiki}

The cofinality of an ordinal $\alpha$ is the least <order type> of an unbounded subset of $\alpha$, equivalently the least ordinal $\beta$ admitting a cofinal function $\beta\to\alpha$.