Tychonoff's theorem
From Academic Kids

In mathematics, Tychonoff's theorem states that the product of any collection of compact topological spaces is compact.
For finite collections of compact spaces, this is not very surprising. The statement is in fact true for infinite collections of arbitrary size; in this case it depends heavily on the particular definition of the product topology and is equivalent to the axiom of choice.
This theorem of Tychonoff has many applications in differential and algebraic topology and in functional analysis, e.g., for the StoneČech compactification or in the proof of the Theorem of BanachAlaoglu. It was published in 1930 by A. Tychonoff.
Sketch of proof
Tychonoff's theorem is complex, and its proof is often approached in parts, proving helpful lemmas first. One approach to proving it exploits an alternative formulation of compactness based on the finite intersection property. We take this approach, which can be found in Munkres, section 37 (see reference). The two lemmas that are shown follow:
 Lemma 1: For any A contained in P(X) (the power set of X) satisfying the finite intersection property (FIP), there is a maximal set D with FIP containing A. By "maximal" we mean that no collection satisfying FIP properly contains D. (Here is where the axiom of choice is used.)
 Lemma 2: If D is a maximal FIPsatisfying subset of P(X), then any finite intersection of elements of D is contained in D, and any subset of X intersecting every element of D is also contained in D.
To actually prove Tychonoff's theorem, we use the definition of compactness based on the FIP, by taking an FIP collection A of sets, and showing that the intersection over closures of elements of A is nonempty. Lemma 1 allows us to choose a maximal collection D containing A, and we now need only show the intersection over closures of elements of D is nonempty.
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.
Another proof uses the Alexander subbase theorem, and yet another proof follows trivially from the properties of nets on product spaces, in particular that a net converges in a product space iff each coordinate converges and the fact that compactness can be expressed in terms of nets.
Tychonoff's theorem and the axiom of choice
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 settheoretic 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!). Nonetheless it has to be mentioned that the full strength of Tychonoff's theorem relies crucially on the fact that it is a statement about all topological spaces. Restricting this to a smaller class can lead to a proper weakening. For example, the Tychnoff theorem for Hausdorff spaces, while not being a theorem of ZF, is equivalent to the Boolean prime ideal theorem  a choice principle strictly weaker than AC.
To prove that Tychonoff's theorem in its general version implies the axiom of choice, we establish that every infinite cartesian product of nonempty 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 {A_{i}} 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 X_{i} to be A_{i} 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 A_{i}, so simply take X_{i} = A_{i} ∪ {i}).
Now the define cartesian product
 <math>X = \prod_{i \in I} X_i<math>
along with the natural projection maps π_{i} which take a member of X to its ith term.
Now here's the trick: we give each X_{i} the topology whose open sets are the cofinite subsets of X_{i}, plus the empty set (the cofinite topology) and the singleton {i}. This makes X_{i} compact, and by Tychonoff's theorem, X is also compact (in the product topology). The projection maps are continuous; all the A_{i}'s are closed, being complements of the singleton open set {i} in X_{i}. So the inverse images π_{i}^{1}(A_{i}) are closed subsets of X. We note that
 <math>\prod_{i \in I} A_i = \bigcap_{i \in I} \pi_i^{1}(A_i) <math>
and prove that these inverse images are nonempty and have the FIP. Let i_{1}, ..., i_{N} be a finite collection of indices in I. Then the finite product A_{i1} × ... × A_{iN} is nonempty (only finitely many choices here, so no AC needed!); it merely consists of Ntuples. Let a = (a_{1}, ..., a_{N}) be such an Ntuple. We "extend" a to the whole index set: take a to the function f defined by f(j) = a_{k} if j = i_{k}, 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 Ntuple in a precise way without choices (we can already "choose," by construction, j from X_{j} ). π_{ik}(f) = a_{k} is obviously an element of each A_{ik} so that f is in each inverse image; thus we have
 <math>\bigcap_{k = 1}^N \pi_{i_k}^{1}(A_{i_k}) \neq \empty.<math>
By the FIP definition of compactness, the entire intersection over I must be nonempty, and we are done.
References
 Munkres, James, Topology, 2nd edition, Prentice Hall, 2000.
 A major general reference.
 Johnstone, Peter T., Stone spaces, Cambridge studies in advanced mathematics 3, Cambridge University Press, 1982.
 Contains some discussions about weaker versions of Tychonoff's theorem, including the abovementioned variant for Hausdorff spaces, and gives further literature.
 Johnstone, Peter T., Tychonoff's theorem without the axiom of choice, Fundamenta Mathematica 113, 2135, 1981.
 Johnstone's proof that Tychonoff's theorem for locales (i.e. in pointless topology) does not need AC.
 Tychonoff, Andrey N., Über die topologische Erweiterung von Räumen. Mathematische Annalen 102, 544561, 1929. Available online from Göttinger DigitalisierungsZentrum (http://134.76.163.65/agora_docs/38446TABLE_OF_CONTENTS.html) (English homepage of the GDZ (http://gdz.sub.unigoettingen.de/en/index.html)) .
 Tychonoff's original paper (in German language).