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)