src/ZF/AC/AC_Equiv.thy
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 2469 b50b8c0eec01
     1.1 --- a/src/ZF/AC/AC_Equiv.thy	Mon Feb 05 21:33:14 1996 +0100
     1.2 +++ b/src/ZF/AC/AC_Equiv.thy	Tue Feb 06 12:27:17 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	ZF/AC/AC_Equiv.thy
     1.5 +(*  Title:      ZF/AC/AC_Equiv.thy
     1.6      ID:         $Id$
     1.7 -    Author: 	Krzysztof Grabczewski
     1.8 +    Author:     Krzysztof Grabczewski
     1.9  
    1.10  Axioms AC1 -- AC19 come from "Equivalents of the Axiom of Choice, II"
    1.11  by H. Rubin and J.E. Rubin, 1985.
    1.12 @@ -42,18 +42,18 @@
    1.13    WO3_def "WO3 == ALL A. EX a. Ord(a) & (EX b. b <= a & A eqpoll b)"
    1.14  
    1.15    WO4_def "WO4(m) == ALL A. EX a f. Ord(a) & domain(f)=a &   
    1.16 -	             (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m)"
    1.17 +                     (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m)"
    1.18  
    1.19    WO5_def "WO5 == EX m:nat. 1 le m & WO4(m)"
    1.20  
    1.21    WO6_def "WO6 == ALL A. EX m:nat. 1 le m & (EX a f. Ord(a) & domain(f)=a   
    1.22 -	            & (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m))"
    1.23 +                    & (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m))"
    1.24  
    1.25    WO7_def "WO7 == ALL A. Finite(A) <-> (ALL R. well_ord(A,R) -->   
    1.26 -	            well_ord(A,converse(R)))"
    1.27 +                    well_ord(A,converse(R)))"
    1.28  
    1.29    WO8_def "WO8 == ALL A. (EX f. f : (PROD X:A. X)) -->  
    1.30 -	            (EX R. well_ord(A,R))"
    1.31 +                    (EX R. well_ord(A,R))"
    1.32  
    1.33  (* Axioms of Choice *)  
    1.34  
    1.35 @@ -62,64 +62,64 @@
    1.36    AC1_def "AC1 == ALL A. 0~:A --> (EX f. f:(PROD X:A. X))"
    1.37  
    1.38    AC2_def "AC2 == ALL A. 0~:A & pairwise_disjoint(A)   
    1.39 -	            --> (EX C. ALL B:A. EX y. B Int C = {y})"
    1.40 +                    --> (EX C. ALL B:A. EX y. B Int C = {y})"
    1.41  
    1.42    AC3_def "AC3 == ALL A B. ALL f:A->B. EX g. g:(PROD x:{a:A. f`a~=0}. f`x)"
    1.43  
    1.44    AC4_def "AC4 == ALL R A B. (R<=A*B --> (EX f. f:(PROD x:domain(R). R``{x})))"
    1.45  
    1.46    AC5_def "AC5 == ALL A B. ALL f:A->B. EX g:range(f)->A.   
    1.47 -	            ALL x:domain(g). f`(g`x) = x"
    1.48 +                    ALL x:domain(g). f`(g`x) = x"
    1.49  
    1.50    AC6_def "AC6 == ALL A. 0~:A --> (PROD B:A. B)~=0"
    1.51  
    1.52    AC7_def "AC7 == ALL A. 0~:A & (ALL B1:A. ALL B2:A. B1 eqpoll B2)   
    1.53 -	            --> (PROD B:A. B)~=0"
    1.54 +                    --> (PROD B:A. B)~=0"
    1.55  
    1.56    AC8_def "AC8 == ALL A. (ALL B:A. EX B1 B2. B=<B1,B2> & B1 eqpoll B2)   
    1.57 -	            --> (EX f. ALL B:A. f`B : bij(fst(B),snd(B)))"
    1.58 +                    --> (EX f. ALL B:A. f`B : bij(fst(B),snd(B)))"
    1.59  
    1.60    AC9_def "AC9 == ALL A. (ALL B1:A. ALL B2:A. B1 eqpoll B2) -->   
    1.61 -	            (EX f. ALL B1:A. ALL B2:A. f`<B1,B2> : bij(B1,B2))"
    1.62 +                    (EX f. ALL B1:A. ALL B2:A. f`<B1,B2> : bij(B1,B2))"
    1.63  
    1.64    AC10_def "AC10(n) ==  ALL A. (ALL B:A. ~Finite(B)) -->   
    1.65 -	            (EX f. ALL B:A. (pairwise_disjoint(f`B) &   
    1.66 -	            sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B))"
    1.67 +                    (EX f. ALL B:A. (pairwise_disjoint(f`B) &   
    1.68 +                    sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B))"
    1.69  
    1.70    AC11_def "AC11 == EX n:nat. 1 le n & AC10(n)"
    1.71  
    1.72    AC12_def "AC12 == ALL A. (ALL B:A. ~Finite(B)) -->   
    1.73 -	    (EX n:nat. 1 le n & (EX f. ALL B:A. (pairwise_disjoint(f`B) &   
    1.74 -	    sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B)))"
    1.75 +            (EX n:nat. 1 le n & (EX f. ALL B:A. (pairwise_disjoint(f`B) &   
    1.76 +            sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B)))"
    1.77  
    1.78    AC13_def "AC13(m) == ALL A. 0~:A --> (EX f. ALL B:A. f`B~=0 &   
    1.79 -	                                  f`B <= B & f`B lepoll m)"
    1.80 +                                          f`B <= B & f`B lepoll m)"
    1.81  
    1.82    AC14_def "AC14 == EX m:nat. 1 le m & AC13(m)"
    1.83  
    1.84    AC15_def "AC15 == ALL A. 0~:A --> (EX m:nat. 1 le m & (EX f. ALL B:A.   
    1.85 -	                              f`B~=0 & f`B <= B & f`B lepoll m))"
    1.86 +                                      f`B~=0 & f`B <= B & f`B lepoll m))"
    1.87  
    1.88    AC16_def "AC16(n, k)  == ALL A. ~Finite(A) -->   
    1.89 -	    (EX T. T <= {X:Pow(A). X eqpoll succ(n)} &   
    1.90 -	    (ALL X:{X:Pow(A). X eqpoll succ(k)}. EX! Y. Y:T & X <= Y))"
    1.91 +            (EX T. T <= {X:Pow(A). X eqpoll succ(n)} &   
    1.92 +            (ALL X:{X:Pow(A). X eqpoll succ(k)}. EX! Y. Y:T & X <= Y))"
    1.93  
    1.94    AC17_def "AC17 == ALL A. ALL g: (Pow(A)-{0} -> A) -> Pow(A)-{0}.   
    1.95 -	            EX f: Pow(A)-{0} -> A. f`(g`f) : g`f"
    1.96 +                    EX f: Pow(A)-{0} -> A. f`(g`f) : g`f"
    1.97  
    1.98    AC18_def "AC18 == (!!X A B. A~=0 & (ALL a:A. B(a) ~= 0) -->   
    1.99                   ((INT a:A. UN b:B(a). X(a,b)) =   
   1.100                   (UN f: PROD a:A. B(a). INT a:A. X(a, f`a))))"
   1.101  
   1.102    AC19_def "AC19 == ALL A. A~=0 & 0~:A --> ((INT a:A. UN b:a. b) =   
   1.103 -	            (UN f:(PROD B:A. B). INT a:A. f`a))"
   1.104 +                    (UN f:(PROD B:A. B). INT a:A. f`a))"
   1.105  
   1.106  (* Auxiliary definitions used in the above definitions *)
   1.107  
   1.108    pairwise_disjoint_def    "pairwise_disjoint(A)   
   1.109 -			    == ALL A1:A. ALL A2:A. A1 Int A2 ~= 0 --> A1=A2"
   1.110 +                            == ALL A1:A. ALL A2:A. A1 Int A2 ~= 0 --> A1=A2"
   1.111  
   1.112    sets_of_size_between_def "sets_of_size_between(A,m,n)   
   1.113 -			    == ALL B:A. m lepoll B & B lepoll n"
   1.114 +                            == ALL B:A. m lepoll B & B lepoll n"
   1.115    
   1.116  end