Completeness of a countable product metric (source code)

= Completeness of a countable product metric

If every factor is a <complete metric space>, the <countable product metric> is complete. For a product-Cauchy sequence, the inequality $2^{-i}\phi(d_i(x_i^{(m)},x_i^{(n)}))\leq D(x^{(m)},x^{(n)})$, with $\phi(t)=t/(1+t)$, makes each coordinate sequence <Cauchy>. Its coordinate limits define a product point. Coordinatewise convergence and the uniformly small summable tail imply convergence to that point in $D$. It matters that the original distances are bounded before they are summed: summing arbitrary unbounded metrics directly need not be finite.