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 equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath to the axiom of choiceMathworldPlanetmath (AC).

Proposition 1.

AC implies (*).


Suppose C={AjjJ} is a set of non-empty sets, with J. We want to show that


is non-empty. Let A=C. Then, by AC, there is a function f:CA such that f(X)X for every XC. Define g:JA by g(j):=f(Aj). Then gB as a result, B is non-empty. ∎

Remark. The statement that if J, then B implies Aj does not require AC: if B is non-empty, then there is a function g:JA, and, as J, g, which means A, or that Aj for some jJ.

Proposition 2.

(*) implies AC.


Suppose C is a set of non-empty sets. If C itself is empty, then the choice function is the empty setMathworldPlanetmath. So suppose that C is non-empty. We want to find a (choice) function f:CC, such that f(x)x for every xC. Index elements of C by C itself: Ax:=x for each xC. So Ax by assumptionPlanetmathPlanetmath. Hence, by (*), the (non-empty) cartesian productMathworldPlanetmath B of the Ax 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 Ax, or C, such that f(Ax)Ax, which is precisely f(x)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