Contraction property of closed subsets characterizes completeness (source code)

= Contraction property of closed subsets characterizes completeness

A <metric space> is <complete> if and only if every <contraction mapping> of every nonempty <closed subset> into itself has a <fixed point>. For the converse, a nonconvergent <Cauchy sequence> contains a rapidly approaching subsequence whose point set is closed and whose shift is a contraction without a fixed point. Requiring the property only on the whole space is a different, weaker condition.