Closed discrete subsets of compact spaces are finite (source code)

= Closed discrete subsets of compact spaces are finite

Let $D$ be a <closed discrete subset> of a <compact space> $X$. Closedness makes $D$ compact. Discreteness makes its singletons open in its <subspace topology>, so the singleton cover has a finite subcover. Thus $D$ is finite. Closedness is essential: the discrete set $\{1/n:n\geq1\}$ inside the compact interval $[0,1]$ is infinite and has the missing accumulation point zero.