Lebesgue number lemma in nLab

Proposition

Assuming excluded middle and countable choice then:

If (X,d)(X,d) is a metric space which is sequentially compact, then for every open cover {U i→X} i∈I\{U_i \to X\}_{i \in I} there exists a positive real number δ∈ℝ\delta \in \mathbb{R}, δ>0\delta \gt 0, called a Lebesgue number for XX, such that for every point x∈Xx \in X there exists an i∈Ii \in I such that the open ball around xx of radius δ\delta is contained in U iU_i:

((X,d)sequentially compact)⇒∃δ>0(∀x∈X(∃i∈I(B x ∘(δ)⊂U i))) \left( (X,d) \, \text{sequentially compact} \right) \;\Rightarrow\; \underset{\delta \gt 0}{\exists} \left( \underset{x \in X}{\forall} \left( \underset{i \in I}{\exists} \left( B^\circ_x(\delta) \subset U_i \right) \right) \right)

Proof

Assume that the statement were not true. This would mean that for every n∈ℕn \in \mathbb{N} there exists a point x n∈Xx_n \in X such that for all i∈Ii \in I the open ball B x n ∘(1/(n+1))B^\circ_{x_n}(1/(n+1)) is not contained in U iU_i. These points (x n) n∈ℕ(x_n)_{n \in \mathbb{N}} would constitute a sequence and so by assumption on XX there would exist a sub-sequence (x n k) k∈ℕ(x_{n_k})_{k \in \mathbb{N}} which converges to some x ∞∈Xx_\infty \in X. Hence then there would be some i ∞∈Ii_\infty \in I with x ∞∈U i ∞x_\infty \in U_{i_\infty}, and this, since U i ∞U_{i_\infty} is open, also a positive real number ϵ>0\epsilon \gt 0 with B x ∞ ∘(ϵ)⊂U i ∞B^\circ_{x_\infty}(\epsilon) \subset U_{i_\infty}. By convergence of the sub-sequence (x n k) k(x_{n_k})_k we could now choose a k∈ℕk \in \mathbb{N} such that

1n k+1<ϵ2AAAandAAAd(x n k,x ∞)<ϵ2. \frac{1}{n_k + 1} \lt \frac{\epsilon}{2} \phantom{AAA} \text{and} \phantom{AAA} d(x_{n_k}, x_{\infinity}) \lt \frac{\epsilon}{2} \,.

This would imply that

B x n k ∘(1/n k)⊂B x ∞ ∘(ϵ)⊂U ∞. B^\circ_{x_{n_k}}(1/n_k) \subset B^\circ_{x_\infty}(\epsilon) \subset U_\infty \,.

This contradicts the assumption that none of the U iU_i contains the open ball B x n k ∘(1/n k)B^\circ_{x_{n_k}}(1/n_k), and hence we have a proof by contradiction.