§ Axiom of Choice and Zorn's Lemma
I have not seen this "style" of proof before of AoC/Zorn's lemma
by thinking of partial functions as monotone functions
§ Zorn's Lemma implies Axiom of Choice
If we are given Zorn's lemma and the set , to build a choice
function, we consider the collection of functions
such that either or . This can be endowed with
a partial order / join semilattice structure using the "flat" lattice, where
for all , and .
For every chain of functions, we have a least upper bound, since a chain
of functions is basically a collection of functions where each function
is "more defined" than .
Hence we can always get a maximal element , which has a value defined
at each . Otherwise, if we have , the element
is not maximal, since it is dominated by a larger function which is defined
Hence, we've constructed a choice function by applying Zorn's Lemma.
Thus, Zorn's Lemma implies Axiom of Choice.