The theorem is named after Andrey Nikolayevich Tikhonov (whose surname sometimes is transcribed Tychonoff), who proved it first in 1930 for powers of the closed unit interval and in 1935 stated the full theorem along with the remark that its proof was the same as for the special case.
The earliest known published proof is contained in a 1935 article by Tychonoff, "Über einen Funktionenraum".
[1] Tychonoff's theorem is often considered as perhaps the single most important result in general topology (along with Urysohn's lemma).
Indeed, the Heine–Borel definition of compactness—that every covering of a space by open sets admits a finite subcovering—is relatively recent.
More popular in the 19th and early 20th centuries was the Bolzano-Weierstrass criterion that every bounded infinite sequence admits a convergent subsequence, now called sequential compactness.
This is a critical failure: if X is a completely regular Hausdorff space, there is a natural embedding from X into [0,1]C(X,[0,1]), where C(X,[0,1]) is the set of continuous maps from X to [0,1].
As a rule of thumb, any sort of construction that takes as input a fairly general object (often of an algebraic, or topological-algebraic nature) and outputs a compact space is likely to use Tychonoff: e.g., the Gelfand space of maximal ideals of a commutative C*-algebra, the Stone space of maximal ideals of a Boolean algebra, and the Berkovich spectrum of a commutative Banach ring.
In his textbook, Munkres gives a reworking of the Cartan–Bourbaki proof that does not explicitly use any filter-theoretic language or preliminaries.
Zorn's lemma is also used to prove Kelley's theorem, that every net has a universal subnet.
In fact these uses of AC are essential: in 1950 Kelley proved that Tychonoff's theorem implies the axiom of choice in ZF.
Indeed, it is not hard to see that it is equivalent to the Boolean prime ideal theorem (BPI), a well-known intermediate point between the axioms of Zermelo-Fraenkel set theory (ZF) and the ZF theory augmented by the axiom of choice (ZFC).
Studying the strength of Tychonoff's theorem for various restricted classes of spaces is an active area in set-theoretic topology.
The analogue of Tychonoff's theorem in pointless topology does not require any form of the axiom of choice.
To prove that Tychonoff's theorem in its general version implies the axiom of choice, we establish that every infinite cartesian product of non-empty sets is nonempty.
Once we have this fact, Tychonoff's theorem can be applied; we then use the finite intersection property (FIP) definition of compactness.
along with the natural projection maps πi which take a member of X to its ith term.
The projection maps are continuous; all the Ai's are closed, being complements of the singleton open set {i} in Xi.
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, 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 ).
By the FIP definition of compactness, the entire intersection over I must be nonempty, and the proof is complete.