For finite collections of compact spaces, this is not very surprising and is easy to prove. The statement is in fact true for infinite collections of arbitrary size, depends heavily on the peculiar definition of the product topology in this case, and is equivalent to the axiom of choice.
Tychonoff's theorem is complex, and its proof is often approached in parts, proving helpful lemmas first. One approach to proving it (Munkres section 37) exploits an alternative formulation of compactness based on the finite intersection property. The two lemmas are shown follow:
Once we have D, we can project it along each of the infinitely many dimensions to obtain FIP sets in the spaces forming the product. But we know these spaces are compact, and so we can choose a point in each space from the intersection of that space's projected D collection. These become the coordinates of an element x in the infinite product space.
Finally, it's possible to show that if one of the spaces in the product has a subbasis element containing that space's coordinate of x, then the "tube" formed by pulling that subbasis into the full product space with an inverse projection map will contain x and will also intersect every element of D. Lemma 2 then tells us that each of these tubes is in D. But tubes form a subbasis in the product topology, and so, also by Lemma 2, all basis elements containing x are in D. But then these basis elements intersect every element of D, and so x is a limit point of each element of D, and so is in the closure of each element of D.
It was mentioned above that Tychonoff's theorem is, in fact, equivalent to the axiom of choice (AC). This seems surprising at first, since AC is an entirely set-theoretic formulation, not mentioning topology at all. But in view of the complexity of the proof of Tychonoff's theorem, and that mathematics can be completely modeled in set theory (i.e. the category of sets is a topos), this is not altogether unexpected. This equivalence shows that the formulation of compactness in infinite product spaces is nonconstructive (also not altogether unexpected, since AC itself is equivalent to asserting whether or not an infinite product is empty!).
To prove that Tychonoff's theorem implies the axiom of choice, we establish that every infinite cartesian product of non-empty sets is nonempty. It is actually a more comprehensible proof than the above (probably because it does not involve Zorn's Lemma, which is quite opaque to most mathematicians as far as intuition is concerned!). The trickiest part of the proof is introducing the right topology. The right topology, as it turns out, is the cofinite topology with a small twist. It turns out that every set given this topology automatically becomes a compact space. Once we have this fact, Tychonoff's theorem can be applied; we then use the FIP definition of compactness (the FIP is sure convenient!). Anyway, to get to the proof itself (due to J.L. Kelley):
Let {Ai} be an indexed family of nonempty sets, for i ranging in I (where I is an arbitrary indexing set). We wish to show that the cartesian product of these sets is nonempty. Now, for each i, take Xi to be Ai with the index i itself tacked on (renaming the indices using the disjoint union if necessary, we may assume that i is not a member of Ai, so simply take Xi = Ai ∪ {i}).
Now the define cartesian product
Now here's the trick: we give each Xi the topology whose open sets are the cofinite subsets of Xi, plus the empty set (the cofinite toplogy) and the singleton {i}.
This makes Xi compact, and by Tychonoff's theorem, X is also compact (in the product topology). The projection maps are continuous; all the Ai's are closed, being complements of the singleton open set {i} in Xi. So the inverse images πi-1(Ai) are closed subsets of X. We note that
Tychonoff's theorem and the Axiom of Choice
along with the natural projection maps πi which take a member of X to its ith term.
and prove that these inverse images are nonempty and have the FIP. Let i1, ..., iN be a finite collection of indices in I. Then the finite product Ai1 × ... × AiN
is nonempty (only finitely many choices here, so no AC needed!); it merely consists of N-tuples. Let a = (a1, ..., aN) be such an N-tuple. We "extend" a to the whole index set: take a to the function f defined by f(j) = ak if j = ik, and f(j) = j otherwise. This step is where the addition of the extra point to each space is crucial (we didn't go through all that trouble for nothing!), for it allows us to define f for everything outside of the N-tuple in a precise way without choices (we can already "choose," by construction, j from Xj ). πik(f) = ak is obviously an element of each Aik so that f is in each inverse image; thus we have
By the FIP definition of compactness, the entire intersection over I must be nonempty, and we are done.