Given a set , a choice function for chooses an element of every subset of , except for the empty subset, of course.
Let be a set. Let be the collection of inhabited subsets of . (So if is the power set of , then is contained in , and .)
A choice function for is a function from to such that (for every inhabited subset ).
is a choice set if it has a choice function. (The choice function need not be unique, and rarely is.)
The axiom of choice states that every set has a choice function.
In any topos, the definition above can be internalised; we get the notion of a choice morphism.
Created on November 19, 2010 18:15:29
by Toby Bartels