Bounded-continuous-function characterization of compact metric spaces (source code)

= Bounded-continuous-function characterization of compact metric spaces

A metric space $X$ is compact exactly when every continuous function $X\to\mathbb R$ is bounded. For the converse, a noncompact metric space contains a closed discrete sequence; the unbounded function assigning its $n$th point the value $n$ extends to $X$ by the Tietze extension theorem.