Lemma: Let $(X,d)$ be a metric space. For each $n \in \{1,2,3,\ldots\}$ there is (by Zorn's lemma) a maximal (by inclusion) set $D_n$ such that for all $x,y \in D_n$ with $x \neq y$, we have $d(x,y) \ge \frac{1}{n}$. If all $D_n$ are at most countable, then $X$ is separable.
Proof: We'll show that $D = \cup_n D_n$ is dense (and is countable when all $D_n$ are), and so pick any $x \in X$ and any $r>0$ and we'll show that $B(x,r) \cap D \neq \emptyset$. Suppose not, then find $m$ with $\frac{1}{m} < r$. Then from $B(x,r) \cap D = \emptyset$ we know that
$d(x, y) \ge \frac{1}{m}$ for all $y \in D_m$ (or else $y \in D \cap B(x,r)$), and then $D_m \cup \{x\}$ would contradict the maximality of $D_m$. So the intersection with $D_m$ and hence $D$ is non-empty, and so $D$ is dense.
(The above is the heart of the proof that a ccc metric space is separable, as $X$ ccc implies that all $D_m$ are countable, as the $B(x,\frac{1}{m})$, $x \in D_m$ are a pairwise disjoint open family of non-empty sets.)
Now suppose that $(X,d)$ is countably compact. Suppose for a contradiction that $X$ is not separable. Then for some $m \ge 1$ we have that $D_m$ (as in the lemma) is uncountable.
Fix such an $m$.
Now $D_m$ is discrete (clear as $B(x,\frac{1}{m}) \cap D_m = \{x\}$ for each $x \in D_m$) and closed: suppose that $y \in X\setminus D_m$ is in $\overline{D_m}$, then $B(y, \frac{1}{2m})$ contains infinitely many points of $D_m$ and for any $2$ of them, say $x_1, x_2 \in D_m$, we'd have $d(x_1, x_2) \le d(x_1, y) + d(y,x_2) < \frac{1}{m}$ contradiction (as points in $D_m$ are at least $\frac{1}{m}$ apart). So $D_m$ is closed and discrete (as an aside: being uncountable this would already contradict Lindelöfness of $X$; this shows that a Lindelöf metric space is separable, e.g.), but we want to contradict countable compactness, which is easy too:
Choose $A \subseteq D_m$ countably infinite (so that $A$ is closed in $X$, as all subsets of $D_m$ are), and define a countable open cover $\mathcal{U} = \{B(p, \frac{1}{m}): p \in A\} \cup \{X\setminus A\}$ of $X$ that has no finite subcover: we need every $B(p,\frac{1}{m})$ to cover $p$ for all $p \in A$.
This contradiction then shows $X$ is separable (and thus has a countable base ,is Lindelöf etc. finishing the compactness).
The crucial fact is that all of the following are equivalent for a metric space:
- $X$ has a countable base.
- $X$ is separable.
- All discrete subspaces of $X$ are at most countable.
- All closed and discrete subspaces of $X$ are at most countable.
- $X$ is ccc.
- $X$ is Lindelöf.
In the above I essentially did "not (2) implies not (4)" implicitly. The fun is that countable compactness implies (4) easily (such closed discrete subspaces are even finite) and thus we get Lindelöfness "for free". Also implicit in the above proof is that every countably compact space is limit point compact.
Best Answer
There is a reasonably direct proof of this fact. The trick is to take a subnet that is a sequence.
Consider a nonempty net $(x_d)_{d \in D}$. If there is a maximal $d$, then the singleton net $x_d$ converges to $d$. Otherwise, for every $d$, there is some greater $d’$. Using dependent choice, choose $d_1 < d_2 < \ldots$. Then $(x_{d_n})_{n \in \mathbb{N}}$ has a convergent subsequence which is also a convergent subnet of the original net.
If you wish for a constructive proof that every sequentially compact space is compact, I’m afraid you’re going to be disappointed (though I haven’t ruled out the possibility that there’s a constructive proof that sequentially compact implies net compact).
We can show constructively that every compact space $X$ either has a point or is empty. For consider the open cover $\{X \mid \exists y (y \in X)\}$. This open cover has a finitely enumerator sub cover $U_1, \ldots, U_n$. If $n = 0$, then $X$ Is empty, while if $n > 0$, then $X$ has a point.
Now for any proposition $p$, consider the associated topological space $\{0 \mid p\}$. This space is sequentially compact (in fact, net compact) and has a point if and only if $p$.
If we could show this space is also compact constructively, then we would have proved the space is either empty or no empty, and thus $p \lor \neg p$. But this cannot be done constructively. So no constructive proof can exist.