From abee75c5e99b07071dd8760617325ce2f3741515 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Mon, 29 Sep 2014 12:54:40 -0400 Subject: [PATCH] feat(quantifiers.lean): change exists_unique to a constructively stronger formulation the previous formulation was constructively probably to weak to be useful --- library/logic/quantifiers.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/library/logic/quantifiers.lean b/library/logic/quantifiers.lean index 605a87cf5..dd77e4a82 100644 --- a/library/logic/quantifiers.lean +++ b/library/logic/quantifiers.lean @@ -28,15 +28,15 @@ assume H1 : ∃x, ¬p x, absurd (H2 w) Hw definition exists_unique {A : Type} (p : A → Prop) := -∃x, p x ∧ ∀y, y ≠ x → ¬p y +∃x, p x ∧ ∀y, p y → y = x notation `∃!` binders `,` r:(scoped P, exists_unique P) := r -theorem exists_unique_intro {A : Type} {p : A → Prop} (w : A) (H1 : p w) (H2 : ∀y, y ≠ w → ¬p y) : ∃!x, p x := +theorem exists_unique_intro {A : Type} {p : A → Prop} (w : A) (H1 : p w) (H2 : ∀y, p y → y = w) : ∃!x, p x := exists_intro w (and.intro H1 H2) theorem exists_unique_elim {A : Type} {p : A → Prop} {b : Prop} - (H2 : ∃!x, p x) (H1 : ∀x, p x → (∀y, y ≠ x → ¬p y) → b) : b := + (H2 : ∃!x, p x) (H1 : ∀x, p x → (∀y, p y → y = x) → b) : b := obtain w Hw, from H2, H1 w (and.elim_left Hw) (and.elim_right Hw)