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

feat(quantifiers.lean): change exists_unique to a constructively stronger formulation

Browse source 
the previous formulation was constructively probably to weak to be useful
This commit is contained in:
Floris van Doorn 2014-09-29 12:54:40 -04:00 committed by Leonardo de Moura
parent 8947bf4347
commit abee75c5e9
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/logic/quantifiers.lean
View file

@ -28,15 +28,15 @@ assume H1 : ∃x, ¬p x,
absurd (H2 w) Hw absurd (H2 w) Hw
definition exists_unique {A : Type} (p : A → Prop) := 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 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) exists_intro w (and.intro H1 H2)
theorem exists_unique_elim {A : Type} {p : A → Prop} {b : Prop} 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, obtain w Hw, from H2,
H1 w (and.elim_left Hw) (and.elim_right Hw) H1 w (and.elim_left Hw) (and.elim_right Hw)