Completeness of the Hausdorff hyperspace (source code)

= Completeness of the Hausdorff hyperspace
{c}

For any nonempty <complete metric space> $X$, the family of its nonempty <closed> bounded subsets is a <complete metric space> under the <Hausdorff distance>. Boundedness of the entire ambient space is unnecessary in this general form.

For a <Cauchy sequence> $(F_n)$ of these sets, define $A_n=\overline{\bigcup_{m\geq n}F_m}$ and $\delta_n=\sup_{p,q\geq n}d_H(F_p,F_q)$. A <Cauchy sequence> in any <metric space> is bounded, so its tail sets are contained in a common finite-radius neighbourhood of one bounded $F_N$; hence every $A_n$ is bounded. The <distance to a set> is one-<Lipschitz>, so estimates pass to the <closure>, giving $d_H(F_n,A_n)\leq\delta_n$ and $d_H(A_n,A_m)\leq\delta_n$ for $m\geq n$. Choose $n_j$ with $\delta_{n_j}\leq2^{-j}$. The <Summably nested Hausdorff intersection theorem> gives $A_{n_j}\to G\ne\varnothing$. The <triangle inequality> now gives $F_n\to G$, proving <completeness>.