Proof of Closest Point Theorem in Hilbert Space

Question

The theorem:

Let $C$ be a non-empty closed convex subset of a Hilbert space $X$, and let $x \in X$. Then there exists a unique $y_0 \in C$ such that $||x-y_0|| \le ||x - y||$ all $y \in C$. In other words there is a point in $C$ which is closest to $x$.

I'm reading a proof here (https://www0.maths.ox.ac.uk/system/files/coursematerial/2014/3075/48/15B4.2-webnotes-all.pdf, p.4) and have two questions about the initial steps in the prooof (I can follow the later steps.):

1. "Let $d = inf\{||x - y||: y \in C\}$" I think that the infimum should exist by the property (axiom) of completeness of the real numbers. $\{||x - y||: y \in C\}$ is a set of real numbers which is bounded below (all norms are $\ge 0$) and therefore has a greatest lower bound - is this correct ?
2. "Let $(y_n)$ be a sequence of points in C such that $||x - y_n|| \to d$". I think such a sequence should exist by the following reasoning: With $d = inf\{||x - y||: y \in C\}$ then for any $\epsilon > 0$ there must be a point $y$ in $C$ such that $||x - y|| \lt d + \epsilon$ (otherwise $d$ is not the infimum). If for this point $||x - y|| = d $ then $y_0 = y$ and we are finished: $(y_0)$ is a one element convergent sequence. Otherwise $||x - y|| = d + \epsilon`$ where $\epsilon` \le \epsilon$ and I can repeat the process to find a different point where $||x - y|| \lt d + \epsilon`/2$ and so generate a convergent sequence. I'm not sure this is valid, and it occurs to me that unless $C = \{y_0\}$ there are probably an infinite number of points at each step and the Axiom of choice is then required to extract a convergent sequence. Any help would be appreciated.

Answer 1

1) You are correct. Every set that is bounded below in $\mathbb{R}$ has a least lower bound.

2)The standard why to show that there exists such a sequence $(y_n)$ is as follows. Let $n\in\mathbb{N}$ then as d is the infimium, $d+\frac{1}{n}$ is not a lower bound so there exists $y_n$ such that $d<||x-y_n||<d+\frac{1}{n}$. This gives a sequence of points $(y_n)$. Then it should be obvious that $||x-y_n||\rightarrow d$.