Axiom·A09
Choice
A choice function exists for any family of non-empty sets.
In words
For any collection A, if the empty set is not a member of A then there is a function f where for every X, if X belongs to A then f(X) belongs to X.
This is a ZFC axiom: it is assumed, not proven. Everything below it in a proof chain ultimately rests here.
Remarks
Choice: for any collection
of non-empty sets, there is a function selecting one element from each member. Equivalent (with the other axioms) to Zorn's lemma and the general well-ordering theorem (every set admits a well-order) - a considerably stronger statement than T09, which is about
specifically and needs no choice; neither Zorn's lemma nor the general well-ordering theorem is developed in this library yet. Unlike the rest of ZFC it is not constructive and is required for much of cardinal arithmetic, Tychonoff's theorem, and the existence of bases.
Propose an edit3 published revisions