L'axiome du choix est un axiome de la théorie des ensembles qui s'énonce comme suit :
Si X est une famille d'ensembles non vides, il existe une fonction définie sur X, appelée fonction de choix, qui à chaque ensemble A de X associe un élément de cet ensemble A.
Il peut être accepté ou rejeté, selon la théorie axiomatique des ensembles choisie. Il n'est en principe pas admis par les mathématiciens constructivistes.
Version faible:
Etant donnée une famille dénombrable d'ensembles non vides, il existe une fonction qui à chacun d'entre eux associe un de ses éléments.
L'axiome du choix dans la théorie des ensembles de Zermolo-Fraenkel (ZF) est équivalent au lemme de Zorn ou au théorème de Zermolo.
Lemme de Zorn: Si un ensemble ordonné est tel que tout sous-ensemble totalement ordonné possède un majorant, alors il possède un élément maximal.
Théorème de Zermelo: Tout ensemble peut être muni d'une structure de bon ordre, c'est-à-dire d'un ordre tel que toute partie non vide admette un plus petit élément.
L'axiome du choix est utilisé pour montrer qu'un ensemble fini au sens de Dedekind (un ensemble qu'on ne peut mettre en bijection avec aucun de ses sous-ensembles stricts) est fini au sens usuel (est en bijection avec un entier naturel).
Le théorème de la base incomplète en dimension quelconque (et même simplement l'existence d'une base pour tout espace vectoriel) n'est vrai qu'en supposant l'axiome du choix.