For a metric space, compact, countably compact, limit point compact, sequentially compact, and complete together with totally bounded are all equivalent, given countable choice and dependent choice

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ($\mathrm{AC}_\omega$)) and the Axiom of Dependent Choice (The axiom of dependent choice: a relation in which every element is related to something admits an $\mathbb{N}$-indexed chain). Let $(X,d)$ be a metric space (Metric space: $d(x,y) = 0$ iff $x = y$, symmetry, and the triangle inequality; pseudometric and ultrametric). Then the following five conditions are equivalent.

• (a) $(X,d)$ is compact (Open cover, subcover, compact metric space, and compact subset of a metric space).
• (b) $(X,d)$ is countably compact (Countably compact, sequentially compact and limit point compact metric spaces).
• (c) $(X,d)$ is limit point compact.
• (d) $(X,d)$ is sequentially compact.
• (e) $(X,d)$ is complete (Complete metric space: every Cauchy sequence converges in the space) and totally bounded (Finite $\varepsilon$-net and totally bounded metric space).

The two hypotheses are not needed everywhere, and the statement should not be read as if they were. Of the implications assembled below, all but two are theorems of ZF. Dependent choice is used only for "sequentially compact implies totally bounded" (A sequentially compact metric space is totally bounded, proved from the axiom of dependent choice), and countable choice only for "complete and totally bounded implies compact" (A complete, totally bounded metric space is compact, proved from countable choice used exactly once). Each is an upper bound on the cost of the proof given in this library and not a claim of necessity; the implication-by-implication account is What each implication between the compactness properties of a metric space costs: which are theorems of ZF, which use countable choice, and which use dependent choice.

Read the equivalence with the ledger beside it. The theorem as stated carries two choice hypotheses, and a reader working in ZF alone still keeps a great deal: by In any metric space compactness implies countable compactness and limit point compactness, and each of countable compactness and limit point compactness implies sequential compactness; every implication here is proved without a choice principle and A compact metric space is complete and totally bounded, and neither implication uses any choice principle, compactness implies all four of the other conditions with no choice at all, and by A sequentially compact metric space is complete, with no choice principle used sequential compactness implies completeness. What fails without choice is the return journey, from the weaker conditions back to compactness.

The direct route from (a) to (e) is worth keeping. Step 6.1 records that A compact metric space is complete and totally bounded, and neither implication uses any choice principle proves (a) $\Rightarrow$ (e) in ZF, whereas reading it off the cycle would route it through (b) and (d) and, at the last leg, through dependent choice. A cycle of implications transmits the weakest hypothesis around it; the individual arrows do not, and it is the individual arrows that the ledger records.

Nothing here is claimed for topological spaces. All five conditions make sense more generally, and the equivalences above are proved for metric spaces only, every argument using the metric.