equal
deleted
inserted
replaced
3 Author: Krzysztof Grabczewski |
3 Author: Krzysztof Grabczewski |
4 |
4 |
5 The proofs concerning the Axiom of Dependent Choice |
5 The proofs concerning the Axiom of Dependent Choice |
6 *) |
6 *) |
7 |
7 |
8 theory DC = AC_Equiv + Hartog + Cardinal_aux: |
8 theory DC imports AC_Equiv Hartog Cardinal_aux begin |
9 |
9 |
10 lemma RepFun_lepoll: "Ord(a) ==> {P(b). b \<in> a} \<lesssim> a" |
10 lemma RepFun_lepoll: "Ord(a) ==> {P(b). b \<in> a} \<lesssim> a" |
11 apply (unfold lepoll_def) |
11 apply (unfold lepoll_def) |
12 apply (rule_tac x = "\<lambda>z \<in> RepFun (a,P) . LEAST i. z=P (i) " in exI) |
12 apply (rule_tac x = "\<lambda>z \<in> RepFun (a,P) . LEAST i. z=P (i) " in exI) |
13 apply (rule_tac d="%z. P (z)" in lam_injective) |
13 apply (rule_tac d="%z. P (z)" in lam_injective) |