Completeness forced by uniformly bounded lifting (source code)

= Completeness forced by uniformly bounded lifting
{title2=$Tx=y,\quad\|x\|\le C\|y\|$}

If a <bounded linear operator> from a <Banach space> onto a <normed vector space> admits the displayed lift for every $y$, then its target is complete. Given a <Cauchy sequence>, choose a subsequence with summable successive differences. Lift those differences to a summable sequence in the source, and use its convergent sum to produce a limit of the target subsequence. The original Cauchy sequence has the same limit.