## Formalized Name Finite-Net Branch Data Gives a Cauchy Subsequence ## Formalized Statement Let $X$ be a metric space with specified finite $2^{-k}$-nets $E_k$ for every $k$. Let $(x_n)$ be a sequence in $X$. Suppose branch-selection data are given: for each $k$ there is a point $e_k\in E_k$ and an infinite increasing sequence of indices $I_k(0)<I_k(1)<\cdots$ such that every $x_{I_k(j)}$ lies within $2^{-k}$ of $e_k$, and the index sequence for $k+1$ is a subsequence of the index sequence for $k$. Then there is a strictly increasing sequence $(n_m)$ such that for all $k$ and all $p,q\ge k+1$ one has $d(x_{n_p},x_{n_q})\le 2^{-k}$. ## Proof [proofplan] Use the nested index sets supplied by the branch-selection data. Choose the diagonal subsequence by taking one sufficiently late index from each level. If two chosen terms are taken after level $k$, then both lie in the same $2^{-k}$-ball around the net point $e_k$, so their distance is at most $2^{1-k}$. [/proofplan] [step:Define the diagonal subsequence] Choose $n_k:=I_k(k)$. Because the index sequence at level $k+1$ is a subsequence of the index sequence at level $k$, and because the chosen position increases with $k$, the indices can be thinned recursively so that \begin{align*} n_0<n_1<n_2<\cdots. \end{align*} Replacing $I_k(k)$ by a later term if necessary preserves membership in the same branch. Thus $(x_{n_k})$ is a subsequence of $(x_n)$. [/step] [step:Prove the Cauchy estimate] Fix $k$. If $p,q\ge k$, then the nestedness of the branch data implies that both $n_p$ and $n_q$ occur in the level-$k$ index sequence. Hence both $x_{n_p}$ and $x_{n_q}$ lie within $2^{-k}$ of $e_k$. By the triangle inequality, \begin{align*} d(x_{n_p},x_{n_q})\le d(x_{n_p},e_k)+d(e_k,x_{n_q})\le 2^{-k}+2^{-k}=2^{1-k}. \end{align*} Therefore the subsequence is Cauchy. Equivalently, using level $k+1$ gives the displayed modulus \begin{align*} p,q\ge k+1\quad\Longrightarrow\quad d(x_{n_p},x_{n_q})\le 2^{-k}. \end{align*} [/step] [step:Conclude sequential compactness from the supplied data] The sequence $(n_k)$ is strictly increasing, so $(x_{n_k})$ is a genuine subsequence. The previous step gives an explicit Cauchy modulus. Thus the finite-net branch-selection data produce a Cauchy subsequence. [/step] [step:Summarize the compactness mechanism] The branch data choose one ball at each precision that contains infinitely many sequence terms, nested through the precisions. The diagonal subsequence eventually stays in every chosen ball, and the triangle inequality gives the Cauchy modulus. [guided] The branch data choose one ball at each precision that contains infinitely many sequence terms, nested through the precisions. The diagonal subsequence eventually stays in every chosen ball, and the triangle inequality gives the Cauchy modulus. [/guided] [/step]