Summably nested Hausdorff intersection theorem (source code)

= Summably nested Hausdorff intersection theorem
{c}
{title2=$d_H(F_n,G)\leq\sum_{k=n}^\infty a_k$}

Let $X$ be a <complete metric space> and let $F_n$ be nonempty <closed> bounded subsets with $F_{n+1}\subseteq F_n$ and <Hausdorff distance> $d_H(F_n,F_{n+1})\leq a_n$, where $a_n\geq0$ and $\sum_n a_n<\infty$. Then $G=\bigcap_n F_n$ is nonempty and <closed>, and $d_H(F_n,G)\leq\sum_{k=n}^{\infty}a_k\to0$.

To prove this, start with any $x_n\in F_n$ and choose $x_{k+1}\in F_{k+1}$ with $d(x_k,x_{k+1})<a_k+\eta2^{n-k-1}$. The <triangle inequality> makes the resulting sequence a <Cauchy sequence>. Its limit exists by <completeness> and belongs to every $F_j$ by nesting and closedness. Its distance from the starting point is at most $\sum_{k=n}^{\infty}a_k+\eta$. Let $\eta\downarrow0$ and take the <supremum> over starting points. The reverse directed distance is zero since $G\subseteq F_n$. Unlike the usual shrinking-diameter form of <Cantor's intersection theorem>, the sets need not have diameters tending to zero.