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
```