If $X$ is a compact metric space, then the set of all sequences in $X$, $X^\mathbb{N}$ is sequentially compact

Since $X$ is a compact metric space, it is sequentially compact so every sequence in $X$ has a subsequence which converges. Now, I want to show that $X^\mathbb{N}$ is sequentially compact, but I'm getting confused because we must show that the sequence of a sequence has a convergent subsequence. I know that we must use the fact that $X$ is sequentially compact. Thanks!

-
Well, $X^N$ is in fact compact (for the reasosonable topology...) – Mariano Suárez-Alvarez Mar 17 '11 at 2:05
This is a direct result of Tychonoff's theorem. – Alex Becker Mar 17 '11 at 2:18
Yes I need to prove that it is compact and I thought it would be easier to prove that it is sequentially compact. The space I am trying to prove is sequentially compact (or compact since we proved it is a metric space) is the set of all sequences in X. I don't think it is the product of space like R^n. Any further explanantions would be appreciated. It is supposed to involve some diagonalization argument – hawaii99 Mar 17 '11 at 2:26
I just reread your comment here and noticed I'd previously overlooked the sentence "I don't think it is the product of space like R^n". The set of all sequences in a space is (isomorphic to) the product of countably many copies of the space. Just like an element of an $n$-fold product is an $n$-tuple, an element of an $\mathbb{N}$-fold product is an $\mathbb{N}$-tuple, i.e. a sequence. – joriki Mar 17 '11 at 17:01

For one, they don't mention that they use the facts that a) the space of sequences in a metric space is metrizable and b) compactness and sequential compactness are equivalent in metrizable spaces. The desired result can only be proved from Tychonoff's theorem using these facts; the product of an uncountable number of compact metric spaces is in general not metrizable and not sequentially compact.

But more importantly, they obscure the set-theoretic premises required for the desired result. Tychonoff's theorem in full generality is equivalent to the axiom of choice. We're only dealing with a countable product here, but I believe Tychonoff's theorem for countable products still requires the boolean prime ideal theorem and the axiom of countable choice (see this article, p. 2). By contrast, the diagonal argument the OP was looking for requires no choice (not even countable choice):

Given a sequence $s$ of sequences in $X$, denote by $s_i(n)$ the $n$-th element of the $i$-th sequence of $s$. (If you tend to get as confused about such things as I do, it helps to keep in mind the concrete example where $s_i(n)$ is the $n$-th digit in the binary representation of $i$.) Consider the sequence $s_i(1)$ in $X$. Since $X$ is a compact metric space and hence sequentially compact, this sequence contains a convergent subsequence $s_{i_1(k)}(1)$. Denote its limit by $a (1)$. Then consider the sequence $s_{i_1(k)}(2)$ (a subsequence of the sequence $s_i(2)$ in $X$). This sequence, too, has a convergent subsequence $s_{i_2(k)}(2)$ with limit $a (2)$. We can continue this construction for all $n$. Now consider $s_{i_l(l)}$, which is a subsequence of the sequence $s$ of sequences. We can show that it converges against the sequence $a$ of the limits $a (n)$.

An element of the basis of the product topology containing $a$ is a product of factors, only a finite number of which differ from $X$. For each $n$, apart from the first $n$ elements the sequence $s_{i_l(l)}(n)$ is a subsequence of $s_{i_n(l)}(n)$, and thus it is a convergent subsequence of $s_i(n)$ with limit $a (n)$, which will eventually end up in the $n$-th factor of the basis element. Since there are finitely many of these factors, eventually all these convergent subsequences will have ended up in their corresponding factors, so that the entire sequence eventually ends up in the given basis element.

[Edit in response to comments by Nate and Theo:]

Here's a construction that picks a particular convergent subsequence of a sequence having at least one convergent subsequence in a metric space without making arbitrary choices (in case Nate and Theo are right that that requires the axiom of choice):

For a given sequence $b_n$, consider the (non-empty) set of all convergent subsequences for which $\lvert b_n - b \rvert < 2^{-n}$ for all $n$, where $b$ is the limit of the subsequence, and take the least of these subsequences in lexicographical order. We can't just take the lexicographically least convergent subsequence because there isn't one, but we can explicitly construct the lexicographically least convergent subsequence that fulfills the given condition: For each element, just pick the earliest element in the sequence such that the resulting partial subsequence is a prefix of at least one subsequence that fulfills the condition. The result is a Cauchy sequence, and hence, since $X$ is compact, converges. (The same construction doesn't work without the additional condition, since the resulting subsequence would just be the sequence itself.)

So it appears that we can avoid choice. However, that would seem to allow us to reason as follows: The fact that all factors in the product are $X$ was not used. Thus, the result generalizes to arbitrary countable products of compact metric spaces. A countable product of metric spaces is metrizable, and in a metrizable space compactness and sequential compactness are equivalent; thus we've proved that the countable product of compact metric spaces is compact. But now we can plug that into the proof of the equivalence of the axiom of choice and Tychonoff's theorem (linked to above). Since to any compact metric space we can add an isolated point and still have a compact metric space (by limiting the metric to $1$ and choosing a uniform distance to the new point $>1$), this seems to prove the possibility of choice from a countable product of compact metric spaces. This is not the full axiom of countable choice, but it does allow considerable choices that I would have expected to be independent of ZF. Is this true, or is there another fallacy somewhere?

-
Ah, but you are using (countable) choice. The sequence $s_{i_l(k)}(l)$ doesn't just contain one convergent subsequence, it contains a lot of them. So you have to choose one. There are infinitely many choices to be made... In fact, if you do your argument with pseudometric spaces instead, it is known to be equivalent to countable choice (this is Form 8AK in Howard and Rubin's web site; see consequences.emich.edu/conseq.htm). – Nate Eldredge Mar 17 '11 at 12:41
@Nate: Thanks for this, I was about to make the exact same point. – t.b. Mar 17 '11 at 12:46
@Nate Eldredge @Theo Buehler: Thanks. Three remarks: a) unless I'm mistaken that Tychonoff's theorem for countable products requires more than countable choice, my point about not using Tychonoff remains valid. b) The equivalence for pseudometric spaces that you cite is a simple modification of the equivalence proof I linked to, since the topology used there is induced by a pseudometric with distance $0$ within $A_i$ and distance $1$ to $x$, but you can't do the same thing for compact metric spaces, since these don't exist for arbitrary cardinalities, so I'm note sure the result is relevant. – joriki Mar 17 '11 at 13:34
@Joriki: if someone has trouble showing that a countable product of compact metric spaces is compact, it is a safe bet that he does not care much about how much choice is needed in order to prove the result---and in fact a discussion about that can most probably confuse more than help. Specially when there is nothing in his question to indicate otherwise! (Usually people that do care about choice are very vocal about it :) ) – Mariano Suárez-Alvarez Mar 17 '11 at 17:05
@Theo Buehler: Thanks for your comment (and the vote :-). But after you said that my claim that I hadn't used choice was flawed, I'd appreciate your opinion as to whether the flaw is now fixed. (Since there seems to be some level of consensus here that these issues shouldn't be discussed in response to this question, I'm thinking of opening a new question to clarify these issues.) – joriki Mar 17 '11 at 23:29