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 .
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
- $\mathbb{R}^n$ as the set of functions $n \to \mathbb{R}$, and $d_1$, $d_2$, $d_\infty$ are metrics on it
- The absolute value makes $\mathbb{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
- 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$
- The recursion theorem
- Finite sums and finite products, by recursion
- Intervals of $\mathbb{R}$: the nine order-convex forms, nondegeneracy, and length
- Integer powers $a^m$
- For $|r| < 1$ the sequence $r^k$ is null, and for $|r| > 1$ the sequence $|r|^k$ diverges to $+\infty$
- 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 $\varepsilon > 0$ in a complete ordered field there is a natural $n \ge 1$ with $1/n < \varepsilon$
- Every complete ordered field is Archimedean
- Square roots exist: a unique $\sqrt{a} \ge 0$ with $(\sqrt{a})^2 = a$; the positives are $\{x^2 : x \neq 0\}$
- Squaring is monotone on the nonnegatives
- Absolute value in an ordered field
- The canonical natural $\iota(n) = n \cdot 1_F$ of a field
- Limits and Cauchy sequences of reals
- Metric space: $d(x,y) = 0$ iff $x = y$, symmetry, and the triangle inequality; pseudometric and ultrametric
Used by
- A globally state-Lipschitz vector field on ℝ×ℝⁿ has global solutions Corollary
- A subset of ℝⁿ with the product topology is compact exactly when it is closed and bounded, the product topology being the Euclidean metric topology Corollary
- Assuming countable choice, on a bounded measurable set, Lusin's closed core can be chosen compact Corollary
- Cauchy's theorem for a null-homologous cycle Corollary
- Each homotopy representative is supported on a finite CW subcomplex Corollary
- For n ≥ 1 every bounded sequence in ℝⁿ has a convergent subsequence Corollary
- Local formula for distance from the centre of a normal neighbourhood Corollary
- Nearby initial values share one Picard–Lindelöf time interval and one state cylinder Corollary
- Real and finite-dimensional Euclidean Ascoli–Arzelà criteria Corollary
- Smooth functions are weakly dense in distributions Corollary
- The index of a cycle is locally constant off its trace and vanishes far from it Corollary
- The modulus of a holomorphic function on a closed polydisc is bounded by its supremum on the distinguished boundary Corollary
- Uniqueness of finite Borel measures from their Fourier transforms Corollary
- A compact subset of ℝ³ need not be Jordan measurable Counterexample
- A complete manifold with zero global injectivity radius Counterexample
- A horned sphere has complementary components that need not be balls Counterexample
- Boundedness of first moments alone does not give uniform integrability Counterexample
- Collapsing the set of naturals inside ℝ to a point gives a quotient of ℝ that is not locally compact at the collapsed point Counterexample
- Pointwise limit discontinuous at zero signals mass escape Counterexample
- Proper endpoint maps joined by a nonproper combined homotopy Counterexample
- Refuted: convergence uniformly on every compact subset of ℝ implies uniform convergence. The maps x ↦ x/(n+1) separate the two Counterexample
- The disc algebra is unital and separating but not self-adjoint or dense Counterexample
- The Smith–Volterra–Cantor slab S×[0,1] is compact and not Jordan measurable Counterexample
- Uniform convergence on the closed unit disc does not give a holomorphic extension to a larger disc Counterexample
- Complex Lp classes and Euclidean test-function conventions Definition
- Finite convex cell complex and linear subdivision Definition
- Locally compact metric space: every point has a compact neighbourhood Definition
- Orientation local system and orientation cover Definition
- The support of a function on ℝⁿ and its compactly supported Riemann integral Definition
- Uniform-on-compacts metric on continuous path space Definition
- [0,1] and the Cantor set are compact, by Heine-Borel and by closedness inside [0,1]; and, assuming the Axiom of Choice, so is [0,1]^ℕ, by Tychonoff Example
- A finite maximum of affine functions and its active subgradients Example
- A normalized compactly supported top form on Euclidean space Example
- Affine interpolants with endpoints in a compact rectangle form a compact family Example
- Alexander duality for the standard equator Example
- C([0,1], ℝ) is complete, and on it the uniform metric and the supremum metric induce the same topology Example
- Continuous kernel integral operator is compact on c of an interval Example
- Dini's theorem applied to a nondecreasing sequence of piecewise linear approximations on [0,1], and what fails when the limit is not continuous Example
- Fredholm alternative for an integral equation Example
- Freudenthal stable range for spheres Example
…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
- Heine-Borel theorem (Wikipedia) (standard reference, not scraped)
- Compact space (Wikipedia) (standard reference, not scraped)
- W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 2 (standard reference, not scraped)