LemmaStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A compact metric space has a countable dense subset, by countable choice

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( $\mathrm{AC}_\omega$ )). Let $(X,d)$ be a compact metric space (Open cover, subcover, compact metric space, and compact subset of a metric space, Metric space: $d(x,y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric). Then there is an at most countable set $D \subseteq X$ (Finite, countably infinite, countable, uncountable) that is dense in $X$ , that is $\overline{D} = X$ (Interior, closure, boundary, limit point, isolated point and dense subset of a metric space).

Where the axiom is spent. Once at step 2.1, to fix a finite $1/(n+1)$ -net for every $n \in \mathbb{N}$ at the same time; the family of sets chosen from is written down before any selection and does not depend on the earlier ones. The appeal to Countable unions of at most countable sets, assuming $\mathrm{AC}_\omega$ at step 4.1 carries the same hypothesis $\mathrm{AC}_\omega$ and no more, so nothing further is spent there. As always on this page the claim is an upper bound on the cost of this proof, not an assertion that $\mathrm{AC}_\omega$ is necessary.

Facts & Assumptions

Given: A compact metric space $(X,d)$ and the Axiom of Countable Choice.

[L1]

A compact metric space is totally bounded: for every real $\varepsilon > 0$ there is a finite $F \subseteq X$ with $X = \bigcup_{y \in F} B(y,\varepsilon)$ (A compact metric space is complete and totally bounded, and neither implication uses any choice principle, Finite $\varepsilon$ -net and totally bounded metric space, Open ball, closed ball and sphere in a metric space).

[L2]

Countable choice: for a family $(E_n)_{n \in \mathbb{N}}$ of nonempty sets there is a function $n \mapsto e_n$ with $e_n \in E_n$ (The Axiom of Countable Choice ( $\mathrm{AC}_\omega$ )).

[L3]

Finite sets are at most countable, and, assuming countable choice, a union $\bigcup_{n \in \mathbb{N}} A_n$ of at most countable sets is at most countable (Finite, countably infinite, countable, uncountable, Countable unions of at most countable sets, assuming $\mathrm{AC}_\omega$ , A nonempty set is at most countable iff it is a surjective image of $\mathbb{N}$ ).

[L4]

$x \in \overline{D}$ exactly when $B(x,r) \cap D \ne \emptyset$ for every real $r > 0$ , and $D$ is dense when $\overline{D} = X$ (Interior, closure, boundary, limit point, isolated point and dense subset of a metric space, The closure of a nonempty $A$ is $\{x : d(x,A) = 0\}$ , equals $A$ together with its limit points, and is the smallest closed superset).

[L5]

For every real $r > 0$ there is a natural $N \ge 1$ with $1/N < r$ , and $0 < 1/(n+1) \le 1/N$ whenever $n + 1 \ge N$ (For every $\varepsilon > 0$ in a complete ordered field there is a natural $n \ge 1$ with $1/n < \varepsilon$ , Every complete ordered field is Archimedean, Inverses of positives are positive, and reciprocation reverses order).

Proof

technique · direct

1.1

For each $n \in \mathbb{N}$ let $E_n$ be the set of finite $1/(n+1)$ -nets for $(X,d)$ ; each $E_n$ is nonempty because $(X,d)$ is compact and hence totally bounded.

2.1

Countable choice applied to $(E_n)_{n \in \mathbb{N}}$ fixes a function $n \mapsto F_n$ with $F_n \in E_n$ for every $n$ , that is a finite $1/(n+1)$ -net $F_n \subseteq X$ for each $n$ ; this is the only appeal to a choice principle here.

L2step 1.1

3.1

Put $D := \bigcup_{n \in \mathbb{N}} F_n \subseteq X$ .

step 2.1

4.1

Each $F_n$ is finite and therefore at most countable, so $D$ is at most countable by the countable union theorem, whose hypothesis is the same $\mathrm{AC}_\omega$ already assumed.

L3step 3.1

4.2

$D$ is dense: given $x \in X$ and a real $r > 0$ , take a natural $N \ge 1$ with $1/N < r$ and put $n := N$ , so that $1/(n+1) < 1/N < r$ ; since $F_n$ is a $1/(n+1)$ -net there is $y \in F_n$ with $d(x,y) < 1/(n+1) < r$ , and that $y$ lies in $B(x,r) \cap D$ .

L1L4L5step 2.1step 3.1

5.1

So every ball around every point of $X$ meets $D$ , that is $\overline{D} = X$ , and $D$ is an at most countable dense subset of $X$ .

L4step 4.1step 4.2∎

Remarks

The word for this property is not used here. A space with an at most countable dense subset has a standard name, and that name is not introduced at this point in the reading order; the statement therefore says what it means outright. Nothing below or elsewhere on this page depends on the terminology.

Why a choice principle appears at all. Total boundedness asserts that a finite $1/(n+1)$ -net exists for each $n$ ; it names none, and there is no rule in this library that singles one out uniformly in $n$ . Fixing one for every $n$ at once is precisely $\mathrm{AC}_\omega$ , and it is spent in exactly the same way, and for exactly the same reason, as in A complete, totally bounded metric space is compact, proved from countable choice used exactly once.

The empty space is covered by the statement. If $X = \emptyset$ then every $F_n$ is empty, $D$ is empty, and $\overline{D} = \emptyset = X$ ; the empty set is finite and hence at most countable.

Depends on

Used by

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 Remark

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 107 results over 17 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Compact space (Wikipedia) (standard reference, not scraped)
Axiom of countable choice (Wikipedia) (standard reference, not scraped)