Solution (source code)

= Solution

A <metric space> is <sequential compactness>[sequentially compact] if every sequence has a <convergent sequence>[convergent] <subsequence> whose limit belongs to the space. A <limit point> $\ell$ of $S$ is a point for which every open ball about $\ell$ contains a point of $S$ other than $\ell$.

Let $(x_n)$ lie in a <compact space>[compact] <metric space>. If one value occurs infinitely often, take a constant <subsequence>. Otherwise its set of values $S$ is infinite. If $S$ had no <limit point>, every point of the space would have a neighborhood containing at most one member of $S$. A finite subcover of these neighborhoods would force $S$ finite, a contradiction. Thus $S$ has a <limit point>; the stated <subsequence> result supplies a <convergent sequence>[convergent] <subsequence>. This proves <sequential compactness>.

Assume now that $X$ is nonempty, as is necessary for the requested minimum and <fixed point>. The function $r(x)=d(f(x),x)$ is <continuous function>[continuous], as a <function composition>[composition] of $x\mapsto(f(x),x)$ with the <metric>. The <extreme value theorem> on a <compact space> implies that $r$ attains its infimum, say at $p$. If $f(p)\neq p$, strict decrease of distances gives
$$
r(f(p))=d(f^2(p),f(p))<d(f(p),p)=r(p),
$$
contradicting minimality. Thus $f(p)=p$. If $p,q$ were distinct <fixed point>[fixed points], then $d(p,q)=d(f(p),f(q))<d(p,q)$, another contradiction. Hence \b[there is exactly one <fixed point>]. This is the <fixed point theorem for a strictly distance-decreasing map on a compact metric space>.

<Compactness> is essential. On $\mathbb R$, take
$$
\boxed{f(x)=\log(1+e^x).}
$$
Here $f(x)-x=\log(1+e^{-x})>0$, so there is no <fixed point>. Nevertheless $0<f'(x)=e^x/(1+e^x)<1$ everywhere, and the <mean value theorem> gives $|f(x)-f(y)|<|x-y|$ for distinct $x,y$. There is no uniform <Lipschitz continuity>[Lipschitz] constant less than $1$, since $f'(x)\to1$ as $x\to\infty$.