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

feat(library/logic/axioms/hilbert.lean): add 'some' operator

Browse source
This commit is contained in:
Jeremy Avigad 2015-03-25 17:15:12 -04:00 • committed by Leonardo de Moura
parent 765f6f21f8
commit 8e007b3441
1 changed files with 8 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
library/logic/axioms/hilbert.lean
View file

@ -48,13 +48,18 @@ epsilon_spec_aux (nonempty_of_exists Hex) P Hex
theorem epsilon_singleton {A : Type} (a : A) : @epsilon A (nonempty.intro a) (λx, x = a) = a := theorem epsilon_singleton {A : Type} (a : A) : @epsilon A (nonempty.intro a) (λx, x = a) = a :=
epsilon_spec (exists.intro a (eq.refl a)) epsilon_spec (exists.intro a (eq.refl a))
definition some {A : Type} {P : A → Prop} (H : ∃x, P x) : A :=
@epsilon A (nonempty_of_exists H) P
theorem some_spec {A : Type} {P : A → Prop} (H : ∃x, P x) : P (some H) :=
epsilon_spec H
/- the axiom of choice -/ /- the axiom of choice -/
theorem axiom_of_choice {A : Type} {B : A → Type} {R : Πx, B x → Prop} (H : ∀x, ∃y, R x y) : theorem axiom_of_choice {A : Type} {B : A → Type} {R : Πx, B x → Prop} (H : ∀x, ∃y, R x y) :
∃f, ∀x, R x (f x) := ∃f, ∀x, R x (f x) :=
let f := λx, @epsilon _ (nonempty_of_exists (H x)) (λy, R x y), have H : ∀x, R x (some (H x)), from take x, some_spec (H x),
H := take x, epsilon_spec (H x) exists.intro _ H
in exists.intro f H
theorem skolem {A : Type} {B : A → Type} {P : Πx, B x → Prop} : theorem skolem {A : Type} {B : A → Type} {P : Πx, B x → Prop} :
(∀x, ∃y, P x y) ↔ ∃f, (∀x, P x (f x)) := (∀x, ∃y, P x y) ↔ ∃f, (∀x, P x (f x)) :=