Weak weak Koenig and covering spaces

[Timothy Y. Chow]

On Mon, 10 May 2021, I wrote:
> The reason I ask is that I was recently refreshing my memory about some 
> of those results, and it seems that some version of the Vitali covering 
> lemma is typically used when lifting a map to a covering space.  So 
> maybe the weak weak Koenig lemma is needed?

I looked more carefully and found that in Munkres's textbook "Topology," 
the key lemma seems to be something he calls the "Lebesgue number lemma":

Lemma.  Let A be an open covering of a compact metric space.  Then there 
exists delta > 0 such that every subset of X with diameter less than delta 
is contained in some element of A.

Is this Lemma provable in RCA_0?

Tim