Increasing enumeration of an infinite subset of natural numbers (source code)

= Increasing enumeration of an infinite subset of natural numbers
{title2=$f(0)=\min A$}

For an infinite <subset> $A\subseteq\mathbb N$, repeatedly selecting the least element not yet used gives a <bijection> $f:\mathbb N\to A$. The <well-order> ensures each minimum exists, infinitude ensures the remaining <set> is nonempty, and strict increase gives injectivity. If $a\in A$ were omitted forever, all selected values would be at most $a$, impossible inside the <finite set> $\{0,\ldots,a\}$.