## $2^{\omega_1}$ separable?

I was rereading an answer to an old question of mine and it included a reference to the fact that $2^{\omega_1}$ was separable. I'm having a hard time finding a reference for this fact, and the proof is not immediately obvious to me. Can anyone provide me with a cite and/or a proof?

-

This is indeed the Hewitt-Marczewski-Pondiczery theorem. My proof, following Engelking, is here. It's in fact not that hard, the fact for a product of copies of 2 point discrete spaces already implies the general theorem pretty quickly.

-

Should have searched a bit harder before asking this one. This is an immediate consequence of the Hewitt-Marczewski-Pondiczery theorem:

Let $m \geq \aleph_0$. If ${X_s : s \in S}$ are topological spaces with $d(X_s) \leq m$ and $|S| \leq 2^m$ then $d(\prod_s X_s) \leq m$.

-
That's overkill, I think. $2^{[0;1]}$ separable is much easier to prove than the Hewitt-Marczewski-Pondiczery Theorem. In fact, the countable system of Walsh functions is dense in $\{-1;1\}^{[0,1)}$ ... mathworld.wolfram.com/WalshFunction.html – Gerald Edgar Apr 3 2010 at 15:47
Interesting. Thanks. – David R. MacIver Apr 3 2010 at 16:03
Of course one also needs $\aleph_1 \le 2^{\aleph_0}$ for this simple proof to work, which is non-constructive (requires Axiom of Choice). Can one prove without choice that $2^{\omega_1}$ is separable? – Gerald Edgar Apr 4 2010 at 18:41
@Gerald: Good question! The statement appears to imply $\aleph_1 \leq 2^{\aleph_0}$. If $\{d_n\}_{n<\omega}$ enumerates a dense subset then the sets $D_\alpha = \{n<\omega: d_n(\alpha) = 1\}$ must be distinct since $D_\alpha\setminus D_\beta$ cannot be empty when $\alpha \neq \beta$. – François G. Dorais Apr 4 2010 at 19:37
Is it not the case that $\aleph_1 \leq 2^{\aleph_0}$ without the axiom of the choice? I think the following should work: By constructing with transfinite induction we can find $g_\alpha : [0, \alpha) \to \mathbb{Q}$ an injection (using the standard argument that countable ordinals embed in the rationals), and so $f_\alpha : \alpha \to \omega$ a bijection. We now define `$f : \omega_1 \to \{0, 1\}^\omega$ inductively as a diagonalisation of $f(\beta)$ for $\beta < \alpha$, which we can do without AC because we can explicitly count $\alpha$ – David R. MacIver Apr 22 2010 at 8:28
show 1 more comment