From 7529ee0a5ce81d14795455cf019a91dd29e00e5c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 16 Apr 2015 12:36:27 -0700 Subject: [PATCH] feat(library/data/countable): prove axiom of choice and skolem theorem for countable types and decidable relations --- library/data/countable.lean | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/library/data/countable.lean b/library/data/countable.lean index da685edf9..5453e72f4 100644 --- a/library/data/countable.lean +++ b/library/data/countable.lean @@ -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) := 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