TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passverified 2026-08-05 (gpt-5.6-sol-codex-subscription)

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 $I$ be a set and let $(X_i, \mathcal{T}_i)_{i \in I}$ 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

$P \;:=\; \prod_{i \in I} X_i$

with the product topology (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 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 $I$ , a family $(X_i, \mathcal{T}_i)_{i \in I}$ of compact spaces, the product $P = \prod_{i \in I} X_i$ with the product topology, and the projections $\pi_i : P \to X_i$ .

[A1]

The Axiom of Choice, in the form: if $Y_i \ne \varnothing$ for every $i \in I$ then $\prod_{i \in I} Y_i \ne \varnothing$ (The Axiom of Choice).

[L1]

The family $\mathcal{G} := \{\, \pi_i^{-1}[U] : i \in I,\ U \in \mathcal{T}_i \,\}$ is a subbasis for the product topology on $P$ (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).

[L2]

Preimage commutes with unions: $\pi_i^{-1}[\bigcup \mathcal{V}] = \bigcup \{\, \pi_i^{-1}[V] : V \in \mathcal{V} \,\}$ , and $\pi_i^{-1}[X_i] = P$ (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).

[L3]

Each $(X_i, \mathcal{T}_i)$ is compact: every family of open subsets of $X_i$ with union $X_i$ has a finite subfamily with union $X_i$ , or $X_i = \varnothing$ 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).

[L4]

Alexander's subbase lemma: if $\mathcal{S}$ is a subbasis for the topology of a space $Y$ and every family $\mathcal{S}_0 \subseteq \mathcal{S}$ with $\bigcup \mathcal{S}_0 = Y$ has a finite subfamily with union $Y$ , then $Y$ 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

technique · direct

1.1

Let $\mathcal{S}_0 \subseteq \mathcal{G}$ satisfy $\bigcup \mathcal{S}_0 = P$ , and for each $i \in I$ put $\mathcal{U}_i := \{\, U \in \mathcal{T}_i : \pi_i^{-1}[U] \in \mathcal{S}_0 \,\}$ , a family of open subsets of $X_i$ cut out by a property and not by any selection; every member of $\mathcal{S}_0$ is $\pi_i^{-1}[U]$ for some $i \in I$ and some $U \in \mathcal{U}_i$ .

L1construct

2.1

There is $i_0 \in I$ with $\bigcup \mathcal{U}_{i_0} = X_{i_0}$ . For if $X_i \setminus \bigcup \mathcal{U}_i$ were nonempty for every $i \in I$ , then [A1] would give a point $a$ of $\prod_{i \in I} (X_i \setminus \bigcup \mathcal{U}_i)$ ; that $a$ lies in $P$ , and it lies in no member of $\mathcal{S}_0$ , since such a member is $\pi_i^{-1}[U]$ with $U \in \mathcal{U}_i$ while $a_i \notin \bigcup \mathcal{U}_i$ and so $a_i \notin U$ — contradicting $\bigcup \mathcal{S}_0 = P$ .

A1step 1.1

3.1

The family $\mathcal{U}_{i_0}$ consists of open subsets of $X_{i_0}$ with union $X_{i_0}$ , so by [L3] either $X_{i_0} = \varnothing$ , or there are $n \in \mathbb{N}$ and $U_0, \dots, U_n \in \mathcal{U}_{i_0}$ with $X_{i_0} = U_0 \cup \dots \cup U_n$ .

L3step 2.1

4.1

In the first case $P = \pi_{i_0}^{-1}[X_{i_0}] = \varnothing$ by [L2] and the empty subfamily of $\mathcal{S}_0$ has union $P$ ; in the second, $\pi_{i_0}^{-1}[U_0], \dots, \pi_{i_0}^{-1}[U_n]$ are members of $\mathcal{S}_0$ by step 1.1 and their union is $\pi_{i_0}^{-1}[U_0 \cup \dots \cup U_n] = \pi_{i_0}^{-1}[X_{i_0}] = P$ by [L2]. Either way $\mathcal{S}_0$ has a finite subfamily with union $P$ .

L2step 1.1step 3.1

5.1

Since $\mathcal{S}_0$ was an arbitrary subfamily of the subbasis $\mathcal{G}$ with union $P$ , [L4] applies and $P$ is compact.

L1L4step 1.1step 4.1∎

Remarks

Why a subbasic cover is easy and an arbitrary cover is not. A member of $\mathcal{G}$ restricts exactly one coordinate, so a subbasic cover of $P$ sorts itself into the families $\mathcal{U}_i$ , 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 theorem implies the Axiom of Choice, so the hypothesis cannot be dropped; that implication is not proved in this library, and the exact form it takes is recorded in Schechter 2006: Kelley's cofinite proof yields BPI, not the Axiom of Choice ‡, which corrects the classical derivation. 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

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 48 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

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)