alignments from lean 3 init.classical
#
theorem
Classical.axiom_of_choice
{α : Sort u}
{β : α → Sort v}
{r : (x : α) → β x → Prop}
(h : ∀ (x : α), ∃ (y : β x), r x y)
:
∃ (f : (x : α) → β x), ∀ (x : α), r x (f x)
Alias of Classical.axiomOfChoice
.
the axiom of choice
Alias of Classical.propComplete
.
Alias of Classical.byCases
.
Alias of Classical.byContradiction
.