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 : with the Euclidean metric a subset of 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 with , let be the set of functions and let be the Euclidean metric on it ( as the set of functions , and , , are metrics on it). Then:
- Closed boxes are compact. For reals the box is a compact subset of (Open cover, subcover, compact metric space, and compact subset of a metric space).
- Heine-Borel. A subset is a compact subset of if and only if is closed 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 bounded (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space).
- The real line. A subset is a compact subset of , the usual metric (The absolute value makes a metric space: is a metric, its open balls are the intervals , and it is unbounded), if and only if is closed in 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 is inherited from as the set of functions , and , , are metrics on it, which defines and its metrics only there; the last remark below records what happens at .
Statement references
Facts & Assumptions
Given: A natural number , the metric space , and the notions of open, closed, bounded and compact subset in it.
is the set of functions , and , are metrics on it ( as the set of functions , and , , are metrics on it, Finite sums and finite products, by recursion, Metric space: iff , symmetry, and the triangle inequality; pseudometric and ultrametric).
Finite sums of nonnegative terms dominate each term and are monotone, and for a constant , being the canonical natural of (Laws of finite sums and finite products, Finite sums and finite products, by recursion, The canonical natural of a field).
For : exactly when ; every has a unique nonnegative square root; and for every real (Squaring is monotone on the nonnegatives, Square roots exist: a unique with ; the positives are , Absolute value in an ordered field).
A subset is compact exactly when every family of open subsets of the ambient space with has finitely many members whose union contains , or ; and the sets open in the subspace are exactly the traces on of the open subsets of the ambient space, so, taking complements inside , the sets closed in are exactly the traces on 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).
A compact subset of a metric space is closed and bounded (A compact subset of a metric space is closed and bounded).
A closed subset of a compact metric space is compact (A closed subset of a compact metric space is compact).
Nested closed bounded intervals with have nonempty intersection, and the intersection is a single point exactly when the lengths tend to (A nested sequence of nonempty closed bounded intervals has nonempty intersection, and the intersection is a single point exactly when the lengths tend to , Intervals of : the nine order-convex forms, nondegeneracy, and length, Limits and Cauchy sequences of reals).
Recursion: for a set , an element and there is a unique with and ; a stage-dependent rule is handled on , the first coordinate of then being (The recursion theorem, Finite sums and finite products, by recursion).
, integer powers being those of Integer powers (For the sequence is null, and for the sequence diverges to , Limits and Cauchy sequences of reals).
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).
is open exactly when every point of has a ball inside ; a subset is bounded when it is empty or lies in some ball with (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, Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space).
For every real there is a natural with (For every in a complete ordered field there is a natural with , Every complete ordered field is Archimedean).
Proof
For and the term is one of the nonnegative terms of , so , and taking nonnegative square roots gives ; hence .
Conversely each , so , the last step because ; hence .
For claim 1 fix reals and the box they determine, let be open subsets of with , call a set finitely covered when finitely many of the have union containing , and suppose for contradiction that is not finitely covered.
For a box with and for , let and be the boxes obtained by replacing the -th interval by and by ; then by trichotomy applied to against the midpoint, the -th side length of each is and the others are unchanged, and if both halves were finitely covered so would be, the union of two finite subfamilies being finite. Define if is not finitely covered, and otherwise; this is a definition by a property, and is not finitely covered whenever is.
Recursion on , with the set of functions from boxes to boxes, starting value and rule for and otherwise, produces for every ; put . By induction on , is a box whose -th side is half that of for and equal to that of for , and is not finitely covered when is not. So halves every side and preserves not being finitely covered.
Recursion applied to the starting value and the rule produces boxes with and ; each fails to be finitely covered, , and the -th side length of is , where .
For each the -th intervals of the form a nested family of closed bounded intervals whose lengths tend to , so their intersection is a single point ; the function , , is a point of lying in every .
Since , there is with , and openness gives a real with .
Put and ; for each is at most the -th side length of , so and by step 1.2. Taking a natural with and then with gives , so is finitely covered by the single set , contradicting step 5.1.
Therefore every such family has finitely many members covering , and is a compact subset of : claim 1 is proved.
For claim 2, a compact is closed and bounded.
Conversely let be closed and bounded; if it is compact, and otherwise for some and real , so every and satisfy by step 1.1; with the box contains .
is the trace on of a closed subset of , namely of itself, so is closed in the metric subspace ; that subspace is compact by step 9.1, so is compact, and claim 2 is proved.
For claim 3, let send to the function with value ; it is a bijection and , 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 to therefore gives claim 3.
Remarks
Why the bisection halves one coordinate at a time. Halving all coordinates at once produces sub-boxes, and choosing one of them canonically means enumerating them, which needs a bijection between the functions 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 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 inside a box. Dropping either leaves a non-compact set: the whole of 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 closed and bounded is enough; that is special to , 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 . has exactly one element, the empty function, and as the set of functions , and , , are metrics on it does not treat it, because would be a maximum over the empty index set. On a one-element set the only metric is the one taking the value , and the resulting space is compact for trivial reasons: it is listed as , and any family of open sets covering it has a member containing (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
Open cover, subcover, compact metric space, and compact subset of a 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
A compact subset of a metric space is closed and bounded
A closed subset of a compact metric space is compact
as the set of functions , and , , are metrics on it
The absolute value makes a metric space: is a metric, its open balls are the intervals , and it is unbounded
A nested sequence of nonempty closed bounded intervals has nonempty intersection, and the intersection is a single point exactly when the lengths tend to
The recursion theorem
Finite sums and finite products, by recursion
Intervals of : the nine order-convex forms, nondegeneracy, and length
Integer powers
For the sequence is null, and for the sequence diverges to
Laws of finite sums and finite products
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
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
Every nonempty finite set of reals has a maximum and a minimum
Maximum and minimum of a set
For every in a complete ordered field there is a natural with
Every complete ordered field is Archimedean
Square roots exist: a unique with ; the positives are
Squaring is monotone on the nonnegatives
Absolute value in an ordered field
The canonical natural of a field
Limits and Cauchy sequences of reals
Metric space: iff , symmetry, and the triangle inequality; pseudometric and ultrametric