Distance-increasing self-map theorem for sequentially compact metric spaces (source code)

= Distance-increasing self-map theorem for sequentially compact metric spaces

Every <continuous> map $T:X\to X$ on a <sequentially compact space> with a <metric> satisfying $d(Tx,Ty)\geq d(x,y)$ is a surjective <isometry>.

A <convergent subsequence> of the paired orbit $(T^kx,T^ky)$ has two late terms arbitrarily close. Removing their common number of iterates by the distance inequality shows that $(x,y)$ returns arbitrarily close to itself after a common positive time $n$. Thus $d(Tx,Ty)\leq d(T^nx,T^ny)\leq d(x,y)+2\epsilon$, and letting $\epsilon\downarrow0$ proves the <isometry> claim. For each $x$, choose return times $n_k\geq1$ with $T^{n_k}x\to x$. A <convergent subsequence> of $T^{n_k-1}x$ has limit $z$, and <continuity> gives $Tz=x$. This proves surjectivity.