Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27
How statement and proof provenance work

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

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

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

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.

Depends on

Used by

…and 153 more results.

Dependency tree · two levels

79 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources