Theorem (von Neumann's big theorem on algebra maps):
Let be Polish spaces that are part of the outer regular measure spaces and . Suppose that is an algebra map such that for all , there exists an such that . Then there exists and such that and a bijective function such that
for , and
for , , where is any set such that .
Proof: First, we write
where is a nullset and each is closed and of diameter . Then write and . Then we write
where is closed and each has diameter . Then set to be a set such that and its closure.
Continuing this ping-pong game, we obtain nested sequences and dependent on different numbers of indices. Moreover, if we set
then , so that for any given number of indices, the corresponding sequence of nested sets resp. covers almost all of resp. , dependent on whether the number of indices is even or odd. Define and . Then define a function as follows: If , then for any given number of indices there exists one and only one that contains . Moreover,