Does this proof that every open set in a metric space is a union of open balls use the axiom of choice?

Question

I am reading "A Course in Analysis vol.3" by Kazuo Matsuzaka.

There is the following proposition in this book.

Does the author use the axiom of choice in the proof?

Proposition 4:

A subset $A$ of a metric space $X$ is open in $X$ if and only if $A$ is a union of open balls in $X$.

Proof:

An open ball is open, so a union of open balls is open. Conversely, if $A$ is open and $a \in A$, then there exists a positive real number $r(a)$ such that $B(a ; r(a)) \subset A$. Obviously $$A = \bigcup_{a \in A} B(a ; r(a))$$ holds.

I think the author's proof uses the axiom of choice as follows:

Let $S_a := \{x \in \mathbb{R} | x > 0, B(a ; x) \subset A\}$.
Since $A$ is open, for any $a \in A$, $S_a \ne \emptyset$.
So, by the axiom of choice, there exists a mapping $r$ from $A$ to $\bigcup_{a \in A} S_a$ such that $r(a) \in S_a$.

Answer 1

Choose the diameter $r_0 := r(a) := 1$. If this ball $B(a, r_0)$ is not in $A$, consider the next terms $r_{n + 1} = \frac{1}{2} r_n$. This sequence converges to zero. Since A is open, after finitely many steps you get (constructively) a value such that the ball is in $A$.

But the Axiom of choice as an axiom concerning the sheer existence of a choice function for arbitrary infinite sets is non-constructive.

Thus the axiom of choice is not needed.

Answer 2

Yes. This proof does seem to use the axiom of choice, but we can fix that using the maxim "If you can't choose one, just take all of them".

$$A=\bigcup\{B(a,r)\mid a\in A, B(a,r)\subseteq A\}.$$

Another way to fix this is be more explicit about $r(a)$. We can assume it is a positive rational, since the rational numbers are dense and it has to be positive, so we can take the one with the smallest representation as $n/m$ where $(n,m)\in\Bbb{N\times N}$ ordered lexicographically.