Description: For a finite set, a choice function exists, without using the axiom of choice. (Contributed by Glauco Siliprandi, 24-Dec-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | choicefi.a | |
|
choicefi.b | |
||
choicefi.n | |
||
Assertion | choicefi | |