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.
The quasicompact convention, why compactness of a subset is read intrinsically here, and what each result on this page costs in choice
Three conventions, fixed once
1. Compact means the open-cover condition and nothing more. Following Bourbaki, some authors reserve compact for a space that is both quasicompact, meaning every open cover has a finite subcover, and Hausdorff, and then say quasicompact for the cover condition alone. This library takes the more widely adopted convention: Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right defines compact as the cover condition, the word quasicompact is not used, and every Hausdorff hypothesis is written into the statement that needs it — as in In a Hausdorff space a point and a disjoint compact set, and two disjoint compact sets, have disjoint open neighbourhoods; hence every compact subset is closed, and in a compact Hausdorff space the compact subsets are exactly the closed ones and In a locally compact Hausdorff space every point has a neighbourhood base of compact sets, every open subspace and every closed subspace is locally compact, every open set around a point contains an open set with compact closure inside it, and every compact set sits inside an open set with compact closure. A reader arriving from the other convention should read every unqualified "compact" here as "quasicompact".
2. Compactness of a subset is intrinsic. Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right calls compact when the subspace carries is a compact space, not when every family of open subsets of covering has finitely many members covering it. The two conditions agree, and that is a theorem, A subspace is compact exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it; no proof here uses the ambient reading without citing it. Compactness belongs to together with its topology. It is preserved under a homeomorphic realization as a subspace, but a different ambient may induce a different topology and a different compactness answer. The metric development fixed the same reading, and that the two developments describe one notion is For a metric space with its metric topology, compactness in the topological sense is compactness in the metric sense, and the two notions of compact subset coincide.
Relative compactness is the exception, and deliberately so: Countably compact, Lindel"of, sequentially compact, limit point compact and -compact spaces, and relatively compact subsets defines to be relatively compact in when is compact, and the closure is taken in . That condition really is about inside and changes when the ambient space changes.
3. A separation axiom is written out rather than named where it is not available. Claim 4 of Compact implies countably compact, Lindel"of and limit point compact; countably compact together with Lindel"of implies compact; and, at the cost of countable or dependent choice, sequentially compact implies countably compact, countably compact implies limit point compact, and the converse holds when every singleton is closed needs every singleton to be closed. That condition is a named separation axiom, and the page naming it is not among this page's declared prerequisites, so the hypothesis is stated in the vocabulary of open and closed sets and nothing is asserted about the axiom it belongs to. On this page a neighbourhood need not be open, and the intersection of no sets is the whole space; these two general conventions are in force without further comment.
The choice ledger
Every entry below is a statement about the proof given in this library, and about nothing else. Each is an upper bound on what that proof spends; no item on this page claims that a choice principle is necessary, because that would be an independence result and this library proves none.
Theorems of ZF, spending no choice principle at all. A subspace is compact exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it, For a metric space with its metric topology, compactness in the topological sense is compactness in the metric sense, and the two notions of compact subset coincide, A space is compact exactly when every family of closed subsets with the finite intersection property has nonempty intersection, A closed subspace of a compact space is compact, and a finite union of compact subspaces is compact, In a Hausdorff space a point and a disjoint compact set, and two disjoint compact sets, have disjoint open neighbourhoods; hence every compact subset is closed, and in a compact Hausdorff space the compact subsets are exactly the closed ones, A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism, Tube lemma: if is compact and an open contains , then contains for some open , A product of finitely many compact spaces is compact in the product topology, A subset of with the product topology is compact exactly when it is closed and bounded, the product topology being the Euclidean metric topology, In a locally compact Hausdorff space every point has a neighbourhood base of compact sets, every open subspace and every closed subspace is locally compact, every open set around a point contains an open set with compact closure inside it, and every compact set sits inside an open set with compact closure, is compact and contains as an open subspace; is dense in exactly when is not compact; and is Hausdorff exactly when is locally compact and Hausdorff, On an ordinal with its order topology the sets and form a basis of clopen sets, the isolated points are exactly the non-limit ordinals, and the space is Hausdorff, In a compact Hausdorff space every quasicomponent is connected, so quasicomponents and components coincide, claim 1 of Compact implies countably compact, Lindel"of and limit point compact; countably compact together with Lindel"of implies compact; and, at the cost of countable or dependent choice, sequentially compact implies countably compact, countably compact implies limit point compact, and the converse holds when every singleton is closed, claims 1 and 2 of Every successor ordinal is compact in its order topology and every limit ordinal is not; and, assuming countable choice, is countably compact and sequentially compact while is compact, and claims 1 and 3 of Every closed initial segment of the long ray is compact; the long ray is not compact; and, assuming countable choice, it is countably compact and not Lindel"of. The refutations of FALSE: a compact subset of a topological space is closed and of FALSE: every subspace of a locally compact space is locally compact are also theorems of ZF: each exhibits a single explicit witness and spends no choice principle.
Where a proof in that list does make a selection, the selection 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 itself a theorem of ZF. Tube lemma: if is compact and an open contains , then contains for some open avoids even the finite selection: it indexes its cover by pairs of open sets, so the compactness criterion hands back the second entries with the indices. In a Hausdorff space a point and a disjoint compact set, and two disjoint compact sets, have disjoint open neighbourhoods; hence every compact subset is closed, and in a compact Hausdorff space the compact subsets are exactly the closed ones avoids the arbitrary selection by collecting the family of all open sets that work rather than choosing one for each point, and then makes only the finite selections that Every natural-number-indexed list of nonempty sets has a choice function on its family of values supplies. The textbook phrase "for each choose disjoint open " is a selection over an arbitrary index set, that is the full Axiom of Choice (The Axiom of Choice), and it is avoided throughout this page.
Spending the Axiom of Choice, through Zorn's lemma (Zorn's lemma). Alexander's subbase lemma: if every cover by members of a fixed subbasis has a finite subcover then the space is compact; the proof is an application of Zorn's lemma spends it exactly once, to obtain a maximal open cover without a finite subcover; Tychonoff's theorem: an arbitrary product of compact spaces is compact in the product topology, assuming the Axiom of Choice inherits that use and spends it a second time directly, to produce a point of a product of nonempty sets; and FALSE: every compact space is sequentially compact inherits both, since its witness is compact by Tychonoff. Tychonoff's theorem implies the Axiom of Choice, so, under the standing assumption that ZF is consistent, no proof of it in ZF alone can exist; the exact form of that implication, and the correction of the classical derivation, are recorded in Schechter 2006: Kelley's cofinite proof yields BPI, not the Axiom of Choice ‡, which this library states and does not prove. Where the ultrafilter lemma sits between the two is What the ultrafilter lemma costs: a choice principle strictly weaker than AC.
Spending the Axiom of Countable Choice (The Axiom of Countable Choice ()). Claims 2 and 4 of Compact implies countably compact, Lindel"of and limit point compact; countably compact together with Lindel"of implies compact; and, at the cost of countable or dependent choice, sequentially compact implies countably compact, countably compact implies limit point compact, and the converse holds when every singleton is closed, each of which picks a point outside each of countably many nested unions; claim 3 of Every successor ordinal is compact in its order topology and every limit ordinal is not; and, assuming countable choice, is countably compact and sequentially compact while is compact; claims 2 and 4 of Every closed initial segment of the long ray is compact; the long ray is not compact; and, assuming countable choice, it is countably compact and not Lindel"of; and the two false statements whose witnesses those are, FALSE: every sequentially compact space is compact and FALSE: every countably compact space is compact. In the ordinal and long-ray results the principle enters through a boundedness theorem for at most countable subsets, which carries the hypothesis in its own statement — and not only through it: claim 2 of Every closed initial segment of the long ray is compact; the long ray is not compact; and, assuming countable choice, it is countably compact and not Lindel"of spends it once more directly, to pick a point in each of countably many nonempty sets, and claim 3 of Every successor ordinal is compact in its order topology and every limit ordinal is not; and, assuming countable choice, is countably compact and sequentially compact while is compact inherits a further use through claim 2 of Compact implies countably compact, Lindel"of and limit point compact; countably compact together with Lindel"of implies compact; and, at the cost of countable or dependent choice, sequentially compact implies countably compact, countably compact implies limit point compact, and the converse holds when every singleton is closed.
Spending the Axiom of Dependent Choice (The axiom of dependent choice: a relation in which every element is related to something admits an -indexed chain). Claim 3 of Compact implies countably compact, Lindel"of and limit point compact; countably compact together with Lindel"of implies compact; and, at the cost of countable or dependent choice, sequentially compact implies countably compact, countably compact implies limit point compact, and the converse holds when every singleton is closed, where it is spent to extract a countably infinite subset from an infinite set, which is not a theorem of ZF; the claim about countably infinite subsets alone, claim 1(d) of the same theorem, is free of that cost. And Assuming dependent choice, every locally compact Hausdorff space is a Baire space, which spends it once, through Dependent choice along a sequence of relations: if is entire on for every , then from any there is a sequence with , to run a shrinking construction whose admissible successors change with the stage. In both cases dependent choice is an upper bound on the cost of the argument given here and is not asserted to be necessary; for the Baire theorem in particular the several versions of the statement correspond to different principles over ZF, as The Baire category theorem is four inequivalent statements over ZF ‡ records.
The metric ledger is separate and remains in force. What each implication between the compactness properties of a metric space costs is recorded in 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. Nothing here supersedes it: by For a metric space with its metric topology, compactness in the topological sense is compactness in the metric sense, and the two notions of compact subset coincide for compactness itself, and by the agreement clauses of Countably compact, Lindel"of, sequentially compact, limit point compact and -compact spaces, and relatively compact subsets for countable compactness, sequential compactness and limit point compactness, the metric statements are the statements of this page read in a metric topology, so the two ledgers describe the same arrows wherever they overlap and different arrows elsewhere.
A warning about equivalences. Compact implies countably compact, Lindel"of and limit point compact; countably compact together with Lindel"of implies compact; and, at the cost of countable or dependent choice, sequentially compact implies countably compact, countably compact implies limit point compact, and the converse holds when every singleton is closed is deliberately stated as a list of implications rather than as one equivalence, because an equivalence proved by going round a cycle charges every arrow in it the maximum cost. The same discipline is what 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 exists to enforce on the metric side.
Depends on
- Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right
- A subspace is compact exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it
- Assuming dependent choice, every locally compact Hausdorff space is a Baire space
- Dependent choice along a sequence of relations: if $R_n$ is entire on $A$ for every $n$, then from any $a$ there is a sequence with $a_n \mathbin{R_n} a_{n+1}$
- For a metric space with its metric topology, compactness in the topological sense is compactness in the metric sense, and the two notions of compact subset coincide
- A space is compact exactly when every family of closed subsets with the finite intersection property has nonempty intersection
- Alexander's subbase lemma: if every cover by members of a fixed subbasis has a finite subcover then the space is compact; the proof is an application of Zorn's lemma
- Tychonoff's theorem: an arbitrary product of compact spaces is compact in the product topology, assuming the Axiom of Choice
- A product of finitely many compact spaces is compact in the product topology
- Tube lemma: if $K$ is compact and an open $N \subseteq X \times Z$ contains $K \times \{z_0\}$, then $N$ contains $K \times W$ for some open $W \ni z_0$
- Countably compact, Lindel\"of, sequentially compact, limit point compact and $\sigma$-compact spaces, and relatively compact subsets
- Compact implies countably compact, Lindel\"of and limit point compact; countably compact together with Lindel\"of implies compact; and, at the cost of countable or dependent choice, sequentially compact implies countably compact, countably compact implies limit point compact, and the converse holds when every singleton is closed
- Every successor ordinal is compact in its order topology and every limit ordinal is not; and, assuming countable choice, $\omega_1$ is countably compact and sequentially compact while $\omega_1 + 1$ is compact
- Every closed initial segment of the long ray is compact; the long ray is not compact; and, assuming countable choice, it is countably compact and not Lindel\"of
- Locally compact topological space: every point has a compact neighbourhood; and what this says in a metric space
- The one-point (Alexandroff) compactification $X^{*} = X \cup \{\infty\}$, whose open sets are the open sets of $X$ together with the complements in $X^{*}$ of the closed compact subsets of $X$
- Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not
- Zorn's lemma
- The Axiom of Choice
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
- The axiom of dependent choice: a relation in which every element is related to something admits an $\mathbb{N}$-indexed chain
- Every natural-number-indexed list of nonempty sets has a choice function on its family of values
- What the ultrafilter lemma costs: a choice principle strictly weaker than AC
Used by
Nothing in the library uses this result yet.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 191 results over 30 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)
- Axiom of choice (Wikipedia) (standard reference, not scraped)
- H. Herrlich, Axiom of Choice, Lecture Notes in Mathematics 1876, Springer 2006 (standard reference, not scraped)