A question about "construction by induction". In Rudin's principle of mathematical analysis or other books, they often write that pick $x_1$ and suppose we have chosen $\{x_1,\dots,x_n\}$, then choose $x_{n+1}$, and says by induction, we have construct a sequence $\{x_n \}_{n=1}^\infty$
For example, if I want to prove: Let $X$ be a metric space and $K \subseteq X$. If every infinite subset of $K$ has an accumulation point in $K$, then $K$ is totally bounded.
Prove it by contradiction. $\exists r \gt0$ s.t. $K$ can not be covered by finitely many open balls centered in $K$ with radius $r$.
Choose an arbitrary point $x_1\in K$, then $K$ can not be covered by $B(x_1,r)$. So $$\exists x_2\in K-B(x_1,r)$$ and $K$ can not be covered by $$B(x_1,r)\cup B(x_2,r)$$
Suppose we have choose $x_1,\dots x_n$, hence $K$ can not be covered by $$B(x_1,r)\cup \dots \cup B(x_n,r)$$, choosing $$x_{n+1}\in K- \Bigl( B(x_1,r)\cup \dots \cup B(x_n,r) \Bigr)$$
By inaction, we have constructed a sequence $\{x_n \}_{n=1}^\infty$ in $K$ s.t. $$x_i\neq x_j  \;\;\forall i\neq j \text{ and } d(x_i,x_j)\geqslant r $$ , then $\dots \dots$ (skip the whole proof)
If I want to write it more formally, let $$S=\{n \in N \;| \; \{x_k \}_{k=1}^n\in K \text{ such that } d(x_i,x_j)\geqslant r\;\; \forall i\neq j \text{ and } x_k\in K- \Bigl( B(x_1,r)\cup \dots \cup B(x_{k-1},r) \Bigr) \} \;\;\;\color{red}{(\star)}$$
First, choosing an arbitrary point $x_1\in K$. Suppose we have chosen $\{ x_1,\dots,x_{n-1}\}$ satisfying that $$d(x_i,x_j)\geqslant r \;\; \forall i\neq j \text{ and } x_k\in K- \Bigl( B(x_1,r)\cup \dots \cup B(x_{k-1},r) \Bigr)\text{, }\forall k=1,\dots,n-1$$
Now, choose $$x_n \in K- \Bigl( B(x_1,r)\cup \dots \cup B(x_{n-1},r) \Bigr)$$, then $$d(x_n,x_k)\geqslant r \;\;\forall k=1,\dots,n-1$$
Hence, $S=\Bbb N$, which means $\{x_n \}_{n=1}^\infty$ is constructed and $d(x_i,x_j)\geqslant r \;\; \forall i\neq j$
$\color{blue}{\textrm{My question :}}$ I thinks the set $S$ in $\color{red}{(\star)}$ for induction looks weird, since I have never write this for construction. Could someone help me to write it more formally, thanks a lot!!
 A: More formally, the kind of construction you're outlining actually boils down to a combination of an application of the Axiom of Choice and a construction by recursion.
In particular, one of the formulations of the Axiom of Choice is: for every set $K$, there is a function $c : P(K) \setminus \{ \emptyset \} \to K$ such that for every $S \subseteq K$ with $S \ne \emptyset$, we have $c(S) \in S$.  Now, suppose we choose such a function $c$ (where this "choose" is actually not a reference to the Axiom of Choice, it stands for an application of the formal proof rule of existence elimination, $\exists E$).  Then under the given hypotheses, we can recursively construct a sequence where $x_n = c\left( K \setminus \bigcup_{i < n} B(x_i, r) \right)$.

To illustrate the gap in the argument you're trying to make, it does not follow just from the fact that a finite sequence of any arbitrary length exists satisfying some property that an infinite sequence exists satisfying that property.  For example, in $\mathbb{N}$, for any $k$ there exists a finite sequence in $\mathbb{N}$ of length $k$ which is strictly decreasing -- namely $(k, k-1, k-2, \ldots, 2, 1)$.  However, it does not follow from this that there exists an infinite sequence in $\mathbb{N}$ which is strictly decreasing -- which does not exist since $\mathbb{N}$ is well-ordered.
A: You have assumed that $K$ is not totally bounded, and that a suitable $r>0$ is fixed.
Define a set $S =$
$$\{n \geq 1 : \text{it is possible to select $n$ distinct elements of $K$}$$
$$ \text{ such that $d(x_i,\,x_j) \geq r$ for any choices with $i \neq j$.}    \}$$
I say that you have proved already that $S \,=\, \{1,2,3,4,\dots\}$.
Did you prove that $1$ belongs to $S$? Yes.
Did you prove that $n = k +1$ belongs to $S$ for any $k \geq 1$, under that assumption that $\{1,2,\dots,k\} \subset S$? Yes.
A: Let $x_1$ be an arbitrary point of $X$. Define $f_n:[1,n] \cap \mathbb{N} \rightarrow X$ by
$$f(1) = x_1 \\
\text{for }n > 1, f_n(i)=
                  \begin{cases}
                   f_{n-1}(i), & 1 \leq i \leq n-1 \\
                   \exists x_n \in K-\bigcup_1^{n-1}B_r(x_i),f_n(n)=x_n
                  \end{cases} \\
$$
Define $f:\mathbb{N} \rightarrow X$ by $f(n)=f_n(n)$.
