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
- Classical.inhabited_of_nonempty h = { default := Classical.choice h }
Instances For
Equations
- Classical.decidableInhabited a = { default := inferInstance }
Instances For
Equations
- Classical.typeDecidableEq α x✝¹ x✝ = inferInstance
Instances For
Equations
- Classical.typeDecidable α = match Classical.propDecidable (Nonempty α) with | isTrue hp => PSum.inl default | isFalse hn => PSum.inr ⋯
Instances For
the Hilbert epsilon Function
Equations
Instances For
Transfer decidability of ¬ p
to decidability of p
.
Equations
Instances For
@[reducible]
Extract an element from a existential statement, using Classical.choose
.
Equations
- P.choose = Classical.choose P