Alphabeta Math
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.

✓ 21 results · all verified · 20 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 1 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Compactness in Metric Spaces

1 · Prerequisites

2 · Summary

Compactness in metric spaces turns arbitrary open covers into finite data and supports the finite-intersection method. The page relates compactness to countable, sequential and limit-point compactness, completeness and total boundedness. It records the proof cost where it occurs: several implications are choice-free, constructing an indefinitely separated sequence uses dependent choice, and fixing finite nets at every scale uses countable choice. Compactness of a subset is treated intrinsically, so ambient and subspace cover arguments agree.

The development proves Heine--Borel in Rn and then applies compactness to continuous images, extreme values, Lebesgue numbers, uniform continuity and continuous inverses. It also obtains a countable dense subset under countable choice. Explicit counterexamples separate boundedness, total boundedness and compactness outside Euclidean space, while the choice ledger states which principles the displayed proofs use without asserting independence or necessity.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

Open cover, subcover, compact metric space, and compact subset of a metric space

Definition

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 open sets as in 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 and balls as in Open ball, closed ball and sphere in a metric space.

  • An open cover of (X,d) is a family U of open subsets of X with X=⋃U, where ⋃U={ x∈X:x∈U for some U∈U }.
  • A subcover of U is a subfamily V⊆U that is itself an open cover.
  • A family V of sets is finite when V=∅ or there are n∈N and sets V0,…,Vn with V={V0,…,Vn}; repetitions in the list are allowed and harmless.
  • (X,d) is compact when every open cover of it has a finite subcover: for every open cover U, either X=∅ and the empty subfamily covers it, or there are n∈N and U0,…,Un∈U with X=U0∪⋯∪Un.
  • A subset A⊆X is a compact subset of X when the metric subspace (A,dA) is a compact metric space, dA being the restriction of d to A×A (Isometry, isometric embedding, and the subspace metric on a subset).

Compactness of a subset is defined intrinsically, and only intrinsically. The last clause speaks about the subspace (A,dA) and its own open sets, not about families of open subsets of the ambient X. The two readings do agree, but that is a theorem and not a convention: it is 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, and no item of this library may use the ambient reading without citing it. Taking the intrinsic reading as the definition is what makes "compact" a property of the metric space (A,dA) alone, so that a set compact in one ambient space is compact in every other one containing it isometrically.

The empty space is compact, since the empty subfamily of any family covers it; this is the reason the clause above is written with the two cases. The one-point space is compact too, and so is every space listed as {x0,…,xn}: given a cover, each xi lies in some member, and finitely many members chosen in this way already cover.

The finiteness convention, and how it is used both ways. "Finite" above is the listing form, matching the finite lists of Finite intersection property. It agrees with the definition of finiteness by equinumerosity with a natural number (Finite, countably infinite, countable, uncountable), and both directions of the agreement are available and are used below:

Neither direction uses a choice principle: the second selects nothing, taking a least index instead.

Remarks

Why open covers rather than closed ones. Nothing in the definition would break if U were allowed to consist of arbitrary sets, but the resulting notion would be uninteresting: every space is covered by its singletons, and only a finite space would survive. Openness of the members is what makes the condition a genuine restriction, and it is what 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 has to keep track of when the ambient space changes.

A warning about the word "cover". A family may cover A⊆X without being a family of subsets of A: the members are open subsets of X and their union merely contains A. That is the ambient reading, and it is a different statement from "U is an open cover of the metric space (A,dA)", whose members are open subsets of A. Which of the two is meant is written out everywhere on this page.

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

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

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), let A⊆X and let (A,dA) be the metric subspace (Isometry, isometric embedding, and the subspace metric on a subset). Then:

  1. Relative openness is a trace. A set V⊆A is open in (A,dA) (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) if and only if V=U∩A for some U open in (X,d).
  2. Compactness read in the ambient space. A is a compact subset of X (Open cover, subcover, compact metric space, and compact subset of a metric space), that is (A,dA) is a compact metric space, if and only if for every family U of open subsets of X with A⊆⋃U there are n∈N and U0,…,Un∈U with A⊆U0∪⋯∪Un, or else A=∅.
  3. The same in indexed form. A is a compact subset of X if and only if for every set I and every family (Ui)i∈I of open subsets of X with A⊆⋃i∈IUi there are n∈N and indices i0,…,in∈I with A⊆Ui0∪⋯∪Uin, or else A=∅.

Claim 3 is the form used by almost every later proof on this page, because a cover is usually produced by a rule that attaches an open set to each point or to each index, and a set of open sets forgets that rule. No choice principle is used anywhere below; the one place a selection is made is over a finite index set, and Every natural-number-indexed list of nonempty sets has a choice function on its family of values is a theorem of ZF.

Facts & Assumptions

Given: A metric space (X,d), a subset A⊆X, and the metric subspace (A,dA) with dA the restriction of d to A×A.

[L1]

Balls of a subspace are traces of ambient balls: BA(a,r)=BX(a,r)∩A for a∈A and r>0 (Isometry, isometric embedding, and the subspace metric on a subset, Open ball, closed ball and sphere in a metric space).

[L2]

A subset W of a metric space is open exactly when every point of W has a ball around it contained in W (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).

[L4]

(A,dA) is compact exactly when every family of sets open in (A,dA) whose union is A has a finite subfamily whose union is A; a family is finite when it is empty or listable as {V0,…,Vn} (Open cover, subcover, compact metric space, and compact subset of a metric space).

[L5]

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

Proof

technique · direct
1.1

Suppose U is open in (X,d) and put V:=U∩A; for a∈V we have a∈U, so there is r>0 with BX(a,r)⊆U, whence BA(a,r)=BX(a,r)∩A⊆U∩A=V, and V is open in (A,dA).

L1L2
1.2

Conversely let V⊆A be open in (A,dA), and let W:={ BX(a,r):a∈V, r>0, BX(a,r)∩A⊆V }, a family cut out by a property of the pair (a,r) and not by any selection; put U:=⋃W.

L1construct
2.1

U is open in (X,d), being a union of open balls.

L3step 1.2
2.2

U∩A⊆V, since every member BX(a,r) of W satisfies BX(a,r)∩A⊆V by the defining condition of W.

step 1.2
2.3

V⊆U∩A: given a∈V, openness of V in (A,dA) gives r>0 with BA(a,r)⊆V, that is BX(a,r)∩A⊆V, so BX(a,r)∈W and a∈BX(a,r)⊆U, while a∈A as well.

L1L2step 1.2
3.1

Claim 1 is proved: by steps 2.2 and 2.3 an open V⊆A equals U∩A with U open in X by step 2.1, and conversely every such trace is open in (A,dA) by step 1.1.

step 1.1step 2.1step 2.2step 2.3
4.1

For claim 3, suppose first that (A,dA) is compact, let I be a set and let (Ui)i∈I be open subsets of X with A⊆⋃i∈IUi; then each Ui∩A is open in (A,dA) and V:={ Ui∩A:i∈I } is a family of open subsets of A whose union is A.

step 3.1L4
5.1

If A=∅ the conclusion of claim 3 holds by its second alternative, so assume A≠∅; then V is an open cover of (A,dA), and compactness yields n∈N and V0,…,Vn∈V with A=V0∪⋯∪Vn.

L4step 4.1
6.1

For each j≤n the set Sj:={ i∈I:Ui∩A=Vj } is nonempty by the definition of V, and j↦Sj is a function with domain the natural number σ(n), so a choice function for its values supplies i0,…,in∈I with Uij∩A=Vj for every j≤n.

L5step 5.1
7.1

Hence A=V0∪⋯∪Vn=(Ui0∩A)∪⋯∪(Uin∩A)⊆Ui0∪⋯∪Uin, which is the conclusion of claim 3 for the family (Ui)i∈I, so the forward implication of claim 3 holds.

step 5.1step 6.1
8.1

The converse of claim 3 remains, the forward implication having been settled at step 7.1; so assume the displayed condition, let G be a family of sets open in (A,dA) with union A, and put U:={ U⊆X:U is open in (X,d) and U∩A∈G }, again a family cut out by a property, indexed by itself.

step 7.1step 3.1construct
9.1

A⊆⋃U: given a∈A there is G∈G with a∈G, and by claim 1 there is U open in X with U∩A=G; that U lies in U and contains a.

step 3.1step 8.1
10.1

If A=∅ the empty subfamily of G covers A; otherwise the assumed condition applied to the family U indexed by itself gives m∈N and W0,…,Wm∈U with A⊆W0∪⋯∪Wm.

step 8.1step 9.1
11.1

Putting Gj:=Wj∩A for j≤m gives members of G with A=(W0∩A)∪⋯∪(Wm∩A)=G0∪⋯∪Gm, so G has a finite subcover and (A,dA) is compact.

L4step 10.1
12.1

Claim 3 is proved by steps 7.1 and 11.1, and claim 2 is the special case of claim 3 in which I=U is a family of open subsets of X and Ui:=i, the conclusion of claim 3 then naming members of U itself.

step 7.1step 11.1∎

Remarks

Why the ambient reading needed a proof at all. A subset A of X carries two candidate notions of open cover: families of sets open in (A,dA), and families of sets open in X whose union contains A. Claim 1 is what turns one into the other, and it is the reason compactness of A does not depend on which space A is regarded as sitting inside. Every later item on this page that covers a subset by ambient balls is using claim 2 or claim 3, and says so.

The traces do not remember their sources. A single relatively open V is usually the trace of many different ambient open sets, and that is exactly why step 6.1 has to recover indices at all. Recovering infinitely many at once would be a choice principle; recovering finitely many is not, and the proof is arranged so that only finitely many are ever needed.

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

Countably compact, sequentially compact and limit point compact metric spaces

Definition

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 open sets as in 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 and open covers, subcovers, finiteness and compactness as in Open cover, subcover, compact metric space, and compact subset of a metric space.

A subset A⊆X is called countably compact, sequentially compact or limit point compact when the metric subspace (A,dA) is (Isometry, isometric embedding, and the subspace metric on a subset), exactly as for compactness.

The countable covers may be listed. A nonempty at most countable family U admits a surjection N→U (A nonempty set is at most countable iff it is a surjective image of N), so countable compactness says: for every sequence (Un)n∈N of open sets with X=⋃n∈NUn there are finitely many indices whose sets already cover X. That surjection is produced from the countability assumption alone and no choice principle is involved; the empty family covers only the empty space, which is compact anyway.

Limit points are computed where the set lives. For S⊆A⊆X and a∈A, the identity BA(a,r)=BX(a,r)∩A (Isometry, isometric embedding, and the subspace metric on a subset) shows that a is a limit point of S in the subspace (A,dA) exactly when a is a limit point of S in X and lies in A. So "A is limit point compact" says that every infinite S⊆A has a limit point belonging to A; a limit point outside A does not count, and that is what distinguishes the property from a statement about X.

Remarks

Three conditions, and none of them is compactness by definition. Each of the three weakens or replaces the open-cover condition of Open cover, subcover, compact metric space, and compact subset of a metric space: countable compactness restricts the covers tested, sequential compactness speaks about sequences instead of covers, and limit point compactness speaks about subsets. That the four conditions are not equivalent for topological spaces in general is standard and is quoted from the references, not proved here. For metric spaces they do coincide, but the coincidence is a theorem with a choice cost that varies from implication to implication, and it is proved on this page one arrow at a time (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, 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, 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).

Indexing starts at 0. A sequence here is a function on N and N contains 0 (Sequences of reals: bounded, eventually, frequently, tails, subsequences), so a subsequence is (xnj)j∈N with n0<n1<⋯ and nj≥j (A strictly increasing index map satisfies nk≥k). Every recursive construction of a subsequence on this page produces n0 first and then nj+1>nj, and every radius written 1/(j+1) is written that way because 1/j is undefined at j=0.

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

Finite ε-net and totally bounded metric space

Definition

Let (X,d) be a metric space (Metric space: d(x,y)=0 iff x=y, symmetry, and the triangle inequality; pseudometric and ultrametric) and let ε be a real with ε>0.

The empty space is totally bounded, the empty net serving for every ε, since a union over no indices is empty. Every space listed as {x0,…,xn} is totally bounded too, itself being an ε-net for every ε.

The centres are required to lie in the space. Writing the condition with centres in X and balls of X is what makes total boundedness a property of the metric space (X,d) alone, matching the treatment of compactness in Open cover, subcover, compact metric space, and compact subset of a metric space. For a subset A this matters: the nets of (A,dA) consist of points of A, not of nearby points of the ambient space.

Total boundedness is stronger than boundedness and is not the same thing. A totally bounded space is bounded in the sense of Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space — that is claim 1 of 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 — and the converse fails, as FALSE: a bounded metric space is totally bounded records. Boundedness asks for one ball containing the space; total boundedness asks for finitely many balls of every prescribed radius, and it is the second condition that controls how spread out the space is at small scales.

Remarks

Why ε ranges over the reals here. Convergence and the Cauchy condition are tested against rational ε in this library (Convergence of a sequence in a metric space: xk→x iff d(xk,x)→0 in R, Cauchy sequence in a metric space), because that is how Limits and Cauchy sequences of reals is written; total boundedness is not a limit condition and is stated for real ε>0 directly. Nothing turns on the difference: a net for a rational ε′≤ε is a net for ε, since B(y,ε′)⊆B(y,ε).

A net is not unique and is not part of the data. Total boundedness asserts that nets exist; it names none. Producing one net for each ε simultaneously, as a function of ε, is a further act of selection, and where a proof needs that function it says so and pays for it — see A complete, totally bounded metric space is compact, proved from countable choice used exactly once and A compact metric space has a countable dense subset, by countable choice, each of which spends the Axiom of Countable Choice (The Axiom of Countable Choice (ACω)) exactly once and at exactly that point.

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

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 ε-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:

  1. If (X,d) is totally bounded, it is bounded.
  2. If (X,d) is totally bounded and A⊆X, then the metric subspace (A,dA) is totally bounded (Isometry, isometric embedding, and the subspace metric on a subset).
  3. If A⊆X is totally bounded, so is its closure 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⊆X, with (A,dA) the metric subspace and A‾ the closure of A in X.

[L1]

(X,d) is totally bounded exactly when for every real ε>0 there is a finite F⊆X, empty or listable as {y0,…,ym}, with X=⋃y∈FB(y,ε) (Finite ε-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(x0,r) with x0 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)≤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: BA(a,r)=BX(a,r)∩A for a∈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).

Proof

technique · direct
1.1

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

L2
1.2

Suppose instead X≠∅, and let F be a finite 1-net for (X,d); then F≠∅, since a union over an empty family of balls is empty while X is not, so F={y0,…,ym} for some m∈N.

L1
2.1

The set { d(y0,yj):j≤m } is a nonempty finite set of reals, so it has a maximum R, and R≥d(y0,y0)=0.

L3L4step 1.2
3.1

Every x∈X lies in B(yj,1) for some j≤m, whence d(y0,x)≤d(y0,yj)+d(yj,x)<R+1; so X⊆B(y0,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⊆X, let ε>0 be real, fix a finite (ε/2)-net F={y0,…,ym} for (X,d), and put J:={ j≤m:B(yj,ε/2)∩A≠∅ }.

step 4.1L1
6.1

If A=∅ then the empty set is a finite ε-net for (A,dA); otherwise fix a∗∈A, put Sj:=B(yj,ε/2)∩A for j∈J and Sj:=A for j≤m with j∉J, all nonempty, and apply finite choice to the function j↦Sj on σ(m) to obtain a0,…,am∈A with aj∈B(yj,ε/2) for every j∈J.

L6step 5.1
7.1

Put G:={a0,…,am}⊆A, a finite set; given a∈A there is j≤m with a∈B(yj,ε/2), so j∈J and d(a,aj)≤d(a,yj)+d(yj,aj)<ε/2+ε/2=ε, that is a∈BA(aj,ε).

L3L5step 6.1
8.1

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

L1step 7.1
9.1

Claim 2 being settled, take up claim 3: assume A⊆X totally bounded, let ε>0 be real and fix a finite (ε/2)-net F={b0,…,bp}⊆A for (A,dA), or F=∅ when A=∅.

step 8.1L1
10.1

Let x∈A‾; then B(x,ε/2) meets A, so there is a∈A with d(x,a)<ε/2, and a∈BA(bi,ε/2) for some i≤p, whence d(x,bi)≤d(x,a)+d(a,bi)<ε.

L3L5L7step 9.1
11.1

Hence A‾=⋃i≤pBA‾(bi,ε) with {b0,…,bp}⊆A⊆A‾ finite, so that set is a finite ε-net for the subspace A‾; as ε>0 was arbitrary, 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 yj of a net for X need not lie in A; moving from yj to a point of A within ε/2 of it costs the other half of ε. 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 N with the discrete metric is bounded and is not totally bounded ↗ exhibits the witness.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

A metric space is compact if and only if every family of closed subsets with the finite intersection property has nonempty intersection

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 closed sets as in 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 and the finite intersection property as in Finite intersection property. For a family A of subsets of X write

⋂A  :=  { x∈X:x∈F for every F∈A },

so that ⋂∅=X, matching the convention for the empty finite intersection in Finite intersection property.

Then (X,d) is compact (Open cover, subcover, compact metric space, and compact subset of a metric space) if and only if every family A of closed subsets of X with the finite intersection property satisfies ⋂A≠∅.

No choice principle is used in either direction: complementation is a canonical bijection, so no member of a family ever has to be selected.

Facts & Assumptions

Given: A metric space (X,d), families of subsets of X, and the two notions above.

[A1]

Elementary set algebra inside X: X∖(X∖S)=S for S⊆X, and for any family S of subsets of X one has X∖⋃S=⋂{ X∖S:S∈S } and X∖⋂S=⋃{ X∖S:S∈S }.

[L1]

(X,d) is compact exactly when every family of open subsets of X with union X has a finite subfamily with union X, the empty subfamily serving when X=∅ (Open cover, subcover, compact metric space, and compact subset of a metric space).

[L3]

A has the finite intersection property exactly when ⋂i∈ns(i)≠∅ for every n∈N and every finite list s:n→A, the empty list having intersection X (Finite intersection property).

Proof

technique · direct
1.1

Complementation inside X is its own inverse, and it exchanges the open subsets of X with the closed ones: X∖(X∖S)=S, and S is open exactly when X∖S is closed.

A1L2
1.2

For any family S of subsets of X, the union of S is X exactly when the intersection of the complements is empty, and the intersection of S is empty exactly when the union of the complements is X.

A1
2.1

In particular, for F0,…,Fn⊆X one has F0∩⋯∩Fn=∅ exactly when (X∖F0)∪⋯∪(X∖Fn)=X.

A1step 1.2
3.1

Assume (X,d) compact, let A be a family of closed subsets of X with the finite intersection property, and suppose for contradiction that ⋂A=∅.

L1L3step 2.1assume-contra
4.1

Applying the finite intersection property to the empty list gives X≠∅; and U:={ X∖F:F∈A } is a family of open subsets of X whose union is X∖⋂A=X, hence an open cover of X.

L2L3step 1.1step 1.2step 3.1
5.1

Compactness applied to U, together with X≠∅, gives n∈N and U0,…,Un∈U with X=U0∪⋯∪Un.

L1step 4.1
6.1

Each Ui is X∖Fi for the set Fi:=X∖Ui, which lies in A and is determined by Ui alone; so F0∩⋯∩Fn=∅ by step 2.1, and the list i↦Fi contradicts the finite intersection property of A.

L3step 1.1step 2.1step 5.1discharge-contradiction
7.1

Therefore ⋂A≠∅, which is the forward implication.

step 6.1
8.1

Conversely assume that every family of closed subsets of X with the finite intersection property has nonempty intersection, let U be a family of open subsets of X with union X, and suppose for contradiction that no finite subfamily of U has union X.

L1step 7.1assume-contra
9.1

Then X≠∅, since otherwise the empty subfamily would have union X; and A:={ X∖U:U∈U } is a family of closed subsets of X.

L2step 1.1step 8.1
10.1

A has the finite intersection property: the empty list has intersection X≠∅, and a list F0,…,Fn of members of A has Fi=X∖Ui with Ui:=X∖Fi∈U, so F0∩⋯∩Fn=∅ would give U0∪⋯∪Un=X by step 2.1, a finite subfamily with union X.

L3step 2.1step 9.1
11.1

By the assumed condition ⋂A≠∅; but ⋂A=X∖⋃U=∅ because U has union X, and this contradiction is the required one.

step 1.2step 10.1discharge-contradiction
12.1

Hence some finite subfamily of U has union X, so (X,d) is compact, and with step 7.1 both implications are proved.

L1step 7.1step 11.1∎

Remarks

The empty family and the empty space. The conventions are not decoration. ⋂∅=X makes the finite intersection property fail outright for every family of subsets of the empty space, so the right-hand condition is vacuously true there; and the empty space is compact, the empty subfamily covering it. The equivalence therefore holds at X=∅ as well, with both sides true.

Why no choice is spent. The natural-looking step "the finite subcover consists of sets X∖Fi, so pick Fi∈A" would be a selection if a member of the family could be the complement of several different members. It cannot: complementation inside X is injective, so Fi is recovered from Ui by a formula. That is the whole reason this characterisation, and the completeness half of A compact metric space is complete and totally bounded, and neither implication uses any choice principle that runs through it, cost nothing.

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

A closed subset of a compact metric space is compact

Facts & Assumptions

Given: A compact metric space (X,d) and a closed subset F⊆X.

[L1]

(X,d) is compact: every family of open subsets of X with union X has a finite subfamily with union X (Open cover, subcover, compact metric space, and compact subset of a metric space).

[L2]

A subset A⊆X is a compact subset exactly when for every set I and every family (Ui)i∈I of open subsets of X with A⊆⋃i∈IUi there are n∈N and i0,…,in∈I with A⊆Ui0∪⋯∪Uin, or else A=∅; and X is a compact subset of itself, its subspace metric being d (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, Isometry, isometric embedding, and the subspace metric on a subset).

Proof

technique · direct
1.1

X∖F is open in X.

L3
1.2

By the ambient characterisation it suffices to show that every family (Ui)i∈I of open subsets of X with F⊆⋃i∈IUi has finitely many members whose union contains F, or that F=∅; so fix such a family.

L2suffices: finitely many members cover F
2.1

Take an object ∗ not in I, put I+:=I∪{∗} and U∗:=X∖F; then (Ui)i∈I+ is a family of open subsets of X whose union is X, since a point outside F lies in U∗ and a point of F lies in some Ui with i∈I.

L1L2step 1.1step 1.2
3.1

Applying the ambient characterisation to the compact subset X of itself gives n∈N and j0,…,jn∈I+ with X=Uj0∪⋯∪Ujn, unless X=∅, in which case F=∅ and there is nothing to prove.

L2step 2.1
4.1

Delete from the list j0,…,jn every entry equal to ∗; what remains is a finite list of indices from I, possibly empty, and the union of the corresponding sets still contains F, because U∗=X∖F contains no point of F while every point of F lies in one of the listed sets.

step 3.1
5.1

If that remaining list is empty then F=∅, and otherwise it exhibits finitely many members of (Ui)i∈I whose union contains F; in both cases the condition of step 1.2 is met, so F is a compact subset of X.

L2step 1.2step 4.1∎

Remarks

The hypothesis that X is compact cannot be dropped, and neither can closedness. A closed subset of a non-compact space need not be compact: the whole space is closed in itself. And a non-closed subset of a compact space need not be compact, since a compact subset of any metric space is closed (A compact subset of a metric space is closed and bounded).

Why the augmented family is the whole trick. The set F is covered by the Ui, but X need not be; adjoining the single open set X∖F repairs that at no cost, and it is the only member of the resulting finite subcover that has to be discarded again at the end.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

A compact subset of a metric space is closed and bounded

Statement

Facts & Assumptions

Given: A metric space (X,d) and a compact subset K⊆X.

[L1]

K is a compact subset exactly when for every set I and every family (Ui)i∈I of open subsets of X with K⊆⋃i∈IUi there are n∈N and i0,…,in∈I with K⊆Ui0∪⋯∪Uin, or else K=∅ (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).

[L2]

For p≠x in X and r:=d(p,x)/2 one has r>0 and B(p,r)∩B(x,r)=∅ (Distinct points of a metric space have disjoint balls around them).

[L4]

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

[L5]

A subset is bounded when it is empty or contained in some ball B(x0,r) with r>0; and B(x0,s)⊆B(x0,r) whenever 0<s≤r (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space, Open ball, closed ball and sphere in a metric space).

Proof

technique · direct
1.1

If K=∅ then K is bounded by the first clause of the definition, and it is closed because X∖K=X is open.

L3L5
1.2

Assume from now on that K≠∅ and fix p∈K; the family (B(p,r))r∈P indexed by the set P of positive reals consists of open sets and covers K, since every x∈K satisfies d(p,x)<d(p,x)+1 and so lies in B(p,d(p,x)+1).

L3L5
2.1

The indexed characterisation gives n∈N and positive reals r0,…,rn with K⊆B(p,r0)∪⋯∪B(p,rn); putting R:=max⁡{r0,…,rn}, a positive real, the balls with common centre p are nested, so K⊆B(p,R) and K is bounded.

L1L4L5step 1.2
3.1

Boundedness being settled, take up closedness: let q∈X∖K and for each x∈K put rx:=d(q,x)/2, which is a positive real because q≠x, and which satisfies B(q,rx)∩B(x,rx)=∅.

L2step 2.1
4.1

The family (B(x,rx))x∈K consists of open subsets of X and covers K, since x∈B(x,rx); so there are n∈N and x0,…,xn∈K with K⊆B(x0,rx0)∪⋯∪B(xn,rxn).

L1L3step 3.1
5.1

Put r:=min⁡{rx0,…,rxn}, a positive real.

L4step 4.1
6.1

Then B(q,r)∩K=∅: a point y of the intersection would lie in B(xi,rxi) for some i≤n by step 4.1, and also in B(q,r)⊆B(q,rxi) by step 5.1, whereas those two balls are disjoint by step 3.1.

L5step 3.1step 4.1step 5.1
7.1

So every point of X∖K has a ball around it inside X∖K, that set is open, and K is closed; together with steps 1.1 and 2.1 this proves the theorem.

L3step 1.1step 2.1step 6.1∎

Remarks

Both conclusions use compactness through the same characterisation. The first cover is by concentric balls of every positive radius, which is what boundedness is about; the second is by balls small enough to keep a fixed outside point away, which is what closedness is about. In each case what compactness returns is a finite list of indices, and a maximum or a minimum of finitely many positive reals then does the rest.

Hausdorffness is what makes the second argument work, and every metric space has it (Distinct points of a metric space have disjoint balls around them). The statement is false for topological spaces without that separation property, which is why the proof cites the separation lemma rather than the metric axioms directly.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)verified 2026-08-04 (gpt-5.6-sol-codex-subscription)Open item page →

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 ε-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).

[L2]

(X,d) is totally bounded exactly when for every real ε>0 there is a finite F⊆X with X=⋃y∈FB(y,ε) (Finite ε-net and totally bounded metric space).

[L3]

X is a compact subset of itself, and for every family (Ui)i∈I of open subsets of X with X=⋃i∈IUi there are n∈N and i0,…,in∈I with X=Ui0∪⋯∪Uin, unless X=∅ (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; (xk) is Cauchy when for every rational ε>0 there is K with d(xm,xl)<ε for all m,l≥K; and xk→p when for every rational ε>0 there is K with d(xk,p)<ε for all k≥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: xk→x iff d(xk,x)→0 in R).

[L5]

The closure S‾ of S⊆X is closed, contains S, and is contained in every closed superset of S; and x∈S‾ exactly when B(x,r)∩S≠∅ 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).

[L8]

A finite list n0,…,np of natural numbers has a greatest member. Indeed the reals ι(n0+1),…,ι(np+1), with ι the canonical natural of R (The canonical natural ι(n)=n⋅1F of a field), form a nonempty finite set of reals and so have a maximum, which is one of them, say ι(nj+1) (Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set); the map m↦ι(m) is strictly increasing on the naturals ≥1 (Canonical naturals are positive and strictly increasing), so nj<ni would force ι(nj+1)<ι(ni+1), which the maximality forbids, and the order of N is linear (≤ is a linear order on N), whence ni≤nj for every i≤p.

Proof

technique · direct
1.1

Let ε>0 be real; the family (B(x,ε))x∈X consists of open subsets of X and has union X, since x∈B(x,ε) for every x.

L1L2
2.1

If X=∅ the empty set is a finite ε-net; otherwise the indexed characterisation gives n∈N and x0,…,xn∈X with X=B(x0,ε)∪⋯∪B(xn,ε), so {x0,…,xn} is a finite ε-net; as ε was arbitrary, (X,d) is totally bounded.

L2L3step 1.1
3.1

Total boundedness being settled, take up completeness: let (xk) be a Cauchy sequence in X and put Tn:={ xk:k≥n }‾ for n∈N, a definition by a rule and not by a selection.

L4L5step 2.1
4.1

Each Tn is closed and nonempty, containing xn; and Tm⊆Tn whenever m≥n, since then {xk:k≥m}⊆{xk:k≥n}⊆Tn and Tm is the smallest closed superset of the first of these sets.

L5step 3.1
5.1

The family A:={ Tn:n∈N } of closed sets has the finite intersection property: the empty list has intersection X, which contains x0; and for a list Tn0,…,Tnp take a greatest member nj of the list of indices, so that Tnj⊆Tni for every i≤p and xnj lies in every one of them.

L6L8step 4.1
6.1

By the finite intersection characterisation of compactness there is a point p∈⋂A, that is p∈Tn for every n∈N.

L6step 5.1
7.1

Let ε>0 be rational and take K∈N with d(xm,xl)<ε/2 for all m,l≥K; since p∈TK, the ball B(p,ε/2) meets {xk:k≥K}, so there is j≥K with d(p,xj)<ε/2, and then d(xk,p)≤d(xk,xj)+d(xj,p)<ε/2+ε/2=ε for every k≥K.

L4L5L7step 6.1
8.1

Hence xk→p with p∈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 Tn 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 (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.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passverified 2026-08-04 (gpt-5.6-sol-codex-subscription)Open item page →

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

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 compactness as in Open cover, subcover, compact metric space, and compact subset of a metric space and the three variants as in Countably compact, sequentially compact and limit point compact metric spaces. Then:

  1. If (X,d) is compact, it is countably compact.
  2. If (X,d) is compact, it is limit point compact.
  3. If (X,d) is countably compact, it is sequentially compact.
  4. If (X,d) is limit point compact, it is sequentially compact.

Every one of the four is a theorem of ZF. Where a subsequence is extracted, the index at each stage is the least admissible one, which The well-ordering principle makes canonical and The recursion theorem then assembles into a function; where finitely many indices have to be recovered from finitely many sets, Every natural-number-indexed list of nonempty sets has a choice function on its family of values supplies them and is itself a theorem of ZF. Nothing below appeals to countable or to dependent choice.

Facts & Assumptions

Given: A metric space (X,d), whichever of the four properties is assumed in the claim under proof.

[L1]

The definitions: (X,d) is compact when every family of open subsets with union X has a finite subfamily with union X; countably compact when every such family that is at most countable does; sequentially compact when every sequence has a subsequence converging in X; limit point compact when every infinite subset has a limit point in X, where p is a limit point of A when B(p,r)∩(A∖{p})≠∅ for every real r>0 (Open cover, subcover, compact metric space, and compact subset of a metric space, Countably compact, sequentially compact and limit point compact metric spaces, Interior, closure, boundary, limit point, isolated point and dense subset of a metric space, Sequences of reals: bounded, eventually, frequently, tails, subsequences).

[L4]

The closure S‾ is closed, contains S and is the smallest closed superset of S; and x∈S‾ exactly when B(x,r)∩S≠∅ 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).

[L5]

Recursion: for a set A, an element a∈A and a function f:A→A there is a unique g:N→A with g(0)=a and g(n+1)=f(g(n)); when the recursion rule depends on the stage, it is applied to A=N×Z and the first coordinate of g(n) is n, by the small induction recorded in Finite sums and finite products, by recursion (The recursion theorem).

[L6]

Every nonempty subset of N has a least element (The well-ordering principle).

[L7]

A finite list n0,…,np of natural numbers has a greatest member: the reals ι(n0+1),…,ι(np+1), with ι the canonical natural of R (The canonical natural ι(n)=n⋅1F of a field), form a nonempty finite set of reals and so have a maximum, which is one of them, say ι(nj+1) (Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set); m↦ι(m) is strictly increasing on the naturals ≥1 (Canonical naturals are positive and strictly increasing) and the order of N is linear (≤ is a linear order on N), so ni≤nj for every i≤p.

[L8]

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

[L9]

Finiteness: a set listed as {a0,…,an} is finite, a nonempty finite set can be listed, and a subset of N bounded above is finite (Open cover, subcover, compact metric space, and compact subset of a metric space, Finite, countably infinite, countable, uncountable, Every subset of an at most countable set is at most countable); an injection carries a set to a set in bijection with its image (Injection, surjection, bijection).

[L10]

A family indexed by N is at most countable, being the image of a surjection from N (Finite, countably infinite, countable, uncountable, A nonempty set is at most countable iff it is a surjective image of N).

[L11]

xk→p when for every rational ε>0 there is K with d(xk,p)<ε for k≥K; and for every real ε>0 there is a natural N≥1 with 1/N<ε (Convergence of a sequence in a metric space: xk→x iff d(xk,x)→0 in R, For every ε>0 in a complete ordered field there is a natural n≥1 with 1/n<ε, Every complete ordered field is Archimedean).

[L12]

An index map n:N→N with nk<nk+1 for every k is strictly increasing, and then nk≥k (A strictly increasing index map satisfies nk≥k).

[L13]

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).

[L14]

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

Proof

technique · direct
1.1

Claim 1 is immediate: an at most countable family of open sets with union X is in particular a family of open sets with union X, so compactness supplies the finite subfamily that countable compactness asks for.

L1
2.1

For claim 2, assume (X,d) compact, let A⊆X have no limit point in X, and put U:={ U⊆X:U open in X and U∩A has at most one element }, a family cut out by a property; U has union X, because each p∈X fails to be a limit point of A and so admits r>0 with B(p,r)∩(A∖{p})=∅, whence B(p,r)∈U and p∈B(p,r).

L1L3step 1.1
3.1

Compactness gives n∈N and U0,…,Un∈U with X=U0∪⋯∪Un, unless X=∅, in which case A=∅ is finite.

L1step 2.1
4.1

Define φ:A→σ(n) by letting φ(a) be the least i≤n with a∈Ui; this is well defined and canonical, and it is injective, since φ(a)=φ(b)=i puts both a and b in Ui∩A, a set with at most one element. Hence A is in bijection with φ[A], a subset of N bounded above by n, so A is finite.

L6L9step 3.1
5.1

So a subset of X with no limit point in X is finite; contrapositively every infinite subset of X has a limit point in X, and (X,d) is limit point compact: claim 2.

L1step 4.1
6.1

For claim 3, assume (X,d) countably compact, let (xk) be a sequence in X and put Tn:={ xk:k≥n }‾ for n∈N.

L1L4step 5.1
7.1

Each Tn is closed and contains xn, and Tm⊆Tn whenever m≥n, because {xk:k≥m}⊆{xk:k≥n}⊆Tn and Tm is the smallest closed superset of the first set.

L4step 6.1
8.1

Suppose for contradiction that ⋂n∈NTn=∅; then V:={ X∖Tn:n∈N } is an at most countable family of open subsets of X whose union is X∖⋂nTn=X.

L3L10step 7.1assume-contra
9.1

Countable compactness gives a finite subfamily V0,…,Vp of V with union X; putting Wi:=X∖Vi, each Wi equals Tn for at least one n, so finite choice applied to i↦{ n∈N:Tn=Wi } yields indices n0,…,np with Wi=Tni, and a greatest member nj of that list satisfies Tnj⊆Tni for every i≤p.

L7L13step 8.1
10.1

Then Tnj=Tn0∩⋯∩Tnp=X∖(V0∪⋯∪Vp)=∅, contradicting xnj∈Tnj.

step 7.1step 9.1discharge-contradiction
11.1

Hence there is p∈X with p∈Tn for every n∈N.

step 10.1
12.1

For every k∈N and every m∈N the set { j∈N:j>m and d(xj,p)<1/(k+2) } is nonempty, since p∈Tm+1 means that the ball B(p,1/(k+2)) meets {xj:j≥m+1}; so it has a least element, and likewise { j:d(xj,p)<1 } is nonempty and has a least element m0.

L4L6L11step 11.1
13.1

Applying recursion on N×N to the starting value (0,m0) and the rule f(k,m):=(k+1, the least j>m with d(xj,p)<1/(k+2)) produces g:N→N×N whose first coordinate at k is k; write nk for its second coordinate.

L5step 12.1
14.1

Then nk<nk+1 for every k, so k↦nk is strictly increasing, and d(xnk,p)<1/(k+1) for every k, the case k=0 being the choice of m0.

L12step 13.1
15.1

Given a rational ε>0 take a natural N≥1 with 1/N<ε; for k≥N one has k+1>N and so d(xnk,p)<1/(k+1)<1/N<ε. Hence xnk→p, the sequence (xk) has a convergent subsequence, and (X,d) is sequentially compact: claim 3.

L1L11step 14.1
16.1

For claim 4, assume (X,d) limit point compact, let (xk) be a sequence in X and let R:={ xk:k∈N } be its range, a nonempty subset of X.

L1step 15.1
17.1

Suppose first that R is finite, and list it as R={v0,…,vm}; putting Si:={ k∈N:xk=vi } for i≤m gives N=S0∪⋯∪Sm.

L9step 16.1
18.1

Some Si is unbounded in N: otherwise each Si has an upper bound in N and hence a least upper bound Ni, canonical by well-ordering, and a greatest member N of the list N0,…,Nm would satisfy N+1>Ni for every i, so that N+1 lies in no Si, against N=S0∪⋯∪Sm. Let i∗ be the least i≤m for which Si is unbounded.

L6L7step 17.1
19.1

Recursion applied to the starting value min⁡Si∗ and the rule f(m):=min⁡{ k∈Si∗:k>m }, each of these sets being nonempty because Si∗ is unbounded, produces a strictly increasing k↦nk with xnk=vi∗ for every k; a constant sequence converges to its value, so xnk→vi∗∈X.

L5L6L11L12L14step 18.1
20.1

Suppose instead that R is infinite; limit point compactness then gives a limit point p∈X of R.

L1step 19.1
21.1

Suppose for contradiction that some real r>0 and some N∈N satisfy d(xk,p)≥r for every k≥N.

step 20.1assume-contra
22.1

Let E be the set listed by r together with the N entries ek for k<N, where ek:=d(xk,p) if xk≠p and ek:=r otherwise; every listed entry is a positive real, so E is a nonempty finite set of positive reals and s:=min⁡E>0. Then B(p,s) misses R∖{p}: a point of R∖{p} is xk with xk≠p, and d(xk,p)≥r≥s when k≥N, while d(xk,p)=ek≥s when k<N. That contradicts p being a limit point of R.

L1L8L14step 21.1discharge-contradiction
23.1

Hence for every real r>0 and every N∈N there is k≥N with d(xk,p)<r.

step 22.1
24.1

Consequently, for every k and every m the set { j>m:d(xj,p)<1/(k+2) } is nonempty, as is { j:d(xj,p)<1 }, and the recursion of steps 13.1 and 14.1 applies verbatim, producing a strictly increasing k↦nk with d(xnk,p)<1/(k+1); by the estimate of step 15.1, xnk→p.

L5L6L11L12step 13.1step 14.1step 15.1step 23.1
25.1

In both cases (xk) has a subsequence converging in X, so (X,d) is sequentially compact: claim 4.

L1step 19.1step 24.1
26.1

Claims 1, 2, 3 and 4 are proved by steps 1.1, 5.1, 15.1 and 25.1 respectively.

step 1.1step 5.1step 15.1step 25.1∎

Remarks

Why "least" and not "some". At every stage of every recursion above, the next index is the least one meeting the requirement. That is what keeps the four implications inside ZF: a rule that says "take some admissible j" would be a selection made infinitely often, and one made in terms of the previous stage, which is dependent choice (The axiom of dependent choice: a relation in which every element is related to something admits an N-indexed chain) rather than countable choice. The same device is what A sequentially compact metric space is totally bounded, proved from the axiom of dependent choice cannot use, and that is exactly why that theorem, alone among the implications between the compactness properties on this page, costs dependent choice. It is not the only implication on the page with a choice cost: A complete, totally bounded metric space is compact, proved from countable choice used exactly once spends countable choice, for the different reason that it needs one net for every radius at once. The arrow-by-arrow accounting 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.

Finite selections are free. Step 9.1 does select, but only over the finite index set {0,…,p}, and Every natural-number-indexed list of nonempty sets has a choice function on its family of values proves that such a selection exists in ZF by induction on the size of the index set. Nothing is being smuggled in: what a choice principle buys is infinitely many selections at once.

The two routes to sequential compactness are genuinely different. Claim 3 works with the closures of the tails of the given sequence and needs the countable cover they generate; claim 4 works with the range of the sequence and splits on whether it is finite. Neither argument subsumes the other, and both are needed, because the equivalence proved in 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 passes through both.

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

A sequentially compact metric space is complete, with no choice principle used

Statement

Let (X,d) be a sequentially compact metric space (Countably compact, sequentially compact and limit point compact metric spaces, Metric space: d(x,y)=0 iff x=y, symmetry, and the triangle inequality; pseudometric and ultrametric). Then (X,d) is complete (Complete metric space: every Cauchy sequence converges in the space).

The proof is a theorem of ZF: it instantiates two existential statements and selects nothing.

Facts & Assumptions

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

[L2]

(X,d) is complete when every Cauchy sequence in X converges to a point of X (Complete metric space: every Cauchy sequence converges in the space, Cauchy sequence in a metric space).

[L3]

A Cauchy sequence with a subsequence converging to p converges to p itself (A Cauchy sequence in a metric space with a convergent subsequence converges to that subsequence’s limit).

Proof

technique · direct
1.1

Let (xk) be a Cauchy sequence in (X,d).

L2
2.1

By sequential compactness there is a strictly increasing index map j↦nj and a point p∈X with xnj→p in (X,d).

L1step 1.1
3.1

Since (xk) is Cauchy and one of its subsequences converges to p, the whole sequence converges to p, and p∈X.

L3step 2.1
4.1

So every Cauchy sequence in (X,d) converges in X, that is (X,d) is complete.

L2step 3.1∎

Remarks

The converse fails. A complete metric space need not be sequentially compact: R with its usual metric is complete, and the sequence xk=k has no convergent subsequence, every subsequence being unbounded. What has to be added to completeness is total boundedness, and that pair is equivalent to compactness (A complete, totally bounded metric space is compact, proved from countable choice used exactly once, 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).

Why this direction is free while the companion is not. Here the sequence is handed to the proof and sequential compactness hands back a subsequence: one object is produced, once. In A sequentially compact metric space is totally bounded, proved from the axiom of dependent choice a point has to be produced at every stage, each in terms of the points already produced, and that is where a choice principle enters the page.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

A sequentially compact metric space is totally bounded, proved from the axiom of dependent choice

Statement

Assume the Axiom of Dependent Choice (The axiom of dependent choice: a relation in which every element is related to something admits an N-indexed chain). Let (X,d) be a sequentially compact metric space (Countably compact, sequentially compact and limit point compact metric spaces, Metric space: d(x,y)=0 iff x=y, symmetry, and the triangle inequality; pseudometric and ultrametric). Then (X,d) is totally bounded (Finite ε-net and totally bounded metric space).

What is claimed about the cost, and what is not. Claimed: the proof below is carried out in ZF+DC, and DC is used exactly once, at step 5.1. Not claimed: that DC is necessary for the statement. Establishing necessity would mean separating the statement from ZF, which is an independence result, and this library proves none. The reason countable choice is not used instead is that the point added at each stage has to be at distance at least ε from the points already produced, so the set it is drawn from depends on the earlier stages; the first remark below spells that out.

Facts & Assumptions

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

[L2]

(X,d) is totally bounded when for every real ε>0 there is a finite F⊆X, empty or listable, with X=⋃y∈FB(y,ε); equivalently, when for every real ε>0 some finite list y0,…,ym−1 of points of X satisfies: every x∈X has d(x,yi)<ε for some i<m (Finite ε-net and totally bounded metric space, Open ball, closed ball and sphere in a metric space).

[L3]

Dependent choice: for a nonempty set S, a relation R on S with every element R-related to some element, and any a∈S, there is a sequence (tn) in S with t0=a and tnRtn+1 for every n (The axiom of dependent choice: a relation in which every element is related to something admits an N-indexed chain).

[L4]

A convergent sequence is Cauchy: if ynj→p then for every rational ε>0 there is K with d(ynj,ynl)<ε for all j,l≥K (Every convergent sequence in a metric space is Cauchy, Cauchy sequence in a metric space).

[L5]

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

[L6]

For every real η>0 there is a natural N≥1 with 1/N<η, and 1/N is a positive rational (For every ε>0 in a complete ordered field there is a natural n≥1 with 1/n<ε, Every complete ordered field is Archimedean).

Proof

technique · contradiction
1.1

Suppose (X,d) is sequentially compact and not totally bounded, and fix a real ε>0 for which no finite subset of X is an ε-net.

L1L2assume-contra
2.1

Then X≠∅, since for X=∅ the empty set is an ε-net.

L2step 1.1
3.1

Let S be the set of ε-separated finite tuples in X, that is of functions t:m→X with m∈N and d(t(i),t(j))≥ε whenever i<j<m; the empty function, with m=0, lies in S, so S≠∅.

L5step 2.1
4.1

Let tRt′ mean that t′:m+1→X extends t:m→X by one term with d(t′(m),t(i))≥ε for every i<m; then R is a relation on S and every t∈S is R-related to some element of S, because the finite set {t(0),…,t(m−1)} is not an ε-net, so some x∈X has d(x,t(i))≥ε for every i<m, and the extension of t by x lies in S.

L2L5step 3.1
5.1

Dependent choice, applied to S, to R and to the empty function as starting point, yields a sequence (tn) in S with t0 the empty function and tnRtn+1 for every n; this is the only appeal to a choice principle in the proof.

L3step 4.1
6.1

Each tn has domain n and tn+1 restricted to n is tn, both by induction on n from the definition of R; so yn:=tn+1(n) defines a sequence (yn) in X, and for i<j both yi=tj+1(i) and yj=tj+1(j) hold, whence d(yi,yj)≥ε.

L5step 5.1
7.1

Sequential compactness gives a strictly increasing j↦nj and p∈X with ynj→p; that subsequence is therefore Cauchy, so, taking a natural N≥1 with 1/N<ε and testing the Cauchy condition at the positive rational 1/N, there is K∈N with d(ynj,ynl)<1/N<ε for all j,l≥K.

L1L4L6step 6.1
8.1

But nK<nK+1, so step 6.1 gives d(ynK,ynK+1)≥ε, contradicting step 7.1; the assumption of step 1.1 is therefore untenable, every real ε>0 admits a finite ε-net, and (X,d) is totally bounded.

L2step 6.1step 7.1discharge-contradiction∎

Remarks

Why countable choice is not what this proof uses. A natural attempt is to apply ACω to the family whose n-th member is the set of ε-separated n-tuples, each of which is nonempty by the argument of step 4.1. What that returns is one ε-separated n-tuple for each n, with no relation whatever between the tuple chosen at n and the one chosen at n+1: the tuples need not extend one another, need not share a single point, and nothing in the data assembles them into one ε-separated sequence. The relation R of step 4.1 is precisely the coherence that is missing, and building a sequence along a relation is what The axiom of dependent choice: a relation in which every element is related to something admits an N-indexed chain is. This is an observation about the argument given here; it is not a proof that ACω is insufficient for the theorem.

The passage to a rational ε in step 7.1. Convergence and the Cauchy condition are tested against rational ε in this library (Convergence of a sequence in a metric space: xk→x iff d(xk,x)→0 in R, Cauchy sequence in a metric space), while the ε of step 1.1 is an arbitrary positive real. The reciprocal form of the Archimedean property supplies a positive rational 1/N below it (For every ε>0 in a complete ordered field there is a natural n≥1 with 1/n<ε), and the contradiction is unaffected: a Cauchy estimate at 1/N≤ε still contradicts a separation of at least ε.

This is the only implication on the page that costs dependent choice, and it is the reason 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 carries DC among its hypotheses. The full accounting 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.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

A complete, totally bounded metric space is compact, proved from countable choice used exactly once

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice (ACω)). Let (X,d) be a metric space (Metric space: d(x,y)=0 iff x=y, symmetry, and the triangle inequality; pseudometric and ultrametric) that is complete (Complete metric space: every Cauchy sequence converges in the space) and totally bounded (Finite ε-net and totally bounded metric space). Then (X,d) is compact (Open cover, subcover, compact metric space, and compact subset of a metric space).

Where the axiom is spent, and why the weaker principle suffices. ACω is used exactly once, at step 3.1, to fix one finite 1/(n+1)-net together with a listing of it for every n∈N at once. The family of sets being chosen from is written down before any selection is made and does not depend on the earlier selections, which is precisely the situation countable choice covers and dependent choice (The axiom of dependent choice: a relation in which every element is related to something admits an N-indexed chain) is not needed for. Everything after step 3.1 is canonical: at each stage the construction takes the least admissible index in the listing already fixed.

As always on this page, the claim is an upper bound on the cost of the proof given here, not an assertion that ACω is necessary for the theorem.

Facts & Assumptions

Given: A complete, totally bounded metric space (X,d), an open cover of it, and the Axiom of Countable Choice.

[L1]

(X,d) is compact when every family U of open subsets of X with union X has a finite subfamily with union X; U open means every point of U has a ball around it inside U (Open cover, subcover, compact metric space, and compact subset of 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, Open ball, closed ball and sphere in a metric space).

[L2]

(X,d) is totally bounded: for every real δ>0 there is a finite F⊆X with X=⋃y∈FB(y,δ), and a nonempty finite set can be listed (Finite ε-net and totally bounded metric space, Open cover, subcover, compact metric space, and compact subset of a metric space).

[L3]

Countable choice: for a family (En)n∈N of nonempty sets there is a function n↦en with en∈En for every n (The Axiom of Countable Choice (ACω)).

[L4]

Recursion: for a set A, an element a∈A and a function f:A→A there is a unique g:N→A with g(0)=a and g(n+1)=f(g(n)); a stage-dependent rule is handled on A=N×Z, the first coordinate of g(n) then being n (The recursion theorem, Finite sums and finite products, by recursion).

[L5]

Every nonempty subset of N has a least element, and the order of N is linear (The well-ordering principle, ≤ is a linear order on N).

[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,d) is complete: every Cauchy sequence converges in X; (cn) is Cauchy when for every rational η>0 there is K with d(cn,cm)<η for n,m≥K; and cn→p when for every rational η>0 there is K with d(cn,p)<η for n≥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: xk→x iff d(xk,x)→0 in R, Sequences of reals: bounded, eventually, frequently, tails, subsequences).

[L8]

For every real η>0 there is a natural N≥1 with 1/N<η, and 1/N is a positive rational; reciprocals of positives are positive and reverse the order (For every ε>0 in a complete ordered field there is a natural n≥1 with 1/n<ε, Every complete ordered field is Archimedean, Inverses of positives are positive, and reciprocation reverses order).

Proof

technique · contradiction
1.1

Suppose (X,d) is complete and totally bounded and that some family U of open subsets of X with union X has no finite subfamily with union X; call a subset S⊆X finitely covered when some finite subfamily of U has union containing S, so that X itself is not finitely covered.

L1assume-contra
2.1

X≠∅, since the empty subfamily of U has union ∅ and would finitely cover an empty X; consequently, for each n∈N, the set En of pairs (m,f) with m∈N and f:σ(m)→X such that {f(0),…,f(m)} is a finite 1/(n+1)-net for X is nonempty.

L2L8step 1.1
3.1

Countable choice applied to (En)n∈N fixes, once and for all, a function n↦(mn,fn) with (mn,fn)∈En; this is the single appeal to a choice principle in this proof, and the family (En) was written down at step 2.1 before any of it was made.

L3step 2.1
4.1

If S⊆X is not finitely covered and n∈N, then S∩B(fn(i),1/(n+1)) fails to be finitely covered for at least one i≤mn: otherwise finite choice applied to i↦{finite subfamilies of U covering S∩B(fn(i),1/(n+1))} produces one such subfamily for each i≤mn, and the concatenation of those finitely many finite lists is a finite subfamily of U whose union contains S=⋃i≤mn(S∩B(fn(i),1/(n+1))).

L2L6step 3.1
5.1

Let i(n,S) be the least i≤mn with S∩B(fn(i),1/(n+1)) not finitely covered when such an i exists, and 0 otherwise; recursion on N×P(X) with starting value (0,X) and rule F(n,S):=(n+1, S∩B(fn(i(n,S)),1/(n+1))) then produces g:N→N×P(X) whose first coordinate at n is n; write An for its second coordinate and cn:=fn(i(n,An)).

L4L5step 4.1
6.1

By induction, no An is finitely covered: A0=X is not, by step 1.1, and if An is not then step 4.1 supplies an admissible i, so i(n,An) is one and An+1=An∩B(cn,1/(n+1)) is not finitely covered either. In particular every An is nonempty, since the empty set is finitely covered by the empty subfamily; moreover An+1⊆An and An+1⊆B(cn,1/(n+1)).

step 4.1step 5.1
7.1

The sequence (cn) is Cauchy: for m≥n one has Am+1⊆An+1⊆B(cn,1/(n+1)) and Am+1⊆B(cm,1/(m+1)), and taking z∈Am+1 gives d(cn,cm)≤d(cn,z)+d(z,cm)<1/(n+1)+1/(m+1)≤2/(n+1); so given a rational η>0, a natural N≥1 with 1/N<η/2 makes d(cn,cm)<η for all n,m≥N.

L8L9step 6.1
8.1

By completeness cn→p for some p∈X; since U has union X there is U∈U with p∈U, and openness of U gives a real r>0 with B(p,r)⊆U.

L1L7step 7.1
9.1

Take a natural N≥1 with 1/N<r/2, then K∈N with d(cn,p)<1/N for all n≥K, and let n be whichever of N and K is the greater; then 1/(n+1)<1/N<r/2 and d(cn,p)<r/2, so every y∈An+1⊆B(cn,1/(n+1)) satisfies d(y,p)≤d(y,cn)+d(cn,p)<r, that is An+1⊆B(p,r)⊆U.

L5L7L8L9step 8.1
10.1

So the one-member subfamily {U} of U has union containing An+1, making An+1 finitely covered and contradicting step 6.1; the assumption of step 1.1 therefore fails, every family of open sets with union X has a finite subfamily with union X, and (X,d) is compact.

L1step 6.1step 9.1discharge-contradiction∎

Remarks

Why the nets have to be chosen with their listings. Total boundedness asserts that a finite 1/(n+1)-net exists for each n; it names none, and a bare net is a set, which carries no order in which its points may be scanned. The construction needs both: a net for each n, so that the sets An shrink, and a listing of it, so that "the least admissible index" is meaningful. That is why the chosen object at step 3.1 is the pair (mn,fn) and not the net alone.

Non-dependent, and that is the whole point. The sets En of step 2.1 depend on n and on (X,d), and on nothing that the construction produces. Had the net at stage n+1 been required to depend on An — for instance a net of the set An rather than of X — the selection would have been dependent and countable choice would not have licensed it; the cost would then have been the dependent choice of The axiom of dependent choice: a relation in which every element is related to something admits an N-indexed chain, as in A sequentially compact metric space is totally bounded, proved from the axiom of dependent choice. Keeping the nets fixed in advance and intersecting with balls of X is what holds the price down.

Both hypotheses are needed. A totally bounded space that is not complete 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 ↗), and a complete space that is not totally bounded need not be compact either, R with its usual metric being complete and having no finite 1-net.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

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

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice (ACω)) and the Axiom of Dependent Choice (The axiom of dependent choice: a relation in which every element is related to something admits an 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.

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.

Facts & Assumptions

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

[L1]

In ZF: a compact metric space is countably compact and limit point compact, and each of countable compactness and limit point compactness implies sequential compactness (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).

[L2]

In ZF: a sequentially compact metric space is complete (A sequentially compact metric space is complete, with no choice principle used).

[L3]

Assuming dependent choice: a sequentially compact metric space is totally bounded (A sequentially compact metric space is totally bounded, proved from the axiom of dependent choice).

[L4]

Assuming countable choice: a complete, totally bounded metric space is compact (A complete, totally bounded metric space is compact, proved from countable choice used exactly once).

Proof

technique · direct
1.1

(a) implies (b), and (a) implies (c).

L1
1.2

(b) implies (d), and (c) implies (d).

L1
2.1

(d) implies (e): completeness of a sequentially compact space is a theorem of ZF, and total boundedness follows from dependent choice.

L2L3step 1.2
3.1

(e) implies (a), by countable choice.

L4step 2.1
4.1

The cycle (a) ⇒ (b) ⇒ (d) ⇒ (e) ⇒ (a) is closed by steps 1.1, 1.2, 2.1 and 3.1, so the four conditions (a), (b), (d) and (e) are equivalent to one another.

step 1.1step 1.2step 2.1step 3.1
5.1

Condition (c) joins them: (a) implies (c) by step 1.1 and (c) implies (d) by step 1.2, while (d) implies (a) through the cycle of step 4.1.

step 1.1step 1.2step 4.1
6.1

Hence all five conditions are equivalent; and the implication (a) ⇒ (e), which the cycle obtains only by going round through (b) and (d), also holds directly and choice-freely.

L5step 4.1step 5.1∎

Remarks

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) ⇒ (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.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

Heine-Borel in Rn: with the Euclidean metric a subset of Rn is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line

Statement

Let n∈N with n≥1, let Rn be the set of functions n→R and let d2 be the Euclidean metric on it (Rn as the set of functions n→R, and d1, d2, d∞ are metrics on it). Then:

  1. Closed boxes are compact. For reals ak≤bk (k<n) the box Q={ x∈Rn:ak≤xk≤bk for every k<n } is a compact subset of (Rn,d2) (Open cover, subcover, compact metric space, and compact subset of a metric space).
  2. Heine-Borel. A subset K⊆Rn is a compact subset of (Rn,d2) if and only if K is closed in Rn (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) and bounded (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space).
  3. The real line. A subset K⊆R is a compact subset of (R,dR), the usual metric dR(x,y)=∣x−y∣ (The absolute value makes R a metric space: d(x,y)=∣x−y∣ is a metric, its open balls are the intervals (x−r,x+r), and it is unbounded), if and only if K is closed in R and bounded.

No choice principle is used. The bisection below halves one coordinate at a time and takes the left half whenever the left half still fails to be finitely covered, the right half otherwise: a rule with two outcomes, decided by a property of the box, not a selection. That is the whole reason the theorem is available in ZF, while the general "complete and totally bounded implies compact" (A complete, totally bounded metric space is compact, proved from countable choice used exactly once) is not.

The hypothesis n≥1 is inherited from Rn as the set of functions n→R, and d1, d2, d∞ are metrics on it, which defines Rn and its metrics only there; the last remark below records what happens at n=0.

Facts & Assumptions

Given: A natural number n≥1, the metric space (Rn,d2), and the notions of open, closed, bounded and compact subset in it.

[L1]

Rn is the set of functions n→R, and d2(x,y)=∑k<n(xk−yk)2, d∞(x,y)=max⁡{∣xk−yk∣:k<n} are metrics on it (Rn as the set of functions n→R, and d1, d2, d∞ are metrics on it, Finite sums and finite products, by recursion, Metric space: d(x,y)=0 iff x=y, symmetry, and the triangle inequality; pseudometric and ultrametric).

[L2]

Finite sums of nonnegative terms dominate each term and are monotone, and ∑k<nc=ι(n)c for a constant c, ι(n) being the canonical natural of R (Laws of finite sums and finite products, Finite sums and finite products, by recursion, The canonical natural ι(n)=n⋅1F of a field).

[L3]

For a,b≥0: a≤b exactly when a2≤b2; every a≥0 has a unique nonnegative square root; and c2=∣c∣ for every real c (Squaring is monotone on the nonnegatives, Square roots exist: a unique a≥0 with (a)2=a; the positives are {x2:x≠0}, Absolute value in an ordered field).

[L4]

A subset A is compact exactly when every family (Ui)i∈I of open subsets of the ambient space with A⊆⋃i∈IUi has finitely many members whose union contains A, or A=∅; and the sets open in the subspace A are exactly the traces on A of the open subsets of the ambient space, so, taking complements inside A, the sets closed in A are exactly the traces on A of the closed subsets of the ambient space (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, 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, Isometry, isometric embedding, and the subspace metric on a subset).

[L5]

A compact subset of a metric space is closed and bounded (A compact subset of a metric space is closed and bounded).

[L6]

A closed subset of a compact metric space is compact (A closed subset of a compact metric space is compact).

[L7]

Nested closed bounded intervals Im=[αm,βm] with Im+1⊆Im have nonempty intersection, and the intersection is a single point exactly when the lengths tend to 0 (A nested sequence of nonempty closed bounded intervals has nonempty intersection, and the intersection is a single point exactly when the lengths tend to 0, Intervals of R: the nine order-convex forms, nondegeneracy, and length, Limits and Cauchy sequences of reals).

[L8]

Recursion: for a set A, an element a∈A and f:A→A there is a unique g:N→A with g(0)=a and g(m+1)=f(g(m)); a stage-dependent rule is handled on A=N×Z, the first coordinate of g(m) then being m (The recursion theorem, Finite sums and finite products, by recursion).

[L10]

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

Proof

technique · direct
1.1

For x,y∈Rn and k<n the term (xk−yk)2 is one of the nonnegative terms of ∑j<n(xj−yj)2, so (xk−yk)2≤d2(x,y)2, and taking nonnegative square roots gives ∣xk−yk∣≤d2(x,y); hence d∞(x,y)≤d2(x,y).

L1L2L3
1.2

Conversely each (xj−yj)2≤d∞(x,y)2, so d2(x,y)2≤ι(n) d∞(x,y)2≤(ι(n)d∞(x,y))2, the last step because ι(n)≥1; hence d2(x,y)≤ι(n) d∞(x,y).

L1L2L3
2.1

For claim 1 fix reals ak≤bk (k<n) and the box Q they determine, let (Ui)i∈I be open subsets of Rn with Q⊆⋃i∈IUi, call a set S⊆Rn finitely covered when finitely many of the Ui have union containing S, and suppose for contradiction that Q is not finitely covered.

L4step 1.1step 1.2assume-contra
3.1

For a box P={ x:cj≤xj≤ej (j<n) } with cj≤ej and for k<n, let Pk,0 and Pk,1 be the boxes obtained by replacing the k-th interval [ck,ek] by [ck,(ck+ek)/2] and by [(ck+ek)/2,ek]; then P=Pk,0∪Pk,1 by trichotomy applied to xk against the midpoint, the k-th side length of each is (ek−ck)/2 and the others are unchanged, and if both halves were finitely covered so would P be, the union of two finite subfamilies being finite. Define Hk(P):=Pk,0 if Pk,0 is not finitely covered, and Hk(P):=Pk,1 otherwise; this is a definition by a property, and Hk(P) is not finitely covered whenever P is.

L7step 2.1
4.1

Recursion on N×Z, with Z the set of functions from boxes to boxes, starting value (0,id) and rule (j,h)↦(j+1, Hj∘h) for j<n and (j,h)↦(j+1,h) otherwise, produces Gj for every j; put G:=Gn. By induction on j≤n, Gj(P)⊆P is a box whose k-th side is half that of P for k<j and equal to that of P for k≥j, and Gj(P) is not finitely covered when P is not. So G(P)⊆P halves every side and preserves not being finitely covered.

L8step 3.1
5.1

Recursion applied to the starting value Q and the rule G produces boxes Pm with P0=Q and Pm+1=G(Pm); each Pm fails to be finitely covered, Pm+1⊆Pm, and the k-th side length of Pm is ℓk(1/2)m, where ℓk:=bk−ak≥0.

L8step 4.1
6.1

For each k<n the k-th intervals of the Pm form a nested family of closed bounded intervals whose lengths ℓk(1/2)m tend to 0, so their intersection is a single point pk; the function p:n→R, k↦pk, is a point of Rn lying in every Pm.

L7L9step 5.1
7.1

Since p∈P0=Q⊆⋃i∈IUi, there is i∗∈I with p∈Ui∗, and openness gives a real r>0 with B(p,r)⊆Ui∗.

L11step 6.1
8.1

Put L:=max⁡{ℓk:k<n}≥0 and C:=ι(n)L+1>0; for x∈Pm each ∣xk−pk∣ is at most the k-th side length of Pm, so d∞(x,p)≤L(1/2)m and d2(x,p)≤ι(n)L(1/2)m≤C(1/2)m by step 1.2. Taking a natural N≥1 with 1/N<r/C and then m with (1/2)m<1/N gives Pm⊆B(p,r)⊆Ui∗, so Pm is finitely covered by the single set Ui∗, contradicting step 5.1.

L9L10L12step 1.2step 5.1step 6.1step 7.1discharge-contradiction
9.1

Therefore every such family has finitely many members covering Q, and Q is a compact subset of (Rn,d2): claim 1 is proved.

L4step 2.1step 8.1
10.1

For claim 2, a compact K⊆Rn is closed and bounded.

L5step 9.1
11.1

Conversely let K⊆Rn be closed and bounded; if K=∅ it is compact, and otherwise K⊆B(x0,ρ) for some x0 and real ρ>0, so every x∈K and k<n satisfy ∣xk∣≤∣(x0)k∣+∣xk−(x0)k∣≤∣(x0)k∣+d2(x,x0)<∣(x0)k∣+ρ by step 1.1; with M:=max⁡{∣(x0)k∣:k<n}+ρ the box QM:={ x:−M≤xk≤M (k<n) } contains K.

L10L11step 1.1step 10.1
12.1

K is the trace on QM of a closed subset of Rn, namely of K itself, so K is closed in the metric subspace QM; that subspace is compact by step 9.1, so K is compact, and claim 2 is proved.

L4L6step 9.1step 11.1
13.1

For claim 3, let ψ:R→R1 send t to the function 1→R with value t; it is a bijection and d2(ψ(s),ψ(t))=(s−t)2=∣s−t∣=dR(s,t), so ψ carries each ball onto the corresponding ball, hence open sets onto open sets and open covers onto open covers with matching finite subfamilies, and likewise closed sets onto closed sets and bounded sets onto bounded sets. Applying claim 2 with n=1 to ψ[K] therefore gives claim 3.

L1L3L4L11step 12.1∎

Remarks

Why the bisection halves one coordinate at a time. Halving all n coordinates at once produces 2n sub-boxes, and choosing one of them canonically means enumerating them, which needs a bijection between the functions n→{0,1} and a natural number. Halving a single coordinate produces two sub-boxes, and "the left one if it is still not finitely covered, the right one otherwise" is a definition by cases needing nothing at all. Composing n such halvings, as step 4.1 does, recovers the full halving of every side and keeps the construction canonical, which is what a choice-free proof requires.

Where each hypothesis is used. Closedness enters only at step 12.1, through A closed subset of a compact metric space is compact; boundedness enters only at step 11.1, to fit K inside a box. Dropping either leaves a non-compact set: the whole of Rn is closed and unbounded, and an open ball is bounded and not closed, and neither is compact by claim 2.

The converse direction is what fails in a general metric space. Claim 2 says that in Rn closed and bounded is enough; that is special to Rn, and FALSE: a closed and bounded subset of a metric space is compact records the false general statement together with a witness. What survives in every metric space is only the direction of step 10.1 (A compact subset of a metric space is closed and bounded).

The case n=0. R0 has exactly one element, the empty function, and Rn as the set of functions n→R, and d1, d2, d∞ are metrics on it does not treat it, because d∞ would be a maximum over the empty index set. On a one-element set the only metric is the one taking the value 0, and the resulting space is compact for trivial reasons: it is listed as {x0}, and any family of open sets covering it has a member containing x0 (Open cover, subcover, compact metric space, and compact subset of a metric space). Nothing above is needed for that case and nothing above claims it.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

The image of a compact metric space under a continuous map is compact, and so is the image of any compact subset

Statement

Let (X,dX) and (Y,dY) be metric spaces (Metric space: d(x,y)=0 iff x=y, symmetry, and the triangle inequality; pseudometric and ultrametric) and let f:X→Y be continuous (Continuity of a map between metric spaces, at a point and globally, in the ε-δ form). Then:

  1. If (X,dX) is compact (Open cover, subcover, compact metric space, and compact subset of a metric space), the image f[X]⊆Y is a compact subset of Y.
  2. More generally, if K⊆X is a compact subset of X, then f[K] is a compact subset of Y.

No choice principle is used.

Facts & Assumptions

Given: Metric spaces (X,dX) and (Y,dY) and a continuous f:X→Y; images and preimages are written f[ ⋅ ] and f−1[ ⋅ ] (Injection, surjection, bijection).

[L1]

A subset A of a metric space is compact exactly when for every family (Vi)i∈I of open subsets of the ambient space with A⊆⋃i∈IVi there are n∈N and i0,…,in∈I with A⊆Vi0∪⋯∪Vin, or else A=∅; and a space is a compact subset of itself exactly when it is a compact metric space (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).

[L3]

The restriction of f to a metric subspace (K,dK) of X is continuous as a map (K,dK)→(Y,dY), since the ε-δ condition at a point of K is the condition for f at that point read for the points of K only, and dK is the restriction of dX (Isometry, isometric embedding, and the subspace metric on a subset, Continuity of a map between metric spaces, at a point and globally, in the ε-δ form).

Proof

technique · direct
1.1

Assume (X,dX) compact and let (Vi)i∈I be a family of open subsets of Y with f[X]⊆⋃i∈IVi.

L1
2.1

Each f−1[Vi] is open in X, and X=⋃i∈If−1[Vi], because every x∈X has f(x)∈f[X] and so f(x)∈Vi for some i.

L2step 1.1
3.1

If X=∅ then f[X]=∅ and there is nothing to prove; otherwise compactness of X, read against the indexed family of step 2.1, gives n∈N and i0,…,in∈I with X=f−1[Vi0]∪⋯∪f−1[Vin].

L1step 2.1
4.1

Every y∈f[X] is f(x) for some x∈X, and that x lies in some f−1[Vij], so y∈Vij; hence f[X]⊆Vi0∪⋯∪Vin and f[X] is a compact subset of Y: claim 1.

L1step 3.1
5.1

For claim 2, let K⊆X be a compact subset, so that (K,dK) is a compact metric space; the restriction of f to K is continuous, and its image is f[K], so claim 1 applied to that restriction gives that f[K] is a compact subset of Y.

L1L3step 4.1∎

Remarks

Compactness travels forwards, not backwards. The preimage of a compact set under a continuous map need not be compact: a constant map from an unbounded space has a one-point image. What claim 1 uses is that preimages of open sets are open, which is the content of continuity, together with the fact that a finite subcover upstairs projects to a finite subcover downstairs.

Consequences on this page. Claim 1 with Y=R gives the extreme value theorem (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value), and claim 2 is what makes the inverse of a continuous bijection from a compact space continuous (A continuous bijection from a compact metric space onto a metric space carries open sets to open sets, so its inverse is continuous).

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value

Statement

Let (X,d) be a nonempty 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) and let f:X→R be continuous (Continuity of a map between metric spaces, at a point and globally, in the ε-δ form), R carrying its usual metric dR(s,t)=∣s−t∣ (The absolute value makes R a metric space: d(x,y)=∣x−y∣ is a metric, its open balls are the intervals (x−r,x+r), and it is unbounded). Then the image f[X] is bounded above and below (Lower bound, bounded below, bounded set), and it has a maximum and a minimum (Maximum and minimum of a set): there are points xmax⁡,xmin⁡∈X with

f(xmin⁡)  ≤  f(x)  ≤  f(xmax⁡)for every x∈X,

and then f(xmax⁡)=sup⁡f[X] and f(xmin⁡)=inf⁡f[X] (Complete ordered field (least-upper-bound property), Greatest lower bound (infimum)).

Nonemptiness of X is a hypothesis and not an oversight: for X=∅ the image is empty and has neither a supremum nor a maximum. No choice principle is used.

Facts & Assumptions

Given: A nonempty compact metric space (X,d) and a continuous f:X→R.

[L1]

The image of a compact metric space under a continuous map is a compact subset of the codomain (The image of a compact metric space under a continuous map is compact, and so is the image of any compact subset).

[L4]

A nonempty subset of R that is bounded above has a supremum, and one bounded below has an infimum (Complete ordered field (least-upper-bound property), Greatest lower bound (infimum), Lower bound, bounded below, bounded set).

[L5]

For S nonempty and bounded above with supremum u: for every real ε>0 there is s∈S with u−ε<s≤u; dually for the infimum (Epsilon characterisation of the supremum, Epsilon characterisation of the infimum).

[L7]

A subset of a metric space is compact exactly when the corresponding metric subspace is compact, the subspace metric being the restriction (Open cover, subcover, compact metric space, and compact subset of a metric space, Isometry, isometric embedding, and the subspace metric on a subset).

Proof

technique · direct
1.1

f[X] is a compact subset of (R,dR), and it is nonempty because X is.

L1L7
2.1

So f[X] is closed in R and bounded as a subset of the metric space (R,dR): there are x0∈R and a real ρ>0 with f[X]⊆B(x0,ρ)=(x0−ρ, x0+ρ).

L2L3step 1.1
3.1

Hence x0+ρ is an upper bound and x0−ρ a lower bound of f[X], so f[X] is bounded above and below, and being nonempty it has a supremum u and an infimum ℓ.

L4step 2.1
4.1

For every real ε>0 there is t∈f[X] with u−ε<t≤u, so ∣t−u∣<ε and t∈B(u,ε)∩f[X]; therefore every ball around u meets f[X] and u lies in the closure of f[X].

L3L5L6step 3.1
5.1

Since f[X] is closed, u∈f[X]; so u is a member of f[X] bounding it above, that is u=max⁡f[X], and u=f(xmax⁡) for some xmax⁡∈X.

L6step 2.1step 4.1
6.1

The same argument with ℓ in place of u, using the infimum form of step 4.1, gives ℓ∈f[X], so ℓ=min⁡f[X] and ℓ=f(xmin⁡) for some xmin⁡∈X.

L5L6step 3.1step 5.1
7.1

For every x∈X the value f(x) lies in f[X], hence f(xmin⁡)=ℓ≤f(x)≤u=f(xmax⁡), which is the assertion, with f(xmax⁡)=sup⁡f[X] and f(xmin⁡)=inf⁡f[X].

L4step 3.1step 5.1step 6.1∎

Remarks

Compactness is what is used, not boundedness of the domain. A bounded non-compact domain is not enough: on the interval (0,1) the identity map is continuous and bounded with no greatest value, and x↦1/x is continuous and unbounded (On (0,1) the identity is bounded with no greatest value and x↦1/x is continuous and unbounded, so the extreme value theorem needs compactness and not merely boundedness of the domain ↗).

Why the supremum has to be shown to be attained at all. sup⁡f[X] exists as soon as f[X] is nonempty and bounded above, which needs only boundedness; what compactness adds is that f[X] is closed, and a closed set contains the supremum it approaches. Steps 4.1 and 5.1 are exactly that passage, and they are where the theorem is more than the least-upper-bound property.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

Every open cover of a compact metric space has a Lebesgue number: a δ>0 such that every nonempty subset of diameter less than δ lies inside a single member of the cover

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) and let U be an open cover of X. Then there is a real δ>0, a Lebesgue number for U, such that every nonempty A⊆X with diam⁡(A)<δ (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space) satisfies A⊆U for some U∈U.

Diameters of nonempty subsets of X are defined because a compact space is bounded (A compact subset of a metric space is closed and bounded) and a subset of a bounded set is bounded. No choice principle is used.

Facts & Assumptions

Given: A compact metric space (X,d) and an open cover U of it.

[L2]

A compact metric space is bounded, and diam⁡(A)=sup⁡{d(u,v):u,v∈A} is defined for every nonempty bounded A (A compact subset of a metric space is closed and bounded, Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space).

[L3]

For nonempty S⊆X, d(x,S)=inf⁡{d(x,y):y∈S}; an infimum is a lower bound of its set and is at least every lower bound (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space, Greatest lower bound (infimum)).

[L5]

A continuous real-valued function on a nonempty compact metric space attains a least value (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).

[L6]

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

Proof

technique · direct
1.1

If X=∅ then δ:=1 serves, there being no nonempty subset of X to test; assume from now on X≠∅.

L2
2.1

Compactness gives m∈N and U0,…,Um∈U with X=U0∪⋯∪Um.

L1step 1.1
3.1

If Ui=X for some i≤m, then δ:=1 serves again, every nonempty A⊆X being contained in that Ui; assume from now on that X∖Ui≠∅ for every i≤m.

step 2.1
4.1

For α0,…,αm and β0,…,βm real one has αi≤βi+∣αi−βi∣≤max⁡jβj+max⁡j∣αj−βj∣ for every i, so max⁡iαi≤max⁡jβj+max⁡j∣αj−βj∣, and by symmetry ∣max⁡iαi−max⁡iβi∣≤max⁡i∣αi−βi∣.

L6step 3.1
5.1

Define g:X→R by g(x):=max⁡{ d(x,X∖Ui):i≤m }, a maximum of a nonempty finite set of reals; each x↦d(x,X∖Ui) changes by at most d(x,y) between x and y, so by step 4.1 ∣g(x)−g(y)∣≤d(x,y), and g is Lipschitz with constant 1, hence continuous.

L4L6step 4.1
6.1

g(x)>0 for every x∈X: such an x lies in some Ui by step 2.1, openness gives a real r>0 with B(x,r)⊆Ui, so every y∈X∖Ui has d(x,y)≥r, making r a lower bound of {d(x,y):y∈X∖Ui} and hence g(x)≥d(x,X∖Ui)≥r>0.

L3L7step 2.1step 5.1
7.1

By the extreme value theorem applied to the nonempty compact X and the continuous g, there is x∗∈X with g(x∗)≤g(x) for every x; put δ:=g(x∗), a real with δ>0 by step 6.1.

L5step 5.1step 6.1
8.1

Let A⊆X be nonempty with diam⁡(A)<δ and fix a∈A; then g(a)≥δ, so some i≤m has d(a,X∖Ui)≥δ, the maximum defining g(a) being one of its members, and the least such i may be taken.

L2L6step 7.1
9.1

Every y∈A satisfies d(a,y)≤diam⁡(A)<δ≤d(a,X∖Ui), so y∉X∖Ui, since a point of that set would make d(a,X∖Ui)≤d(a,y); hence A⊆Ui with Ui∈U, and δ is a Lebesgue number for U.

L2L3step 8.1∎

Remarks

What the lemma buys. An open cover gives, around each point, some member containing a ball about that point, with a radius depending on the point. A Lebesgue number is one radius that works everywhere at once, and that uniformity is exactly what turns pointwise continuity into uniform continuity in Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous.

Compactness is not removable. The cover of the interval (0,1) by the intervals (1/(k+2),1), k∈N, has no Lebesgue number (The cover of (0,1) by the intervals (1/(k+2),1) has no Lebesgue number, so the Lebesgue number lemma needs compactness ↗), and (0,1) is not compact.

The two degenerate cases in steps 1.1 and 3.1 are genuine. If X is empty the conclusion is vacuous, and if some member of the finite subcover is the whole space the function g of step 5.1 would call for the distance to the empty set, which this library leaves undefined (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space). Handling both separately costs two lines and avoids writing something undefined.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous

Statement

Facts & Assumptions

Given: A compact metric space (X,dX), a metric space (Y,dY) and a continuous f:X→Y.

[L1]

f is continuous at a: for every real ε>0 there is a real δ>0 with f[BX(a,δ)]⊆BY(f(a),ε) (Continuity of a map between metric spaces, at a point and globally, in the ε-δ form, Open ball, closed ball and sphere in a metric space).

[L2]

f is uniformly continuous when for every real ε>0 there is a real δ>0 such that dX(x,x′)<δ implies dY(f(x),f(x′))<ε, for all x,x′∈X (Uniform continuity of a map of metric spaces: one δ serving every point).

[L3]

Every open cover of a compact metric space has a Lebesgue number: a real δ>0 such that every nonempty subset of diameter less than δ lies in a single member of the cover (Every open cover of a compact metric space has a Lebesgue number: a δ>0 such that every nonempty subset of diameter less than δ lies inside a single member of the cover, Open cover, subcover, compact metric space, and compact subset of a metric space).

[L5]

For nonempty bounded A, diam⁡(A)=sup⁡{dX(u,v):u,v∈A}; in particular diam⁡({x,x′})=dX(x,x′), the set of distances being {0,dX(x,x′)} and a metric being nonnegative (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space, Nonnegativity of a metric is a consequence of the other axioms, not an axiom).

Proof

technique · direct
1.1

If X=∅ the condition of uniform continuity holds vacuously, so assume X≠∅, and let ε>0 be real.

L2
2.1

Put U:={ U⊆X:U is open in X and f[U]⊆BY(z,ε/2) for some z∈Y }, a family cut out by a property and not by a selection.

L1step 1.1
3.1

U is an open cover of X: given x∈X, continuity at x supplies a real δx>0 with f[BX(x,δx)]⊆BY(f(x),ε/2), and BX(x,δx) is open and contains x, so it belongs to U.

L1L4step 2.1
4.1

By the Lebesgue number lemma there is a real δ>0 such that every nonempty subset of X of diameter less than δ is contained in a single member of U.

L3step 3.1
5.1

Let x,x′∈X with dX(x,x′)<δ; the set {x,x′} is nonempty with diameter dX(x,x′)<δ, so {x,x′}⊆U for some U∈U, and there is z∈Y with f[U]⊆BY(z,ε/2).

L5step 2.1step 4.1
6.1

Then dY(f(x),z)<ε/2 and dY(z,f(x′))<ε/2, so dY(f(x),f(x′))≤dY(f(x),z)+dY(z,f(x′))<ε; as ε>0 was arbitrary, f is uniformly continuous.

L2L6step 5.1∎

Remarks

The centre z is not chosen, and that is why the proof is choice free. The family U is defined by the existence of a suitable z, and the argument instantiates that existential once, at step 5.1, for the single member U that the Lebesgue number produced. No function assigning a centre to every member of U is ever needed.

Compactness is not removable. The map x↦1/x is continuous on the interval (0,1) and is not uniformly continuous there (x↦1/x is continuous on (0,1) and not uniformly continuous, so Heine-Cantor needs compactness of the domain ↗); (0,1) is not compact.

The codomain is arbitrary. Nothing is assumed about (Y,dY) — not completeness, not boundedness, not compactness. All the work is done on the domain side, which is where the finite subcover lives.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

A continuous bijection from a compact metric space onto a metric space carries open sets to open sets, so its inverse is continuous

Statement

Let (X,dX) be a compact metric space (Open cover, subcover, compact metric space, and compact subset of a metric space), let (Y,dY) be a metric space (Metric space: d(x,y)=0 iff x=y, symmetry, and the triangle inequality; pseudometric and ultrametric) and let f:X→Y be a continuous bijection (Continuity of a map between metric spaces, at a point and globally, in the ε-δ form, Injection, surjection, bijection). Then:

  1. f[U] is open in Y for every U open in X (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);
  2. the inverse function f−1:Y→X is continuous.

The words used are deliberately those of open sets and of the inverse map: a single name for a continuous bijection with continuous inverse is not available at this point in the reading order. No choice principle is used.

Facts & Assumptions

Given: A compact metric space (X,dX), a metric space (Y,dY) and a continuous bijection f:X→Y.

[L2]

The image of a compact subset under a continuous map is a compact subset of the codomain (The image of a compact metric space under a continuous map is compact, and so is the image of any compact subset).

[L3]

A compact subset of a metric space is closed (A compact subset of a metric space is closed and bounded).

[L6]

For a bijection f:X→Y and U⊆X: f[X∖U]=Y∖f[U], and for the inverse function g=f−1 one has g−1[U]=f[U] (Injection, surjection, bijection).

Proof

technique · direct
1.1

Let U⊆X be open; then X∖U is closed in X.

L4
2.1

Being a closed subset of the compact space X, the set X∖U is a compact subset of X.

L1step 1.1
3.1

Hence f[X∖U] is a compact subset of Y, and therefore closed in Y.

L2L3step 2.1
4.1

Since f is a bijection, f[X∖U]=Y∖f[U], so f[U]=Y∖f[X∖U] is open in Y: claim 1.

L4L6step 3.1
5.1

Write g:=f−1:Y→X, a function because f is a bijection; for every open U⊆X the preimage g−1[U] equals f[U], which is open by claim 1, so g is continuous: claim 2.

L5L6step 4.1∎

Remarks

Compactness of the domain is essential. Without it a continuous bijection can have a discontinuous inverse, and no part of the argument survives, compactness being consumed at steps 2.1 and 3.1 alike. What the theorem says is that on a compact domain no such failure occurs, and the reason is entirely the open map property established at step 4.1.

Hausdorffness of the codomain is used silently and is automatic here. What step 3.1 needs is that a compact subset of Y be closed, which is A compact subset of a metric space is closed and bounded and rests on the separation of distinct points by disjoint balls. Every metric space has that property, so no hypothesis on (Y,dY) beyond being a metric space is required.

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

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

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice (ACω)). 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⊆X (Finite, countably infinite, countable, uncountable) that is dense in X, that is 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∈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 ACω at step 4.1 carries the same hypothesis ACω 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 ACω 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 ε>0 there is a finite F⊆X with X=⋃y∈FB(y,ε) (A compact metric space is complete and totally bounded, and neither implication uses any choice principle, Finite ε-net and totally bounded metric space, Open ball, closed ball and sphere in a metric space).

[L2]

Countable choice: for a family (En)n∈N of nonempty sets there is a function n↦en with en∈En (The Axiom of Countable Choice (ACω)).

[L3]

Finite sets are at most countable, and, assuming countable choice, a union ⋃n∈NAn of at most countable sets is at most countable (Finite, countably infinite, countable, uncountable, Countable unions of at most countable sets, assuming ACω, A nonempty set is at most countable iff it is a surjective image of N).

[L5]

Proof

technique · direct
1.1

For each n∈N let En be the set of finite 1/(n+1)-nets for (X,d); each En is nonempty because (X,d) is compact and hence totally bounded.

L1
2.1

Countable choice applied to (En)n∈N fixes a function n↦Fn with Fn∈En for every n, that is a finite 1/(n+1)-net Fn⊆X for each n; this is the only appeal to a choice principle here.

L2step 1.1
3.1

Put D:=⋃n∈NFn⊆X.

step 2.1
4.1

Each Fn is finite and therefore at most countable, so D is at most countable by the countable union theorem, whose hypothesis is the same ACω already assumed.

L3step 3.1
4.2

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

L1L4L5step 2.1step 3.1
5.1

So every ball around every point of X meets D, that is 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 ACω, 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=∅ then every Fn is empty, D is empty, and D‾=∅=X; the empty set is finite and hence at most countable.

RemarkRemark: AI-generatedProof: Not applicablejudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

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

What this page spends, implication by implication

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 states five conditions and asserts that they are equivalent, under two choice hypotheses. Stated that way the theorem overcharges almost every arrow it contains, so this remark records the arrows one at a time. Every entry is a statement about the proof given in this library, and about nothing else.

Theorems of ZF, using no choice principle at all.

Using the Axiom of Countable Choice (The Axiom of Countable Choice (ACω)), spent once and named at the step that spends it.

Using the Axiom of Dependent Choice (The axiom of dependent choice: a relation in which every element is related to something admits an N-indexed chain).

  • A sequentially compact metric space is totally bounded (A sequentially compact metric space is totally bounded, proved from the axiom of dependent choice). This is the only implication on the page with that cost. The construction adds one point at a time, each at distance at least ε from all the points already produced, so the set the next point is drawn from is not known until the earlier ones are fixed. Countable choice returns one ε-separated tuple for each length with no coherence between them, and no diagonal argument assembles those into a single separated sequence.

What is claimed and what is not

Claimed: each proof in this library can be carried out in ZF together with the principle named above, and in no case is more used than is named.

Not claimed: that any of these principles is necessary. Showing that an implication cannot be proved in ZF alone is an independence result, obtained by forcing or by permutation models, and this library contains neither and proves none. Every cost above is an upper bound. The systematic study of which forms of compactness need which fragment of choice is a subject in its own right, and Herrlich's Axiom of Choice is the standard reference; it is cited here as literature and is not used.

Not claimed either: that a cost recorded for one proof is a cost of the statement. Two proofs of the same implication may spend differently, and the completeness half of A compact metric space is complete and totally bounded, and neither implication uses any choice principle is exactly a case where the textbook route and the route taken here differ in what they use.

How to read the equivalence theorem

A cycle of implications transmits the weakest hypothesis around the whole cycle: once 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 has closed its cycle, every one of its five conditions implies every other under both hypotheses. The individual arrows do not inherit that. A reader working in ZF alone still has, without any choice at all, that a compact metric space satisfies all four of the other conditions, and that a sequentially compact one is complete. What fails in ZF, as far as this library's proofs go, is the journey back from the weaker conditions to compactness.

Where these principles sit relative to one another — that the Axiom of Choice implies dependent choice, which implies countable choice, and that the reverse implications are relative-consistency results quoted rather than proved — is recorded in The axiom of dependent choice: a relation in which every element is related to something admits an N-indexed chain and in the definitions it points to.

5 · Examples, counterexamples and false statements

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)verified 2026-08-04 (gpt-5.6-sol-codex-subscription)Open item page →

FALSE: a closed and bounded subset of a metric space is compact

Statement

False claim: in every metric space (X,d) (Metric space: d(x,y)=0 iff x=y, symmetry, and the triangle inequality; pseudometric and ultrametric), a subset that is closed in X (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) and bounded (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space) is a compact subset of X (Open cover, subcover, compact metric space, and compact subset of a metric space).

Where the claim comes from, and what is actually true. One half of the Heine-Borel property does hold in every metric space: a compact subset is closed and bounded (A compact subset of a metric space is closed and bounded). The converse holds in Rn with the Euclidean metric (Heine-Borel in Rn: with the Euclidean metric a subset of Rn is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line), and the claim above is that reading of Heine-Borel transplanted to an arbitrary metric space, where it fails. What survives in general is that a compact space is complete and totally bounded (A compact metric space is complete and totally bounded, and neither implication uses any choice principle), and it is total boundedness, not boundedness, that the witness below lacks.

The refutation builds its own witness: the set N carrying the metric that assigns distance 1 to distinct points.

Facts & Assumptions

Given: The set N of natural numbers (The natural numbers N (von Neumann)) and the function d:N×N→R with d(m,n)=0 for m=n and d(m,n)=1 for m≠n.

[A1]

The false claim: in every metric space a closed bounded subset is compact.

[L1]

A metric on a set is a real-valued function satisfying (M1) d(x,y)=0 exactly when x=y, (M2) d(x,y)=d(y,x) and (M3) d(x,z)≤d(x,y)+d(y,z) (Metric space: d(x,y)=0 iff x=y, symmetry, and the triangle inequality; pseudometric and ultrametric).

[L2]

B(x,r)={y:d(x,y)<r}; a set is open when each of its points has a ball around it inside it; a set is closed when its complement is open; and a subset is bounded when it is empty or lies in a ball (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, Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space).

[L3]

A subset A of a metric space is compact exactly when the metric subspace (A,dA) is a compact metric space; and a compact metric space has, for every family of open subsets with union the space, a finite subfamily with union the space (Open cover, subcover, compact metric space, and compact subset of a metric space).

[L4]

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

[L5]

For every real M there is a natural N≥1 with M<ι(N), where ι is the canonical natural of R (Every complete ordered field is Archimedean, The canonical natural ι(n)=n⋅1F of a field).

Refutation

technique · direct
1.1

d is a metric on N: (M1) holds because d(m,n)=0 was defined to mean m=n; (M2) because the defining condition is symmetric in m and n; and (M3) because the left side is 0 or 1, and when it is 1 one has x≠z, so y differs from at least one of x and z and the right side is at least 1.

L1
2.1

In (N,d) one has B(n,1)={n}, since d(n,m)<1 forces d(n,m)=0 and hence m=n; consequently every subset of N is open, each of its points n having B(n,1) inside it, and every subset is closed as well.

L2step 1.1
3.1

N is a closed subset of the metric space (N,d), and it is bounded, since d(0,n)≤1<2 for every n gives N=B(0,2).

L2step 2.1
3.2

The family (B(n,1))n∈N consists of open subsets of N and has union N, because n∈B(n,1) for every n.

L2step 2.1
4.1

No finite subfamily has union N: such a subfamily is B(n0,1),…,B(nk,1) for some k∈N and naturals n0,…,nk, with union {n0,…,nk} by step 2.1; the reals ι(n0),…,ι(nk) have a maximum M, and a natural N≥1 with M<ι(N) then satisfies ι(N)≠ι(ni) and hence N≠ni for every i≤k, so N lies in N and in no member of the subfamily.

L4L5step 2.1step 3.2
5.1

Hence (N,d) is not a compact metric space, so N is a closed and bounded subset of the metric space (N,d) that is not compact, and the claim [A1] is false.

A1L3step 3.1step 3.2step 4.1∎

Remarks

What the witness fails is total boundedness, not boundedness. The space (N,d) has diameter 1, so it is as bounded as a nonempty space can be; but a finite 1/2-net would have to contain every point, and N is not finite (N with the discrete metric is bounded and is not totally bounded ↗, FALSE: a bounded metric space is totally bounded). Since a compact space is totally bounded (A compact metric space is complete and totally bounded, and neither implication uses any choice principle), that alone already settles non-compactness; the explicit cover of step 3.2 is given because it makes the failure visible without any theory.

The witness is complete, so completeness is not the missing ingredient either. In (N,d) a Cauchy sequence is eventually constant, hence convergent, so this is a complete, bounded, closed space that is not compact. The pair that is equivalent to compactness, once the Axiom of Countable Choice and the Axiom of Dependent Choice are assumed, is completeness together with total boundedness (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).

A second, analytically natural witness is the closed unit ball of the bounded real-valued functions on N under the supremum metric, where the indicator functions of the singletons are pairwise at distance 1 (In the bounded real-valued functions on N with the supremum metric, the closed unit ball is closed and bounded and is not compact: the indicator functions of the singletons are pairwise at distance 1 ↗).

False statementConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)verified 2026-08-04 (gpt-5.6-sol-codex-subscription)Open item page →

FALSE: a totally bounded metric space is compact

Statement

False claim: every totally bounded metric space (Finite ε-net and totally bounded metric space) is compact (Open cover, subcover, compact metric space, and compact subset of a metric space).

Where the claim comes from, and what is actually true. A compact metric space is totally bounded, and it is also complete (A compact metric space is complete and totally bounded, and neither implication uses any choice principle); the converse needs both of those conditions, not one of them, and, as stated in this library, it also assumes the Axiom of Countable Choice (A complete, totally bounded metric space is compact, proved from countable choice used exactly once, The Axiom of Countable Choice (ACω)). The claim above drops completeness, and dropping it is fatal.

The refutation takes the open interval (0,1) (Intervals of R: the nine order-convex forms, nondegeneracy, and length) as a metric subspace of R with its usual metric ∣x−y∣ (The absolute value makes R a metric space: d(x,y)=∣x−y∣ is a metric, its open balls are the intervals (x−r,x+r), and it is unbounded, Isometry, isometric embedding, and the subspace metric on a subset).

Facts & Assumptions

Given: The interval (0,1)={x∈R:0<x<1} as a metric subspace of (R,dR), dR(x,y)=∣x−y∣.

[A1]

The false claim: every totally bounded metric space is compact.

[L1]

A space is totally bounded when for every real ε>0 it has a finite ε-net, a finite subset F with the balls B(y,ε), y∈F, covering the space (Finite ε-net and totally bounded metric space, Open ball, closed ball and sphere in a metric space).

[L4]

Every nonempty subset of N has a least element (The well-ordering principle).

[L5]

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

[L6]

For every real η>0 there is a natural m≥1 with 1/m<η; reciprocals of positives are positive and reverse the order (For every ε>0 in a complete ordered field there is a natural n≥1 with 1/n<ε, Every complete ordered field is Archimedean, Inverses of positives are positive, and reciprocation reverses order).

Refutation

technique · direct
1.1

Let ε>0 be real and take a natural m≥1 with 1/m<ε; the points j/(m+1) for 1≤j≤m lie in (0,1), since 0<j/(m+1)<1, and they form a finite subset F of (0,1).

L3L6
2.1

F is a finite ε-net for (0,1): given x∈(0,1), the set of naturals j≥1 with x<(j+1)/(m+1) is nonempty, containing m because x<1=(m+1)/(m+1), so it has a least element j, and j≤m.

L4L6step 1.1
3.1

For that j one has x<(j+1)/(m+1) and also (j−1)/(m+1)<x: for j=1 because x>0, and for j≥2 because minimality gives x≥j/(m+1)>(j−1)/(m+1). Hence ∣x−j/(m+1)∣<1/(m+1)<1/m<ε, so x lies in the subspace ball of radius ε about j/(m+1).

L3L6step 2.1
4.1

As ε>0 was arbitrary, (0,1) with the restricted metric is totally bounded.

L1step 1.1step 3.1
5.1

For each k∈N put Uk:=(1/(k+2), 1), an open subset of R contained in (0,1); the family (Uk)k∈N has union (0,1), because any x∈(0,1) admits a natural m≥1 with 1/m<x and then 1/(m+2)<1/m<x<1.

L3L6step 4.1
6.1

No finitely many of the Uk have union containing (0,1): given Uk0,…,Ukp, put t:=min⁡{1/(ki+2):i≤p}, a positive real; each Uki is contained in (t,1) because 1/(ki+2)≥t, so the union of the finite subfamily is contained in (t,1), while the real x:=min⁡{t,1/2}/2 satisfies 0<x<1 and x≤t, so x∈(0,1) and x lies in no Uki.

L5L6step 5.1
7.1

Hence (0,1) is not a compact subset of R, that is the metric subspace (0,1) is a totally bounded metric space that is not compact, and the claim [A1] is false.

A1L2step 4.1step 5.1step 6.1∎

Remarks

What the witness lacks is completeness. A compact metric space is complete (A compact metric space is complete and totally bounded, and neither implication uses any choice principle, Complete metric space: every Cauchy sequence converges in the space), and (0,1) is not: the terms 1/(k+2) form a Cauchy sequence in (0,1) whose only candidate limit in R is 0, which is not a point of the space. Adding completeness to total boundedness does restore compactness (A complete, totally bounded metric space is compact, proved from countable choice used exactly once), at the cost of the Axiom of Countable Choice.

The same interval also witnesses that boundedness is far from compactness, and it is the standard example behind the failure of the extreme value theorem and of Heine-Cantor off a compact domain (On (0,1) the identity is bounded with no greatest value and x↦1/x is continuous and unbounded, so the extreme value theorem needs compactness and not merely boundedness of the domain ↗, x↦1/x is continuous on (0,1) and not uniformly continuous, so Heine-Cantor needs compactness of the domain ↗).

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27Open item page →

FALSE: a bounded metric space is totally bounded

Statement

False claim: every bounded metric space (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space, Metric space: d(x,y)=0 iff x=y, symmetry, and the triangle inequality; pseudometric and ultrametric) is totally bounded (Finite ε-net and totally bounded metric space).

Where the claim comes from, and what is actually true. The implication holds in the other direction: a totally bounded metric space is bounded, which is claim 1 of 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. The claim above is its converse, and the converse fails. Boundedness asks for one ball containing the space; total boundedness asks for finitely many balls of every prescribed radius, and no amount of shrinking the diameter forces the second condition.

The refutation builds its witness: the set N carrying the metric that assigns distance 1 to distinct points.

Facts & Assumptions

Given: The set N (The natural numbers N (von Neumann)) and the function d with d(m,n)=0 for m=n and d(m,n)=1 for m≠n.

[A1]

The false claim: every bounded metric space is totally bounded.

[L1]

A metric satisfies (M1) d(x,y)=0 exactly when x=y, (M2) symmetry and (M3) the triangle inequality (Metric space: d(x,y)=0 iff x=y, symmetry, and the triangle inequality; pseudometric and ultrametric).

[L2]

B(x,r)={y:d(x,y)<r}, and a space is bounded when it is empty or is contained in a ball (Open ball, closed ball and sphere in a metric space, Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space).

[L3]

A finite ε-net is a finite F⊆X with X=⋃y∈FB(y,ε), and a space is totally bounded when it has one for every real ε>0; a nonempty finite set can be listed as {n0,…,nk} (Finite ε-net and totally bounded metric space, Open cover, subcover, compact metric space, and compact subset of a metric space, Finite, countably infinite, countable, uncountable).

[L4]

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

[L5]

For every real M there is a natural N≥1 with M<ι(N), where ι is the canonical natural of R (Every complete ordered field is Archimedean, The canonical natural ι(n)=n⋅1F of a field).

Refutation

technique · direct
1.1

d is a metric on N: (M1) holds by the definition of d; (M2) because the defining condition is symmetric; and (M3) because the left side is 0 or 1, and if it is 1 then x≠z, so y differs from at least one of x and z and the right side is at least 1.

L1
2.1

(N,d) is bounded: d(0,n)≤1<2 for every n, so N=B(0,2).

L2step 1.1
2.2

In (N,d) one has B(y,1/2)={y}, since d(y,n)<1/2 forces d(y,n)=0 and hence n=y.

L2step 1.1
3.1

Suppose F were a finite 1/2-net for (N,d); then N=⋃y∈FB(y,1/2)=⋃y∈F{y}=F, so N would be finite, and being nonempty it could be listed as N={n0,…,nk}.

L3step 2.2
4.1

The reals ι(n0),…,ι(nk) then have a maximum M, and a natural N≥1 with M<ι(N) satisfies ι(N)≠ι(ni) and hence N≠ni for every i≤k, so N is a natural number outside {n0,…,nk}=N, which is impossible.

L4L5step 3.1
5.1

So no finite 1/2-net exists, (N,d) is a bounded metric space that is not totally bounded, and the claim [A1] is false.

A1L3step 2.1step 3.1step 4.1∎

Remarks

Diameter is not a measure of how spread out a space is at small scales. The witness has diameter 1, and yet every ball of radius 1/2 contains a single point, so no finite family of them can cover an infinite space. Total boundedness is exactly the condition that rules this out, and it is what makes the pair "complete and totally bounded" equivalent to compactness (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).

The same witness refutes more. Because it is complete and closed in itself, it also shows that a closed bounded subset of a metric space need not be compact (FALSE: a closed and bounded subset of a metric space is compact). The counterexample page records it once, in N with the discrete metric is bounded and is not totally bounded ↗.

In Rn the claim is true, since a bounded subset lies in a box and a box is compact, hence totally bounded (Heine-Borel in Rn: with the Euclidean metric a subset of Rn is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line, A compact metric space is complete and totally bounded, and neither implication uses any choice principle). What fails is the general metric statement, and the witness is a space whose points are pairwise equidistant, which is exactly what the geometry of Rn forbids for infinitely many points at once.

Sources