Cauchy-sequence construction of a metric completion (source code)

= Cauchy-sequence construction of a metric completion
{title2=$\widehat d([(x_n)],[(y_n)])=\lim_n d(x_n,y_n)$}

For two <Cauchy sequences>, $|d(x_n,y_n)-d(x_m,y_m)|\leq d(x_n,x_m)+d(y_n,y_m)$, so the displayed limit exists. It defines a <pseudometric> on the Cauchy sequences, and its <metric quotient> identifies sequences whose mutual distance tends to zero. Constant sequences embed the original <metric space> isometrically. Their image is dense, because the class of $(x_n)$ is approached by the constant classes of $x_n$. The quotient is complete: from a Cauchy sequence of its points select a subsequence whose successive distances are below $2^{-j}$ and choose original-space points within $2^{-j}$ of these subsequence points. Those original-space points form a Cauchy sequence and its class is the limit of the subsequence, hence of the whole sequence. The original embedding is onto exactly when the original space is complete.