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 totally bounded metric space is bounded, every subspace of a totally bounded space is totally bounded, and the closure of a totally bounded subset is totally bounded

Statement

Let $(X,d)$ be a metric space (Metric space: $d(x,y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric), with total boundedness as in Finite $\varepsilon$ -net and totally bounded metric space and boundedness as in Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space. Then:

If $(X,d)$ is totally bounded, it is bounded.
If $(X,d)$ is totally bounded and $A \subseteq X$ , then the metric subspace $(A,d_A)$ is totally bounded (Isometry, isometric embedding, and the subspace metric on a subset).
If $A \subseteq X$ is totally bounded, so is its closure $\overline{A}$ (Interior, closure, boundary, limit point, isolated point and dense subset of a metric space).

No choice principle is used. The one selection made is over a finite index set, which Every natural-number-indexed list of nonempty sets has a choice function on its family of values supplies in ZF.

Facts & Assumptions

Given: A metric space $(X,d)$ and a subset $A \subseteq X$ , with $(A,d_A)$ the metric subspace and $\overline{A}$ the closure of $A$ in $X$ .

[L1]

$(X,d)$ is totally bounded exactly when for every real $\varepsilon > 0$ there is a finite $F \subseteq X$ , empty or listable as $\{y_0, \dots, y_m\}$ , with $X = \bigcup_{y \in F} B(y,\varepsilon)$ (Finite $\varepsilon$ -net and totally bounded metric space, Open ball, closed ball and sphere in a metric space).

[L2]

A subset is bounded when it is empty or contained in a ball $B(x_0,r)$ with $x_0$ in the space and $r > 0$ real (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space).

[L3]

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

[L4]

A nonempty finite set of reals has a maximum, which is one of its members (Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set).

[L5]

Balls of a subspace are traces: $B_A(a,r) = B_X(a,r) \cap A$ for $a \in A$ , $r > 0$ (Isometry, isometric embedding, and the subspace metric on a subset).

[L6]

A function with domain a natural number all of whose values are nonempty sets has a choice function, in ZF (Every natural-number-indexed list of nonempty sets has a choice function on its family of values).

[L7]

$x \in \overline{A}$ exactly when $B(x,r) \cap A \ne \emptyset$ for every real $r > 0$ (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).

Proof

technique · direct

1.1

If $X = \emptyset$ then $X$ is bounded, emptiness being one of the two cases of the definition.

1.2

Suppose instead $X \ne \emptyset$ , and let $F$ be a finite $1$ -net for $(X,d)$ ; then $F \ne \emptyset$ , since a union over an empty family of balls is empty while $X$ is not, so $F = \{y_0, \dots, y_m\}$ for some $m \in \mathbb{N}$ .

2.1

The set $\{\, d(y_0, y_j) : j \le m \,\}$ is a nonempty finite set of reals, so it has a maximum $R$ , and $R \ge d(y_0,y_0) = 0$ .

L3L4step 1.2

3.1

Every $x \in X$ lies in $B(y_j, 1)$ for some $j \le m$ , whence $d(y_0,x) \le d(y_0,y_j) + d(y_j,x) < R + 1$ ; so $X \subseteq B(y_0, R+1)$ with $R + 1 > 0$ , and $X$ is bounded.

L1L2L3step 2.1

4.1

Claim 1 is proved, by step 1.1 in the empty case and by step 3.1 otherwise.

step 1.1step 3.1

5.1

Claim 1 being settled, take up claim 2: assume $(X,d)$ totally bounded, let $A \subseteq X$ , let $\varepsilon > 0$ be real, fix a finite $(\varepsilon/2)$ -net $F = \{y_0, \dots, y_m\}$ for $(X,d)$ , and put $J := \{\, j \le m : B(y_j, \varepsilon/2) \cap A \ne \emptyset \,\}$ .

step 4.1L1

6.1

If $A = \emptyset$ then the empty set is a finite $\varepsilon$ -net for $(A,d_A)$ ; otherwise fix $a^\ast \in A$ , put $S_j := B(y_j,\varepsilon/2) \cap A$ for $j \in J$ and $S_j := A$ for $j \le m$ with $j \notin J$ , all nonempty, and apply finite choice to the function $j \mapsto S_j$ on $\sigma(m)$ to obtain $a_0, \dots, a_m \in A$ with $a_j \in B(y_j, \varepsilon/2)$ for every $j \in J$ .

L6step 5.1

7.1

Put $G := \{a_0, \dots, a_m\} \subseteq A$ , a finite set; given $a \in A$ there is $j \le m$ with $a \in B(y_j, \varepsilon/2)$ , so $j \in J$ and $d(a, a_j) \le d(a,y_j) + d(y_j,a_j) < \varepsilon/2 + \varepsilon/2 = \varepsilon$ , that is $a \in B_A(a_j, \varepsilon)$ .

L3L5step 6.1

8.1

So $G$ is a finite $\varepsilon$ -net for $(A,d_A)$ , and since $\varepsilon > 0$ was arbitrary the subspace $(A,d_A)$ is totally bounded: claim 2 is proved.

L1step 7.1

9.1

Claim 2 being settled, take up claim 3: assume $A \subseteq X$ totally bounded, let $\varepsilon > 0$ be real and fix a finite $(\varepsilon/2)$ -net $F = \{b_0, \dots, b_p\} \subseteq A$ for $(A, d_A)$ , or $F = \emptyset$ when $A = \emptyset$ .

step 8.1L1

10.1

Let $x \in \overline{A}$ ; then $B(x,\varepsilon/2)$ meets $A$ , so there is $a \in A$ with $d(x,a) < \varepsilon/2$ , and $a \in B_A(b_i, \varepsilon/2)$ for some $i \le p$ , whence $d(x,b_i) \le d(x,a) + d(a,b_i) < \varepsilon$ .

L3L5L7step 9.1

11.1

Hence $\overline{A} = \bigcup_{i \le p} B_{\overline{A}}(b_i, \varepsilon)$ with $\{b_0,\dots,b_p\} \subseteq A \subseteq \overline{A}$ finite, so that set is a finite $\varepsilon$ -net for the subspace $\overline{A}$ ; as $\varepsilon > 0$ was arbitrary, $\overline{A}$ is totally bounded and claim 3 is proved.

L1L5step 10.1

12.1

Claims 1, 2 and 3 hold, by steps 4.1, 8.1 and 11.1 respectively.

step 4.1step 8.1step 11.1∎

Remarks

Where the halving is needed. In claim 2 the net of the subspace has to consist of points of $A$ , and a point $y_j$ of a net for $X$ need not lie in $A$ ; moving from $y_j$ to a point of $A$ within $\varepsilon/2$ of it costs the other half of $\varepsilon$ . The same halving appears in claim 3, where the point being approximated lies in the closure rather than in $A$ .

Claim 1 does not reverse. A bounded metric space need not be totally bounded; FALSE: a bounded metric space is totally bounded states the false converse and $\mathbb{N}$ with the discrete metric is bounded and is not totally bounded ↗ exhibits the witness.

Depends on

Used by

ℕ with the discrete metric is bounded and is not totally bounded Counterexample
FALSE: a bounded metric space is totally bounded False statement

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 59 results over 15 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)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 2 (standard reference, not scraped)