2 Added a paragraph on $\sigma$-centeredness vs separability.

I just wanted to point out how Andreas' proof above relates to the separability of products of $2^{\aleph_0}$ separable spaces:

Let $\lambda<(2^{\aleph_0})^+$. Suppose $\langle X_\alpha:\alpha<\lambda\rangle$ is a family of separable spaces. For each $\alpha<\lambda$ let $\langle x_\alpha^n:n\in\omega\rangle$ enumerate a dense subset of $X_\alpha$. Let $F:\lambda\times\omega\to\omega$ be as in Andreas' proof. Now the set of sequences of the form $\langle x_{\alpha}^{F(\alpha,n)}:{\alpha<\lambda}\rangle$, $n\in\omega$, is dense in $\prod_{\alpha<\lambda}X_\alpha$.

Also note that $\sigma$-centeredness of a forcing notion $\mathbb P$ corresponds to the separability of the Stone space of the completion of $\mathbb P$. However, I don't know whether it is possible to deduce the $\sigma$-centeredness of short finite support iterations of $\sigma$-centered forcing notions directly from the separability of small product of separable spaces.

1

I just wanted to point out how Andreas' proof above relates to the separability of products of $2^{\aleph_0}$ separable spaces:

Let $\lambda<(2^{\aleph_0})^+$. Suppose $\langle X_\alpha:\alpha<\lambda\rangle$ is a family of separable spaces. For each $\alpha<\lambda$ let $\langle x_\alpha^n:n\in\omega\rangle$ enumerate a dense subset of $X_\alpha$. Let $F:\lambda\times\omega\to\omega$ be as in Andreas' proof. Now the set of sequences of the form $\langle x_{\alpha}^{F(\alpha,n)}:{\alpha<\lambda}\rangle$, $n\in\omega$, is dense in $\prod_{\alpha<\lambda}X_\alpha$.