I recently read a proof on Wikipedia of Heine's theorem here. I am using their notations.
The proof aims at showing that given two metric spaces $M$ and $N$ where $M$ is compact, if $f$ is a continuous mapping $M\rightarrow N$, then $f$ is uniformly continuous.
Part of the proof states that for every $\epsilon>0$ and every $x$, there exists a $\delta_x$ such that $d_M(x,y)<\delta_x \Rightarrow d_N(f(x),f(y))<\epsilon$, and then uses $\delta_x$ which is a mapping from $M$ to $\mathbb R^+$.
Am I right when wondering if the axiom of choice is implicitly assumed?
Going back to various proofs on compact sets, I have the feeling that some form of Axiom of Choice (either general or at least countable) must be assumed in quite a few proofs.
For instance, when showing that a sequence of values in a bounded interval in $\mathbb R$ has a converging subsequence, you need to choose recursively subsequences and sequence elements, so at least do a countable number of choices.
When I was taught that at university, I don't remember that was mentioned, so I am wondering if those technical details have been brushed under the carpet back then.