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.
Tychonoff's theorem: an arbitrary product of compact spaces is compact in the product topology, assuming the Axiom of Choice
Statement
Assume the Axiom of Choice (The Axiom of Choice).
Let be a set and let be a family of compact topological spaces (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right, Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison). Then the product
with the product topology (The product set of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space) is compact.
The Axiom of Choice is spent twice, and both uses are flagged below. Once inside 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, through Zorn's lemma (Zorn's lemma), and once directly at step 2.1, to produce a point of a product of nonempty sets.
Facts & Assumptions
Given: A set , a family of compact spaces, the product with the product topology, and the projections .
The Axiom of Choice, in the form: if for every then (The Axiom of Choice).
The family is a subbasis for the product topology on (The product set of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space, Basis and subbasis for a topology, and the topology generated by a family of sets).
Each is compact: every family of open subsets of with union has a finite subfamily with union , or and the empty subfamily covers it (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right).
Alexander's subbase lemma: if is a subbasis for the topology of a space and every family with has a finite subfamily with union , then is compact (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).
Proof
Let satisfy , and for each put , a family of open subsets of cut out by a property and not by any selection; every member of is for some and some .
There is with . For if were nonempty for every , then [A1] would give a point of ; that lies in , and it lies in no member of , since such a member is with while and so — contradicting .
The family consists of open subsets of with union , so by [L3] either , or there are and with .
In the first case by [L2] and the empty subfamily of has union ; in the second, are members of by step 1.1 and their union is by [L2]. Either way has a finite subfamily with union .
Since was an arbitrary subfamily of the subbasis with union , [L4] applies and is compact.
Remarks
Why a subbasic cover is easy and an arbitrary cover is not. A member of restricts exactly one coordinate, so a subbasic cover of sorts itself into the families , one per coordinate, and the whole argument is the observation that one of those families must already cover its own factor. A member of an arbitrary open cover is a union of basic sets, each restricting its own finite set of coordinates, so such a member need not be determined by any finite set of coordinates and the cover admits no such sorting; that is why the theorem is proved through 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 rather than directly.
The unrestricted product principle implies AC. The later The compact T1 product theorem is equivalent to AC proves this already for compact factors, using a cofinite space with a separately adjoined isolated point and the finite-intersection characterization of compactness. Its forward implication uses the theorem proved here. The choice ledger for this page is The quasicompact convention, why compactness of a subset is read intrinsically here, and what each result on this page costs in choice.
For an index set that is a natural number neither use of choice is needed, and the result is then A product of finitely many compact spaces is compact in the product topology, a theorem of ZF proved on this page by induction and the tube lemma.
A product of compact spaces is compact for the product topology and in general not for the box topology. Nothing above survives the substitution: the box topology has no subbasis of one-coordinate restrictions, and the sorting carried out in the first step of the proof is exactly what disappears.
Depends on
- 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
- Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right
- The product set $\prod_{i \in I} X_i$ of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space
- Basis and subbasis for a topology, and the topology generated by a family of sets
- The Axiom of Choice
- Zorn's lemma
- Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison
Used by
- [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
- Haar measure on an infinite product of compact groups Example
- Under the Axiom of Choice, the Hilbert cube is compact, Polish, and universal for separable metrizable spaces Example
- FALSE: every Baire space is completely metrizable False statement
- FALSE: every compact space is sequentially compact False statement
- Aut(U_ℚ^<) is extremely amenable Lemma
- Duals of finite products and of discrete direct sums Lemma
- Glimm criteria for separable C star algebras and type I groups Lemma
- Haar candidate sets have the finite intersection property Lemma
- Measurable fields of von Neumann algebras have measurable commutants and centers Lemma
- Weak containment of the trivial representation and almost invariant vectors Lemma
- The compact Hausdorff product theorem uses the ultrafilter lemma, while the published arbitrary compact product theorem assumes the full Axiom of Choice Remark
- The quasicompact convention, why compactness of a subset is read intrinsically here, and what each result on this page costs in choice Remark
- Compact groups have discrete duals and discrete groups have compact duals Theorem
- Finite étale covers are equivalent to finite continuous étale fundamental group sets Theorem
- Inverse limits of finite discrete groups are Hausdorff and totally disconnected, and compact assuming Choice Theorem
- The arbitrary compact product theorem is equivalent to AC Theorem
- The compact T1 product theorem is equivalent to AC Theorem
- Under Choice, pointwise closure is compact exactly when every coordinate set has compact closure Theorem
- Under the Axiom of Choice, a space is Polish exactly when it is homeomorphic to a G_δ subspace of the Hilbert cube Theorem
- Under the Axiom of Choice, countable products of Čech-complete spaces are Čech-complete Theorem
Dependency tree · two levels
22 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
- Tychonoff's theorem (Wikipedia) (standard reference, not scraped)
- Alexander subbase theorem (Wikipedia) (standard reference, not scraped)
- J. Munkres, Topology, 2nd ed., §37 (standard reference, not scraped)
- Stacks Project, Tag 08ZU (standard reference, not scraped)