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.
You don't need the axiom of choice here.
Since for each $x$ there is some $\delta$ that is a candidate for $\delta_x$, and moreover, if we make that $\delta$ smaller then we do not lose any generality either, we can simply take $\delta_x$ to be $\frac1n$ where $n$ is the least one for which $\frac1n$ works.
You see this sort of behaviour on occasion, where we seemingly utilise choice at unnecessary points where a slightly more elaborate argument will avoid it. However, topology is something that breaks very very easily without assuming the axiom of choice. Which is why people tend to just assume it and move on.