Closure in a topological product: is AC needed? I'm working on a proof of $\prod_{\alpha\in\Lambda}\overline{A_\alpha}=\overline{\prod_{\alpha\in\Lambda}A_\alpha}$ in the product topology. This has been asked before, i.e. Closure in a product of topological spaces, The closure of a product is the product of closures? but they aren't explicit on the parts which are giving me trouble.
If $(C_\alpha)_{\alpha\in\Lambda}$ is a collection of closed sets, the product $\prod_{\alpha\in\Lambda}C_\alpha$ can be written as $\bigcap_{\alpha\in\Lambda}\pi_\alpha^{-1}(C_\alpha)$, and continuity of $\pi_\alpha$ implies $\pi_\alpha^{-1}(C_\alpha)$ is closed, so $\prod_{\alpha\in\Lambda}C_\alpha$ is also closed. Setting $C_\alpha=\overline{A_\alpha}$ this proves $\prod_{\alpha\in\Lambda}\overline{A_\alpha}\supseteq\overline{\prod_{\alpha\in\Lambda}A_\alpha}$.
For the reverse inclusion, suppose $x=(x_\alpha)_{\alpha\in\Lambda}\in\prod_{\alpha\in\Lambda}\overline{A_\alpha}$, and let $U=\prod_{\alpha\in\Lambda}U_\alpha$ be a basic open set containing $x$, with $I\subseteq \Lambda$ finite such that $U_\alpha=X_\alpha$ for $\alpha\notin I$. Since $x_\alpha\in \overline{A_\alpha}\cap U_\alpha$, there is a $y_\alpha\in A_\alpha\cap U_\alpha$, so an application of the axiom of choice would give a $y=(y_\alpha)_{\alpha\in\Lambda}\in$ $\prod_{\alpha\in\Lambda}A_\alpha\cap U$ as desired.
Is AC necessary here? So far I haven't even been able to show that $\prod_{\alpha\in\Lambda}\overline{A_\alpha}\ne\emptyset$ implies $\prod_{\alpha\in\Lambda}A_\alpha\ne\emptyset$, and surely the theorem can't be proven without establishing this.
 A: The theorem is equivalent of the axiom of choice. Suppose the theorem is true. First, we can recover the weak form mentioned at the end:

Theorem: If $\prod_{\alpha\in\Lambda}\overline{A_\alpha}\ne\emptyset$, then $\prod_{\alpha\in\Lambda}A_\alpha \ne\emptyset$.

Proof: If $\prod_{\alpha\in\Lambda}A_\alpha =\emptyset$, then $\prod_{\alpha\in\Lambda}\overline{A_\alpha}=\overline{\prod_{\alpha\in\Lambda}A_\alpha }=\overline{\emptyset}=\emptyset$.
Now let us show that $\forall{\alpha\in\Lambda},A_\alpha\ne\emptyset\implies \prod_{\alpha\in\Lambda}A_\alpha\ne\emptyset$ (where the $A_\alpha$ are just sets, not members of a topological space), which is equivalent to the axiom of choice.
Let $X_\alpha=A_\alpha\sqcup\{a_\alpha\}$ (the disjoint union of $A_\alpha$ and a new point), and topologize $X_\alpha$ using the excluded point topology, in which a set is open iff it is either $X_\alpha$ or a subset of $A_\alpha$. Then given any open set containing $a_\alpha$, the definition of the topology implies that the set must be all of $X_\alpha$, and hence must meet $A_\alpha$ (which we are assuming is non-empty), so $a_\alpha\in\overline{A_\alpha}$ for this topology. Thus $(a_\alpha)_{\alpha\in\Lambda}$ is an element of $\prod_{\alpha\in\Lambda}\overline{A_\alpha}$, and applying the theorem above we get $\prod_{\alpha\in\Lambda}A_\alpha\ne\emptyset$ as desired.
