Tychonoff's Theorem

Statement

Let $\{X_i\}_{i \in I}$ be an arbitrary (possibly uncountable) family of topological spaces. The product space $\prod_{i \in I} X_i$, equipped with the product topology (the coarsest topology making all projections continuous), is compact if and only if each factor $X_i$ is compact:

Visualization

For two compact intervals $[0,1]$ and $[0,1]$, their product is the closed unit square — compact.

[0,1] × [0,1]:

1 ┌─────────────────┐
  │                 │
  │   Compact grid  │
  │   of [0,1]²     │
  │                 │
  │  Each row [0,1] │ ← compact
  │  Each col [0,1] │ ← compact
0 └─────────────────┘
  0                 1
  ↑_________________↑
     product is compact (= closed bounded square, Heine–Borel)

For infinitely many factors [0,1] × [0,1] × ··· (countably or uncountably many):
  The product topology is coarser than the norm topology.
  Tychonoff: still compact! (Alexander subbase theorem + Axiom of Choice)

Each horizontal slice is a copy of a compact interval; the infinite product assembles them all into one compact space. This is remarkable: no single bounded-metric characterisation works in infinite dimensions, yet the purely topological notion of compactness is preserved.

Proof Sketch

The standard proof uses the Alexander subbase theorem: a topological space is compact iff every open cover by subbase elements (preimages of open sets in each factor) has a finite subcover.

Given an open cover by subbase elements $\pi_i^{-1}(U_i)$, if for every $i$ the sets $\{U : \pi_i^{-1}(U) \text{ in cover}\}$ covered $X_i$, compactness of each $X_i$ would give a finite subcover. A contrapositive argument (using the Axiom of Choice, e.g. via Zorn's lemma) shows the cover must already contain a finite subcover.

The proof is equivalent to the Axiom of Choice: for infinite products, neither direction is provable in ZF without AC.

Connections

• Heine–Borel TheoremHeine–Borel Theorem$$K \subseteq \mathbb{R}^n \;\text{compact} \iff K \;\text{closed and bounded}$$In ℝⁿ, a subset is compact if and only if it is closed and boundedRead more → — the $n$-dimensional case: $[0,1]^n$ is compact as a finite product of compact intervals. Tychonoff is the infinite-dimensional extension.
• Bolzano–Weierstrass TheoremBolzano–Weierstrass Theorem$$\text{bounded } (x_n) \subseteq \mathbb{R}^n \implies \exists\, \text{convergent subsequence}$$Every bounded sequence in ℝⁿ has a convergent subsequenceRead more → — in the product (weak) topology on infinite-dimensional spaces, Tychonoff's theorem recovers sequential compactness results (e.g. Banach–Alaoglu theorem for weak-* topology).
• Brouwer Fixed-Point TheoremBrouwer Fixed-Point Theorem$$f : D^n \to D^n \text{ continuous} \implies \exists\, x,\; f(x) = x$$Every continuous map from a compact convex set to itself has a fixed pointRead more → — Schauder's fixed-point theorem in Banach spaces uses weak compactness (Tychonoff + Banach–Alaoglu) to generalise Brouwer to infinite dimensions.
• Urysohn's LemmaUrysohn's Lemma$$\exists\, f : X \to [0,1],\quad f|_s = 0,\; f|_t = 1$$In a normal space, disjoint closed sets can be separated by a continuous functionRead more → — a product of completely regular (Tychonoff) spaces is completely regular; Urysohn-type separation passes to products.
• Hausdorff DistanceHausdorff Distance$$d_H(A, B) = \max\left(\sup_{a \in A} d(a, B),\ \sup_{b \in B} d(b, A)\right)$$A metric on non-empty compact sets, foundation for the IFS attractor theoremRead more → — the hyperspace of compact subsets inherits compactness from an ambient compact space; Tychonoff underlies this transfer.
• Iterated Function SystemsIterated Function Systems$$A = \bigcup_{i=1}^{N} f_i(A)$$Constructing fractals via contractive affine transformationsRead more → — the space of probability measures on a compact space (used in IFS analysis) is compact in the weak-* topology by Tychonoff + Riesz representation.

import Mathlib.Topology.Compactness.Compact

open Set Topology

/-- **Tychonoff's theorem**: a product of compact sets is compact (Set.pi version).
    Mathlib: `isCompact_univ_pi` in `Mathlib.Topology.Compactness.Compact`. -/
theorem tychonoff {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)]
    {s : ∀ i, Set (X i)} (h : ∀ i, IsCompact (s i)) :
    IsCompact (pi univ s) :=
  isCompact_univ_pi h

/-- **Tychonoff's theorem** (instance form): a product of compact spaces is compact. -/
example {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)]
    [∀ i, CompactSpace (X i)] : CompactSpace (∀ i, X i) :=
  inferInstance