Consider any infinite $S \subseteq \mathbb{N}$. I was trying to formally define the function $f_S(k)$ which is the $k$ th minimum of $S$.
(Note: If $z = (x,y)$ is a $2-$tuple, define $z_1 = x, z_2 = y$. Also $g^{(k)}(x) = \underbrace{g \circ g \circ \ldots \circ g (x)}_{k \text{ times}}$ )
I took the following approach:
Define $\sigma(\alpha,T) = (\min T, T - \{\min T\})$. Then, set $f_S(k) = \sigma^{(k)}(S)_1$.
(Note: That first argument $\alpha$ is there only so that I can compose $\sigma$.)
But I have a bit of a problem in here. How do I show that this function exists for all $k$. Like, "after a while", I'm taking very large subsets of $S$. How are we sure that then $|\sigma^{(k)}(S)_2| = \infty$. Even after we take potentially infinitely large subsets of $S$, will we still have an infinite set left?
I realize that induction is a pretty good way here. After $n-1$, we have an infinite set left, so I take $1$ more and still have infinitely many left.
But somehow this still nags me. Is there a way to convincingly show this existence?
You can prove by induction on $n$ that if $S \subseteq \mathbb{N}$ is infinite and $U \subseteq S$ is finite with $|U|=n$, then $S \setminus U$ is infinite.
Now define a function $f_S : \mathbb{N} \to \mathbb{N}$ by letting $$f_S(k) = \min g^{(k)}(S)$$ where $g : \mathcal{P}(\mathbb{N}) \setminus \{ \varnothing \} \to \mathcal{P}(\mathbb{N})$ is the function defined by letting $g(T) = T \setminus \{ \min T \}$ for all inhabited $T \subseteq \mathbb{N}$.
By induction on $k$, you can prove that $f_S(k) = S \setminus U$ for some finite set $U \subseteq S$. Having done this, it follows that $f_S$ indeed is well-defined, and returns the $k^{\text{th}}$-least element of $S$.