Classical reasoning support #
Given that there exists an element satisfying p
, returns one such element.
This is a straightforward consequence of, and equivalent to, Classical.choice
.
See also choose_spec
, which asserts that the returned value has property p
.
Equations
Instances For
Diaconescu's theorem: excluded middle from choice, Function extensionality and propositional extensionality.
Equations
Instances For
Equations
Instances For
Equations
Instances For
the Hilbert epsilon Function
Equations
Instances For
@[reducible]
Extract an element from an existential statement, using Classical.choose
.