michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/standard): add inhabited_exists theorem

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-13 00:24:58 +01:00
parent 0bd943574e
commit ea2fffc260
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
library/standard/logic.lean
View file

@ -218,3 +218,6 @@ theorem inhabited_Bool [instance] : inhabited Bool
theorem inhabited_fun [instance] (A : Type) {B : Type} (H : inhabited B) : inhabited (A → B)
:= inhabited_elim H (take (b : B), inhabited_intro (λ a : A, b))
theorem inhabited_exists {A : Type} {P : A → Bool} (H : ∃ x, P x) : inhabited A
:= obtain w Hw, from H, inhabited_intro w