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

feat(library/data/countable): prove axiom of choice and skolem theorem for countable types and decidable relations

Browse source
This commit is contained in:
Leonardo de Moura 2015-04-16 12:36:27 -07:00
parent 0dd7667836
commit 7529ee0a5c
1 changed files with 14 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
library/data/countable.lean
View file

@ -300,4 +300,18 @@ assume ex, elt_of (find_a ex)
theorem choose_spec {A : Type} {p : A → Prop} [c : countable A] [d : decidable_pred p] (ex : ∃ x, p x) : p (choose ex) := theorem choose_spec {A : Type} {p : A → Prop} [c : countable A] [d : decidable_pred p] (ex : ∃ x, p x) : p (choose ex) :=
has_property (find_a ex) has_property (find_a ex)
theorem axiom_of_choice {A : Type} {B : A → Type} {R : Π x, B x → Prop} [c : Π a, countable (B a)] [d : ∀ x y, decidable (R x y)]
: (∀x, ∃y, R x y) → ∃f, ∀x, R x (f x) :=
assume H,
have H₁ : ∀x, R x (choose (H x)), from take x, choose_spec (H x),
exists.intro _ H₁
theorem skolem {A : Type} {B : A → Type} {P : Π x, B x → Prop} [c : Π a, countable (B a)] [d : ∀ x y, decidable (P x y)]
: (∀x, ∃y, P x y) ↔ ∃f, (∀x, P x (f x)) :=
iff.intro
(assume H : (∀x, ∃y, P x y), axiom_of_choice H)
(assume H : (∃f, (∀x, P x (f x))),
take x, obtain (fw : ∀x, B x) (Hw : ∀x, P x (fw x)), from H,
exists.intro (fw x) (Hw x))
end countable end countable