Alphabeta Math
RemarkRemark: AI-adaptedProof: Not applicableSession-authored (Fable 5 assisted)verified 2026-08-05 (gpt-5.6-sol-codex-subscription) rests on unproved material (inherited)
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.

Rests on 2 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Feferman 1965: ZF does not prove that a free ultrafilter on the naturals exists and Halpern and Lévy 1971: the Boolean prime ideal theorem does not imply the Axiom of Choice. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

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 AXA \subseteq X compact when the subspace AA carries is a compact space, not when every family of open subsets of XX covering AA 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 AA 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 σ\sigma-compact spaces, and relatively compact subsets defines AA to be relatively compact in XX when A\overline{A} is compact, and the closure is taken in XX. That condition really is about AA inside XX 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 KK is compact and an open NX×ZN \subseteq X \times Z contains K×{z0}K \times \{z_0\}, then NN contains K×WK \times W for some open Wz0W \ni z_0, A product of finitely many compact spaces is compact in the product topology, A subset of Rn\mathbb{R}^n 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, XX^{*} is compact and contains XX as an open subspace; XX is dense in XX^{*} exactly when XX is not compact; and XX^{*} is Hausdorff exactly when XX is locally compact and Hausdorff, On an ordinal with its order topology the sets [0,β][0,\beta] and (α,β](\alpha,\beta] 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, ω1\omega_1 is countably compact and sequentially compact while ω1+1\omega_1 + 1 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 KK is compact and an open NX×ZN \subseteq X \times Z contains K×{z0}K \times \{z_0\}, then NN contains K×WK \times W for some open Wz0W \ni z_0 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 yKy \in K choose disjoint open Uy,VyU_y, V_y" 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 (ACω\mathrm{AC}_\omega)). 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, ω1\omega_1 is countably compact and sequentially compact while ω1+1\omega_1 + 1 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, ω1\omega_1 is countably compact and sequentially compact while ω1+1\omega_1 + 1 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 N\mathbb{N}-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 RnR_n is entire on AA for every nn, then from any aa there is a sequence with anRnan+1a_n \mathbin{R_n} a_{n+1}, 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 σ\sigma-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

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