nLab choice function

Choice functions

Choice functions


Given a set AA, a choice function for AA chooses an element of every subset of AA, except for the empty subset, of course.


Let AA be a set. Let 𝒫 +A\mathcal{P}^+A be the collection of inhabited subsets of AA. (So if 𝒫A\mathcal{P}A is the power set of AA, then 𝒫 +A\mathcal{P}^+A is contained in 𝒫A\mathcal{P}A, and 𝒫A𝒫 +A={}\mathcal{P}A \setminus \mathcal{P}^+A = \{\empty\}.)

A choice function for AA is a function cc from 𝒫 +A\mathcal{P}^+A to AA such that c(x)xc(x) \in x (for every inhabited subset xx).


AA 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 notions of choice object and choice morphism.

Last revised on April 19, 2024 at 15:23:39. See the history of this page for a list of all contributions to it.