src/ZF/AC/AC_Equiv.thy

--- a/src/ZF/AC/AC_Equiv.thy	Wed Aug 27 18:22:34 2003 +0200
+++ b/src/ZF/AC/AC_Equiv.thy	Thu Aug 28 01:56:40 2003 +0200
@@ -41,7 +41,7 @@
     "WO7 == \<forall>A. Finite(A) <-> (\<forall>R. well_ord(A,R) --> well_ord(A,converse(R)))"
 
   WO8 :: o
-    "WO8 == \<forall>A. (\<exists>f. f \<in> (\<Pi>X \<in> A. X)) --> (\<exists>R. well_ord(A,R))"
+    "WO8 == \<forall>A. (\<exists>f. f \<in> (\<Pi> X \<in> A. X)) --> (\<exists>R. well_ord(A,R))"
 
 
 (* Auxiliary concepts needed below *)
@@ -54,28 +54,28 @@
 
 (* Axioms of Choice *)  
   AC0 :: o
-    "AC0 == \<forall>A. \<exists>f. f \<in> (\<Pi>X \<in> Pow(A)-{0}. X)"
+    "AC0 == \<forall>A. \<exists>f. f \<in> (\<Pi> X \<in> Pow(A)-{0}. X)"
 
   AC1 :: o
-    "AC1 == \<forall>A. 0\<notin>A --> (\<exists>f. f \<in> (\<Pi>X \<in> A. X))"
+    "AC1 == \<forall>A. 0\<notin>A --> (\<exists>f. f \<in> (\<Pi> X \<in> A. X))"
 
   AC2 :: o
     "AC2 == \<forall>A. 0\<notin>A & pairwise_disjoint(A)   
 		   --> (\<exists>C. \<forall>B \<in> A. \<exists>y. B Int C = {y})"
   AC3 :: o
-    "AC3 == \<forall>A B. \<forall>f \<in> A->B. \<exists>g. g \<in> (\<Pi>x \<in> {a \<in> A. f`a\<noteq>0}. f`x)"
+    "AC3 == \<forall>A B. \<forall>f \<in> A->B. \<exists>g. g \<in> (\<Pi> x \<in> {a \<in> A. f`a\<noteq>0}. f`x)"
 
   AC4 :: o
-    "AC4 == \<forall>R A B. (R \<subseteq> A*B --> (\<exists>f. f \<in> (\<Pi>x \<in> domain(R). R``{x})))"
+    "AC4 == \<forall>R A B. (R \<subseteq> A*B --> (\<exists>f. f \<in> (\<Pi> x \<in> domain(R). R``{x})))"
 
   AC5 :: o
     "AC5 == \<forall>A B. \<forall>f \<in> A->B. \<exists>g \<in> range(f)->A. \<forall>x \<in> domain(g). f`(g`x) = x"
 
   AC6 :: o
-    "AC6 == \<forall>A. 0\<notin>A --> (\<Pi>B \<in> A. B)\<noteq>0"
+    "AC6 == \<forall>A. 0\<notin>A --> (\<Pi> B \<in> A. B)\<noteq>0"
 
   AC7 :: o
-    "AC7 == \<forall>A. 0\<notin>A & (\<forall>B1 \<in> A. \<forall>B2 \<in> A. B1\<approx>B2) --> (\<Pi>B \<in> A. B) \<noteq> 0"
+    "AC7 == \<forall>A. 0\<notin>A & (\<forall>B1 \<in> A. \<forall>B2 \<in> A. B1\<approx>B2) --> (\<Pi> B \<in> A. B) \<noteq> 0"
 
   AC8 :: o
     "AC8 == \<forall>A. (\<forall>B \<in> A. \<exists>B1 B2. B=<B1,B2> & B1\<approx>B2)   
@@ -121,13 +121,13 @@
 locale AC18 =
   assumes AC18: "A\<noteq>0 & (\<forall>a \<in> A. B(a) \<noteq> 0) -->
     ((\<Inter>a \<in> A. \<Union>b \<in> B(a). X(a,b)) =   
-      (\<Union>f \<in> \<Pi>a \<in> A. B(a). \<Inter>a \<in> A. X(a, f`a)))"
+      (\<Union>f \<in> \<Pi> a \<in> A. B(a). \<Inter>a \<in> A. X(a, f`a)))"
   --"AC18 cannot be expressed within the object-logic"
 
 constdefs
   AC19 :: o
     "AC19 == \<forall>A. A\<noteq>0 & 0\<notin>A --> ((\<Inter>a \<in> A. \<Union>b \<in> a. b) =   
-		   (\<Union>f \<in> (\<Pi>B \<in> A. B). \<Inter>a \<in> A. f`a))"
+		   (\<Union>f \<in> (\<Pi> B \<in> A. B). \<Inter>a \<in> A. f`a))"
 
 
 
@@ -194,10 +194,10 @@
 by (blast dest!: well_ord_imp_ex1_first
                     [THEN theI, THEN first_def [THEN def_imp_iff, THEN iffD1]])
 
-lemma ex_choice_fun: "[| well_ord(Union(A), R); 0\<notin>A |] ==> \<exists>f. f:(\<Pi>X \<in> A. X)"
+lemma ex_choice_fun: "[| well_ord(Union(A), R); 0\<notin>A |] ==> \<exists>f. f:(\<Pi> X \<in> A. X)"
 by (fast elim!: first_in_B intro!: lam_type)
 
-lemma ex_choice_fun_Pow: "well_ord(A, R) ==> \<exists>f. f:(\<Pi>X \<in> Pow(A)-{0}. X)"
+lemma ex_choice_fun_Pow: "well_ord(A, R) ==> \<exists>f. f:(\<Pi> X \<in> Pow(A)-{0}. X)"
 by (fast elim!: well_ord_subset [THEN ex_choice_fun])