Choice function

A choice function $𝑓 : 𝑋 ↣ ⋃ 𝑋$ on a set of inhabited sets $𝑋$ is a function which “chooses” an element from each set $𝐴 \in 𝑋$ , #m/def/set i.e.

(\forall 𝐴 \in 𝑋) [𝑓 (𝐴) \in 𝐴]

Within $Z F$ , a choice function cannot be guaranteed unless an explicit rule can be given for choosing elements, e.g. the smallest element of well ordered sets. To guarantee the existence of a choice function for an arbitrary set of inhabited sets, the Axiom of Choice is required.

#state/tidy | #lang/en | #SemBr