TheoremStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)verified 2026-08-04 (gpt-5.6-sol-codex-subscription)

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 is complete and totally bounded, and neither implication uses any choice principle

Statement

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 $(X,d)$ is totally bounded (Finite $\varepsilon$ -net and totally bounded metric space) and complete (Complete metric space: every Cauchy sequence converges in the space).

Both implications are theorems of ZF. Completeness is obtained here from the finite intersection characterisation (A metric space is compact if and only if every family of closed subsets with the finite intersection property has nonempty intersection) applied to the closures of the tails of a Cauchy sequence, and not from the extraction of a convergent subsequence, which would route the argument through sequential compactness. What matters for the ledger is that the route taken below selects nothing at all; the first remark below says why the other route was not taken.

Facts & Assumptions

Given: A compact metric space $(X,d)$ .

[L1]

Open balls are open (Arbitrary unions and finite intersections of open sets are open, open balls are open and closed balls are closed, Open ball, closed ball and sphere in a metric space, The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement).

[L2]

$(X,d)$ is totally bounded exactly when for every real $\varepsilon > 0$ there is a finite $F \subseteq X$ with $X = \bigcup_{y \in F} B(y,\varepsilon)$ (Finite $\varepsilon$ -net and totally bounded metric space).

[L3]

$X$ is a compact subset of itself, and for every family $(U_i)_{i \in I}$ of open subsets of $X$ with $X = \bigcup_{i \in I} U_i$ there are $n \in \mathbb{N}$ and $i_0, \dots, i_n \in I$ with $X = U_{i_0} \cup \dots \cup U_{i_n}$ , unless $X = \emptyset$ (A subset of a metric space is open in the subspace metric exactly when it is the trace of an open set of the ambient space, and it is compact as a metric space in its own right exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it, Open cover, subcover, compact metric space, and compact subset of a metric space).

[L4]

$(X,d)$ is complete when every Cauchy sequence converges to a point of $X$ ; $(x_k)$ is Cauchy when for every rational $\varepsilon > 0$ there is $K$ with $d(x_m,x_l) < \varepsilon$ for all $m,l \ge K$ ; and $x_k \to p$ when for every rational $\varepsilon > 0$ there is $K$ with $d(x_k,p) < \varepsilon$ for all $k \ge K$ (Complete metric space: every Cauchy sequence converges in the space, Cauchy sequence in a metric space, Convergence of a sequence in a metric space: $x_k \to x$ iff $d(x_k, x) \to 0$ in $\mathbb{R}$ ).

[L5]

The closure $\overline{S}$ of $S \subseteq X$ is closed, contains $S$ , and is contained in every closed superset of $S$ ; and $x \in \overline{S}$ exactly when $B(x,r) \cap S \ne \emptyset$ for every real $r > 0$ (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, Interior, closure, boundary, limit point, isolated point and dense subset of a metric space).

[L6]

$(X,d)$ is compact exactly when every family of closed subsets of $X$ with the finite intersection property has nonempty intersection, the empty finite list having intersection $X$ (A metric space is compact if and only if every family of closed subsets with the finite intersection property has nonempty intersection, Finite intersection property).

[L7]

A metric satisfies the triangle inequality and is symmetric (Metric space: $d(x,y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric).

[L8]

A finite list $n_0, \dots, n_p$ of natural numbers has a greatest member. Indeed the reals $\iota(n_0+1), \dots, \iota(n_p+1)$ , with $\iota$ the canonical natural of $\mathbb{R}$ (The canonical natural $\iota(n) = n \cdot 1_F$ of a field), form a nonempty finite set of reals and so have a maximum, which is one of them, say $\iota(n_j+1)$ (Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set); the map $m \mapsto \iota(m)$ is strictly increasing on the naturals $\ge 1$ (Canonical naturals are positive and strictly increasing), so $n_j < n_i$ would force $\iota(n_j+1) < \iota(n_i+1)$ , which the maximality forbids, and the order of $\mathbb{N}$ is linear ( $\le$ is a linear order on $\mathbb{N}$ ), whence $n_i \le n_j$ for every $i \le p$ .

Proof

technique · direct

1.1

Let $\varepsilon > 0$ be real; the family $(B(x,\varepsilon))_{x \in X}$ consists of open subsets of $X$ and has union $X$ , since $x \in B(x,\varepsilon)$ for every $x$ .

L1L2

2.1

If $X = \emptyset$ the empty set is a finite $\varepsilon$ -net; otherwise the indexed characterisation gives $n \in \mathbb{N}$ and $x_0, \dots, x_n \in X$ with $X = B(x_0,\varepsilon) \cup \dots \cup B(x_n,\varepsilon)$ , so $\{x_0, \dots, x_n\}$ is a finite $\varepsilon$ -net; as $\varepsilon$ was arbitrary, $(X,d)$ is totally bounded.

L2L3step 1.1

3.1

Total boundedness being settled, take up completeness: let $(x_k)$ be a Cauchy sequence in $X$ and put $T_n := \overline{\{\, x_k : k \ge n \,\}}$ for $n \in \mathbb{N}$ , a definition by a rule and not by a selection.

L4L5step 2.1

4.1

Each $T_n$ is closed and nonempty, containing $x_n$ ; and $T_m \subseteq T_n$ whenever $m \ge n$ , since then $\{x_k : k \ge m\} \subseteq \{x_k : k \ge n\} \subseteq T_n$ and $T_m$ is the smallest closed superset of the first of these sets.

L5step 3.1

5.1

The family $\mathcal{A} := \{\, T_n : n \in \mathbb{N} \,\}$ of closed sets has the finite intersection property: the empty list has intersection $X$ , which contains $x_0$ ; and for a list $T_{n_0}, \dots, T_{n_p}$ take a greatest member $n_j$ of the list of indices, so that $T_{n_j} \subseteq T_{n_i}$ for every $i \le p$ and $x_{n_j}$ lies in every one of them.

L6L8step 4.1

6.1

By the finite intersection characterisation of compactness there is a point $p \in \bigcap \mathcal{A}$ , that is $p \in T_n$ for every $n \in \mathbb{N}$ .

L6step 5.1

7.1

Let $\varepsilon > 0$ be rational and take $K \in \mathbb{N}$ with $d(x_m,x_l) < \varepsilon/2$ for all $m,l \ge K$ ; since $p \in T_K$ , the ball $B(p,\varepsilon/2)$ meets $\{x_k : k \ge K\}$ , so there is $j \ge K$ with $d(p,x_j) < \varepsilon/2$ , and then $d(x_k,p) \le d(x_k,x_j) + d(x_j,p) < \varepsilon/2 + \varepsilon/2 = \varepsilon$ for every $k \ge K$ .

L4L5L7step 6.1

8.1

Hence $x_k \to p$ with $p \in X$ ; every Cauchy sequence in $X$ converges, so $(X,d)$ is complete, and with step 2.1 the theorem is proved.

L4step 2.1step 7.1∎

Remarks

Why the textbook route is avoided. The usual proof of completeness takes a Cauchy sequence, extracts a convergent subsequence and appeals to A Cauchy sequence in a metric space with a convergent subsequence converges to that subsequence’s limit. That is correct, but it goes through sequential compactness, and the reader tracking the ledger then has to check the cost of that implication before believing this one. The tail-closure argument above is shorter and manifestly selects nothing: the sets $T_n$ are given by a formula, the point $p$ is produced by one existential instantiation, and the index $j$ in step 7.1 by another.

Neither converse holds. A complete metric space need not be totally bounded and need not be compact ( $\mathbb{R}$ is complete and unbounded), and a totally bounded space need not be compact (FALSE: a totally bounded metric space is compact, The open interval $(0,1)$ is totally bounded and not compact, the cover by the intervals $(1/(k+2), 1)$ having no finite subcover ↗). What is true is that, assuming the Axiom of Countable Choice, the two together are equivalent to compactness; the missing direction is A complete, totally bounded metric space is compact, proved from countable choice used exactly once, and that is exactly where the Axiom of Countable Choice is spent.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 95 results over 18 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

Totally bounded space (Wikipedia) (standard reference, not scraped)
Compact space (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 3 (standard reference, not scraped)