Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adapted
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

Facts & Assumptions

Given: A set I, a family (Xi,Ti)i∈I of compact spaces, the product P=∏i∈IXi with the product topology, and the projections πi:P→Xi.

[A1]

The Axiom of Choice, in the form: if Yi≠∅ for every i∈I then ∏i∈IYi≠∅ (The Axiom of Choice).

[L2]

Preimage commutes with unions: πi−1[⋃V]=⋃{ πi−1[V]:V∈V }, and πi−1[Xi]=P (The product set ∏i∈IXi 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 (Xi,Ti) is compact: every family of open subsets of Xi with union Xi has a finite subfamily with union Xi, or Xi=∅ 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 S is a subbasis for the topology of a space Y and every family S0⊆S with ⋃S0=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.1L1construct

Let S0⊆G satisfy ⋃S0=P, and for each i∈I put Ui:={ U∈Ti:πi−1[U]∈S0 }, a family of open subsets of Xi cut out by a property and not by any selection; every member of S0 is πi−1[U] for some i∈I and some U∈Ui.

2.1A1step 1.1

There is i0∈I with ⋃Ui0=Xi0. For if Xi∖⋃Ui were nonempty for every i∈I, then [A1] would give a point a of ∏i∈I(Xi∖⋃Ui); that a lies in P, and it lies in no member of S0, since such a member is πi−1[U] with U∈Ui while ai∉⋃Ui and so ai∉U — contradicting ⋃S0=P.

3.1L3step 2.1

The family Ui0 consists of open subsets of Xi0 with union Xi0, so by [L3] either Xi0=∅, or there are n∈N and U0,…,Un∈Ui0 with Xi0=U0∪⋯∪Un.

4.1L2step 1.1step 3.1

In the first case P=πi0−1[Xi0]=∅ by [L2] and the empty subfamily of S0 has union P; in the second, πi0−1[U0],…,πi0−1[Un] are members of S0 by step 1.1 and their union is πi0−1[U0∪⋯∪Un]=πi0−1[Xi0]=P by [L2]. Either way S0 has a finite subfamily with union P.

5.1L1L4step 1.1step 4.1∎

Since S0 was an arbitrary subfamily of the subbasis G with union P, [L4] applies and P is compact.

Remarks

Why a subbasic cover is easy and an arbitrary cover is not. A member of G restricts exactly one coordinate, so a subbasic cover of P sorts itself into the families Ui, 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 T1 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

Used by

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