TheoremStatement: Literature-sourcedProof: Literature-sourcedPipeline-generatedaudited 2026-09-22

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 arbitrary compact product theorem is equivalent to AC

Statement

Over $Z F$ , AC (The Axiom of Choice) is equivalent to the assertion that every product of arbitrary compact spaces (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) is compact. The empty product is a one-point space and is included.

Facts & Assumptions

Given: AC and, in the reverse direction, the hypothesis that every product of compact spaces is compact.

[F1]

Under AC, Tychonoff's theorem gives compactness of every product of compact spaces, the empty product being the one-point space (Tychonoff's theorem: an arbitrary product of compact spaces is compact in the product topology, assuming the Axiom of Choice, 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).

[F2]

Over ZF, AC is equivalent to compactness of every product of compact $T_{1}$ spaces (The compact T1 product theorem is equivalent to AC, $T_{0}$ (Kolmogorov) and $T_{1}$ (Frechet) spaces).

[F3]

Over ZF, BPI is equivalent to compactness of every product of compact Hausdorff spaces (Compact Hausdorff Tychonoff is equivalent to BPI).

Proof

technique · direct

1.1

Under AC every product of compact spaces is compact by [F1], and the empty product is the one-point space; this is one direction.

assume-hypF1

2.1

Conversely, if every product of compact spaces is compact then in particular every product of compact $T_{1}$ spaces is compact, since compact $T_{1}$ spaces are compact spaces; by [F2] this gives AC.

step 1.1F2

3.1

The two directions give the displayed equivalence; in particular the compact-Hausdorff case is a different statement, whose strength is BPI by [F3] and which is not identified with the arbitrary compact case here.

step 1.1step 2.1F2F3∎

Remarks

Why the two strengths differ. Products of compact $T_{1}$ spaces and products of compact Hausdorff spaces are not the same assertion: the first is equivalent to AC by [F2] and the second to BPI by [F3]. The empty product is compact in both cases and therefore separates nothing.

Depends on

Used by

Choice ledger for Baire, Urysohn, Stone, and Tychonoff Remark

Dependency tree · two levels

28 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

Kyriakos Keremedis and Eleftherios Tachtsis, Wallman Compactifications and Tychonoff's Compactness Theorem in ZF (standard reference, not scraped)