From ea2fffc2609681000eb8927528fd9e1c6433e94f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 13 Jul 2014 00:24:58 +0100 Subject: [PATCH] feat(library/standard): add inhabited_exists theorem Signed-off-by: Leonardo de Moura --- library/standard/logic.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/library/standard/logic.lean b/library/standard/logic.lean index 5f66206894..a3d0b9c26d 100644 --- a/library/standard/logic.lean +++ b/library/standard/logic.lean @@ -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