equal
deleted
inserted
replaced
122 |
122 |
123 locale AC18 = |
123 locale AC18 = |
124 assumes AC18: "A\<noteq>0 & (\<forall>a \<in> A. B(a) \<noteq> 0) \<longrightarrow> |
124 assumes AC18: "A\<noteq>0 & (\<forall>a \<in> A. B(a) \<noteq> 0) \<longrightarrow> |
125 ((\<Inter>a \<in> A. \<Union>b \<in> B(a). X(a,b)) = |
125 ((\<Inter>a \<in> A. \<Union>b \<in> B(a). X(a,b)) = |
126 (\<Union>f \<in> \<Prod>a \<in> A. B(a). \<Inter>a \<in> A. X(a, f`a)))" |
126 (\<Union>f \<in> \<Prod>a \<in> A. B(a). \<Inter>a \<in> A. X(a, f`a)))" |
127 \<comment>"AC18 cannot be expressed within the object-logic" |
127 \<comment> \<open>AC18 cannot be expressed within the object-logic\<close> |
128 |
128 |
129 definition |
129 definition |
130 "AC19 == \<forall>A. A\<noteq>0 & 0\<notin>A \<longrightarrow> ((\<Inter>a \<in> A. \<Union>b \<in> a. b) = |
130 "AC19 == \<forall>A. A\<noteq>0 & 0\<notin>A \<longrightarrow> ((\<Inter>a \<in> A. \<Union>b \<in> a. b) = |
131 (\<Union>f \<in> (\<Prod>B \<in> A. B). \<Inter>a \<in> A. f`a))" |
131 (\<Union>f \<in> (\<Prod>B \<in> A. B). \<Inter>a \<in> A. f`a))" |
132 |
132 |