# product of non-empty set of non-empty sets is non-empty

In this entry, we show that the statement:

(*) the non-empty generalized cartesian product of non-empty sets is non-empty

is equivalent^{} to the axiom of choice^{} (AC).

###### Proposition 1.

AC implies (*).

###### Proof.

Suppose $C=\{{A}_{j}\mid j\in J\}$ is a set of non-empty sets, with $J\ne \mathrm{\varnothing}$. We want to show that

$$B:=\prod _{j\in J}{A}_{j}$$ |

is non-empty. Let $A=\bigcup C$. Then, by AC, there is a function $f:C\to A$ such that $f(X)\in X$ for every $X\in C$. Define $g:J\to A$ by $g(j):=f({A}_{j})$. Then $g\in B$ as a result, $B$ is non-empty. ∎

Remark. The statement that if $J\ne \mathrm{\varnothing}$, then $B\ne \mathrm{\varnothing}$ implies ${A}_{j}\ne \mathrm{\varnothing}$ does not require AC: if $B$ is non-empty, then there is a function $g:J\to A$, and, as $J\ne \mathrm{\varnothing}$, $g\ne \mathrm{\varnothing}$, which means $A\ne \mathrm{\varnothing}$, or that ${A}_{j}\ne \mathrm{\varnothing}$ for some $j\in J$.

###### Proposition 2.

(*) implies AC.

###### Proof.

Suppose $C$ is a set of non-empty sets. If $C$ itself is empty, then the choice function is the empty set^{}. So suppose that $C$ is non-empty. We want to find a (choice) function $f:C\to \bigcup C$, such that $f(x)\in x$ for every $x\in C$. Index elements of $C$ by $C$ itself: ${A}_{x}:=x$ for each $x\in C$. So ${A}_{x}\ne \mathrm{\varnothing}$ by assumption^{}. Hence, by (*), the (non-empty) cartesian product^{} $B$ of the ${A}_{x}$ is non-empty. But an element of $B$ is just a function $f$ whose domain is $C$ and whose codomain is the union of the ${A}_{x}$, or $\bigcup C$, such that $f({A}_{x})\in {A}_{x}$, which is precisely $f(x)\in x$.
∎

Title | product of non-empty set of non-empty sets is non-empty |
---|---|

Canonical name | ProductOfNonemptySetOfNonemptySetsIsNonempty |

Date of creation | 2013-03-22 18:44:28 |

Last modified on | 2013-03-22 18:44:28 |

Owner | CWoo (3771) |

Last modified by | CWoo (3771) |

Numerical id | 7 |

Author | CWoo (3771) |

Entry type | Derivation |

Classification | msc 03E20 |