equal
deleted
inserted
replaced
46 |
46 |
47 lemma AC6_AC7: "AC6 \<Longrightarrow> AC7" |
47 lemma AC6_AC7: "AC6 \<Longrightarrow> AC7" |
48 by (unfold AC6_def AC7_def, blast) |
48 by (unfold AC6_def AC7_def, blast) |
49 |
49 |
50 (* ********************************************************************** *) |
50 (* ********************************************************************** *) |
51 (* AC7 \<Longrightarrow> AC6, Rubin \<and> Rubin p. 12, Theorem 2.8 *) |
51 (* AC7 \<Longrightarrow> AC6, Rubin & Rubin p. 12, Theorem 2.8 *) |
52 (* The case of the empty family of sets added in order to complete *) |
52 (* The case of the empty family of sets added in order to complete *) |
53 (* the proof. *) |
53 (* the proof. *) |
54 (* ********************************************************************** *) |
54 (* ********************************************************************** *) |
55 |
55 |
56 lemma lemma1_1: "y \<in> (\<Prod>B \<in> A. Y*B) \<Longrightarrow> (\<lambda>B \<in> A. snd(y`B)) \<in> (\<Prod>B \<in> A. B)" |
56 lemma lemma1_1: "y \<in> (\<Prod>B \<in> A. Y*B) \<Longrightarrow> (\<lambda>B \<in> A. snd(y`B)) \<in> (\<Prod>B \<in> A. B)" |
102 done |
102 done |
103 |
103 |
104 |
104 |
105 (* ********************************************************************** *) |
105 (* ********************************************************************** *) |
106 (* AC8 \<Longrightarrow> AC9 *) |
106 (* AC8 \<Longrightarrow> AC9 *) |
107 (* - this proof replaces the following two from Rubin \<and> Rubin: *) |
107 (* - this proof replaces the following two from Rubin & Rubin: *) |
108 (* AC8 \<Longrightarrow> AC1 and AC1 \<Longrightarrow> AC9 *) |
108 (* AC8 \<Longrightarrow> AC1 and AC1 \<Longrightarrow> AC9 *) |
109 (* ********************************************************************** *) |
109 (* ********************************************************************** *) |
110 |
110 |
111 lemma AC8_AC9_lemma: |
111 lemma AC8_AC9_lemma: |
112 "\<forall>B1 \<in> A. \<forall>B2 \<in> A. B1 \<approx> B2 |
112 "\<forall>B1 \<in> A. \<forall>B2 \<in> A. B1 \<approx> B2 |
122 |
122 |
123 |
123 |
124 (* ********************************************************************** *) |
124 (* ********************************************************************** *) |
125 (* AC9 \<Longrightarrow> AC1 *) |
125 (* AC9 \<Longrightarrow> AC1 *) |
126 (* The idea of this proof comes from "Equivalents of the Axiom of Choice" *) |
126 (* The idea of this proof comes from "Equivalents of the Axiom of Choice" *) |
127 (* by Rubin \<and> Rubin. But (x * y) is not necessarily equipollent to *) |
127 (* by Rubin & Rubin. But (x * y) is not necessarily equipollent to *) |
128 (* (x * y) \<union> {0} when y is a set of total functions acting from nat to *) |
128 (* (x * y) \<union> {0} when y is a set of total functions acting from nat to *) |
129 (* \<Union>(A) -- therefore we have used the set (y * nat) instead of y. *) |
129 (* \<Union>(A) -- therefore we have used the set (y * nat) instead of y. *) |
130 (* ********************************************************************** *) |
130 (* ********************************************************************** *) |
131 |
131 |
132 lemma snd_lepoll_SigmaI: "b \<in> B \<Longrightarrow> X \<lesssim> B \<times> X" |
132 lemma snd_lepoll_SigmaI: "b \<in> B \<Longrightarrow> X \<lesssim> B \<times> X" |