How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced — the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted — a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated — a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
A compact subset of is closed and bounded
Statement
Let be compact (Open cover, subcover, compact subset of (every open cover has a finite subcover), and sequentially compact subset). Then is closed (Open subset of (every point has a neighbourhood inside it), closed subset (complement open), and clopen) and bounded (Lower bound, bounded below, bounded set).
Two covers do the work, and they use the Archimedean property in its two different forms. Boundedness is read off the cover of by the intervals , which needs the cofinal form, that the canonical naturals exceed every real (Every complete ordered field is Archimedean). Closedness is read off the cover of , for a point outside it, by the sets , which needs the reciprocal form, that the reciprocals of the naturals get below every positive real (For every in a complete ordered field there is a natural with ); the cofinal form alone does not deliver it.
Facts & Assumptions
Given: A compact set . Throughout, denotes both a natural number and the canonical natural of , as is standard.
Open cover, finite subfamily and compactness: every open cover of has a subcover that is empty or of the form with (Open cover, subcover, compact subset of (every open cover has a finite subcover), and sequentially compact subset).
is open when every admits with ; is closed when is open; each of the forms , , , is an open set (Open subset of (every point has a neighbourhood inside it), closed subset (complement open), and clopen, Intervals of : the nine order-convex forms, nondegeneracy, and length).
is bounded when there are with for every (Lower bound, bounded below, bounded set).
Archimedean property, cofinal form: for every there is a natural with (Every complete ordered field is Archimedean).
Archimedean property, reciprocal form: 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).
Absolute value: , , , and exactly when (Basic properties of the absolute value).
Triangle inequality: (The triangle inequality).
Every 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).
Canonical naturals: for and in gives (Canonical naturals are positive and strictly increasing); reciprocation of positives reverses the order (Inverses of positives are positive, and reciprocation reverses order); the order is total and transitive (Complete ordered field (least-upper-bound property), Ordered field). These order-arithmetic facts are stated by their sources for the strict order only; the nonstrict forms used below follow by adjoining the equality case, in which the two sides coincide.
Proof
For each natural put , an open set by [L2]. The family covers , hence covers : given , [L5] supplies with , and then and by [L7], so .
Let and for each natural put , which is defined because has a positive inverse by [L10]. Each is open: given , put ; for the triangle inequality [L8] gives , whence and . The family covers : for one has , so by [L7], and [L6] supplies with , that is .
Apply compactness to the cover of step 1.1. If the finite subcover is empty then and holds vacuously for ; otherwise there are naturals with , and putting by [L9] we get for each , since gives and in by [L10]. Hence and for every , so is bounded.
Apply compactness to the cover of step 1.2. If the finite subcover is empty then and holds vacuously for , so take ; otherwise there are naturals with , and putting by [L9] we get for each , since gives by [L10]. In both cases , that is, for every .
Consequently , since has while would give , which trichotomy forbids; so . As was an arbitrary point of , that complement is open and is closed.
is bounded by step 2.1 and closed by step 3.1, which is the assertion.
Remarks
-
Why the reciprocal form is unavoidable in step 1.2. The sets covering must exhaust the complement of the single point , and the natural way to do that with open sets is to exclude a shrinking closed neighbourhood of . The radii of those neighbourhoods have to become smaller than for each , and that is exactly the statement of For every in a complete ordered field there is a natural with . The cofinal form Every complete ordered field is Archimedean says the naturals get large, which is what step 1.1 needs and is a different assertion; the corollary exists in this library precisely so that the inversion between them is done once.
-
The converse needs completeness and this lemma does not. Nothing above uses the least-upper-bound property except through the Archimedean property; beyond the ordered-field axioms the proof asks only for that property and for the existence of a maximum of a finite set. The converse, that a closed bounded set is compact, is false in (FALSE: in every ordered field a closed bounded set is compact, so Heine-Borel needs no completeness) and true in (A subset of is compact if and only if it is closed and bounded).
-
Neither conclusion can be strengthened to an equivalence on its own. A closed set need not be compact and a bounded set need not be compact, and both failures are recorded in is closed and not compact, and is bounded and not compact: neither hypothesis of Heine-Borel can be dropped ↗.
Depends on
- Open cover, subcover, compact subset of $\mathbb{R}$ (every open cover has a finite subcover), and sequentially compact subset
- Open subset of $\mathbb{R}$ (every point has a neighbourhood inside it), closed subset (complement open), and clopen
- Lower bound, bounded below, bounded set
- The $\varepsilon$-neighbourhood and the punctured $\varepsilon$-neighbourhood of a point of $\mathbb{R}$
- Intervals of $\mathbb{R}$: the nine order-convex forms, nondegeneracy, and length
- Every complete ordered field is Archimedean
- For every $\varepsilon > 0$ in a complete ordered field there is a natural $n \ge 1$ with $1/n < \varepsilon$
- Basic properties of the absolute value
- The triangle inequality
- Every nonempty finite set of reals has a maximum and a minimum
- Maximum and minimum of a set
- Canonical naturals are positive and strictly increasing
- Inverses of positives are positive, and reciprocation reverses order
- Complete ordered field (least-upper-bound property)
- Ordered field
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 39 results over 12 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- Compact space (Wikipedia) (standard reference, not scraped)
- Heine-Borel theorem (Wikipedia) (standard reference, not scraped)
- W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 2 (Thm 2.34, 2.35) (standard reference, not scraped)
- J. Lebl, Basic Analysis I, §7.4 (standard reference, not scraped)
- J. K. Hunter, An Introduction to Real Analysis (standard reference, not scraped)