:: Cardinal Arithmetics :: by Grzegorz Bancerek :: :: Received March 6, 1990 :: Copyright (c) 1990-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies ORDINAL1, CARD_1, FUNCT_1, TARSKI, RELAT_1, XBOOLE_0, ZFMISC_1, MCART_1, FUNCT_2, ORDINAL2, ORDINAL3, FUNCOP_1, SUBSET_1, NUMBERS, ARYTM_3, FINSET_1, XXREAL_0, ARYTM_1, NAT_1, CARD_2, CARD_3, CLASSES1, FINSUB_1; notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, RELAT_1, ORDINAL1, MCART_1, ORDINAL2, ORDINAL3, WELLORD2, CLASSES1, CARD_1, NUMBERS, FUNCT_1, RELSET_1, FUNCT_2, XCMPLX_0, FINSET_1, FINSUB_1, FUNCOP_1, SUBSET_1, XXREAL_0, CARD_3; constructors ENUMSET1, WELLORD2, FUNCOP_1, ORDINAL3, XXREAL_0, XREAL_0, NAT_1, CARD_1, CARD_3, CLASSES1, SETFAM_1, FINSUB_1, FUNCT_4, RELSET_1, DOMAIN_1, XTUPLE_0, NUMBERS; registrations SUBSET_1, ORDINAL1, FINSET_1, XREAL_0, CARD_1, FUNCT_2, ZFMISC_1, XBOOLE_0, RELAT_1, CARD_3, FUNCT_1, FINSUB_1, RELSET_1, XTUPLE_0, NAT_1; requirements NUMERALS, SUBSET, BOOLE, ARITHM, REAL; begin reserve A,B for Ordinal, K,M,N for Cardinal, x,x1,x2,y,y1,y2,z,u for object,X,Y,Z,X1,X2, Y1,Y2 for set, f,g for Function; theorem :: CARD_2:1 x in X & X,Y are_equipotent implies Y <> {} & ex x st x in Y; theorem :: CARD_2:2 bool X,bool card X are_equipotent & card bool X = card bool card X; theorem :: CARD_2:3 Z in Funcs(X,Y) implies Z,X are_equipotent & card Z = card X; definition let M,N; func M +` N -> Cardinal equals :: CARD_2:def 1 card( M +^ N); commutativity; func M *` N -> Cardinal equals :: CARD_2:def 2 card [:M,N:]; commutativity; func exp(M,N) -> Cardinal equals :: CARD_2:def 3 card Funcs(N,M); end; theorem :: CARD_2:4 [:X,Y:],[:Y,X:] are_equipotent & card [:X,Y:] = card [:Y,X:]; theorem :: CARD_2:5 [:[:X,Y:],Z:],[:X,[:Y,Z:]:] are_equipotent & card [:[:X,Y:],Z:] = card [:X,[:Y,Z:]:]; ::$CT theorem :: CARD_2:7 [:X,Y:],[:card X,Y:] are_equipotent & [:X,Y:],[:X,card Y:] are_equipotent & [:X,Y:],[:card X,card Y:] are_equipotent & card [:X,Y:] = card [:card X,Y:] & card [:X,Y:] = card [:X,card Y:] & card [:X,Y:] = card [:card X, card Y:]; theorem :: CARD_2:8 X1,Y1 are_equipotent & X2,Y2 are_equipotent implies [:X1,X2:],[: Y1,Y2:] are_equipotent & card [:X1,X2:] = card [:Y1,Y2:]; theorem :: CARD_2:9 x1 <> x2 implies A+^B,[:A,{x1}:] \/ [:B,{x2}:] are_equipotent & card(A +^B) = card([:A,{x1}:] \/ [:B,{x2}:]); theorem :: CARD_2:10 x1 <> x2 implies K+`M,[:K,{x1}:] \/ [:M,{x2}:] are_equipotent & K+`M = card([:K,{x1}:] \/ [:M,{x2}:]); theorem :: CARD_2:11 A*^B,[:A,B:] are_equipotent & card(A*^B) = card [:A,B:]; theorem :: CARD_2:12 X1,Y1 are_equipotent & X2,Y2 are_equipotent & x1 <> x2 & y1 <> y2 implies [:X1,{x1}:] \/ [:X2,{x2}:],[:Y1,{y1}:] \/ [:Y2,{y2}:] are_equipotent & card ([:X1,{x1}:] \/ [:X2,{x2}:]) = card ([:Y1,{y1}:] \/ [:Y2,{y2}:]); theorem :: CARD_2:13 card(A+^B) = card A +` card B; theorem :: CARD_2:14 card(A*^B) = card A *` card B; theorem :: CARD_2:15 [:X,{0}:] \/ [:Y,{1}:],[:Y,{0}:] \/ [:X,{1}:] are_equipotent & card([: X,{0}:] \/ [:Y,{1}:]) = card([:Y,{0}:] \/ [:X,{1}:]); theorem :: CARD_2:16 [:X1,X2:] \/ [:Y1,Y2:],[:X2,X1:] \/ [:Y2,Y1:] are_equipotent & card ([:X1,X2:] \/ [:Y1,Y2:]) = card ([:X2,X1:] \/ [:Y2,Y1:]); theorem :: CARD_2:17 x <> y implies card X +` card Y = card([:X,{x}:] \/ [:Y,{y}:]); theorem :: CARD_2:18 M+`0 = M; theorem :: CARD_2:19 (K+`M)+`N = K+`(M+`N); theorem :: CARD_2:20 K*`0 = 0; theorem :: CARD_2:21 K*`1 = K; theorem :: CARD_2:22 (K*`M)*`N = K*`(M*`N); theorem :: CARD_2:23 2*`K = K+`K; theorem :: CARD_2:24 K*`(M+`N) = K*`M +` K*`N; theorem :: CARD_2:25 exp(K,0) = 1; theorem :: CARD_2:26 K <> 0 implies exp(0,K) = 0; theorem :: CARD_2:27 exp(K,1) = K & exp(1,K) = 1; theorem :: CARD_2:28 exp(K,M+`N) = exp(K,M)*`exp(K,N); theorem :: CARD_2:29 exp(K*`M,N) = exp(K,N)*`exp(M,N); theorem :: CARD_2:30 exp(K,M*`N) = exp(exp(K,M),N); ::$N The Number of Subsets of a Set theorem :: CARD_2:31 exp(2,card X) = card bool X; theorem :: CARD_2:32 exp(K,2) = K*`K; theorem :: CARD_2:33 exp(K+`M,2) = K*`K +` 2*`K*`M +` M*`M; theorem :: CARD_2:34 card(X \/ Y) c= card X +` card Y; theorem :: CARD_2:35 X misses Y implies card (X \/ Y) = card X +` card Y; reserve m,n for Nat; theorem :: CARD_2:36 n+m = n +^ m; theorem :: CARD_2:37 n*m = n *^ m; theorem :: CARD_2:38 card(n+m) = card n +` card m; theorem :: CARD_2:39 card(n*m) = card n *` card m; theorem :: CARD_2:40 for X,Y being finite set st X misses Y holds card (X \/ Y) = card X + card Y; theorem :: CARD_2:41 for X being finite set st not x in X holds card (X \/ {x}) = card X + 1; theorem :: CARD_2:42 for X being set holds card X = 1 iff ex x being object st X = {x}; theorem :: CARD_2:43 for X,Y being finite set holds card(X \/ Y) <= card X + card Y; theorem :: CARD_2:44 for X,Y being finite set st Y c= X holds card (X \ Y) = card X - card Y; theorem :: CARD_2:45 for X,Y being finite set holds card (X \/ Y) = card X + card Y - card (X /\ Y); theorem :: CARD_2:46 for X,Y being finite set holds card [:X,Y:] = card X * card Y; theorem :: CARD_2:47 :: GRAPH_5:1, AK, 21.02.2006 for f being finite Function holds card rng f <= card dom f; theorem :: CARD_2:48 for X,Y being finite set st X c< Y holds card X < card Y & card X in Segm card Y; theorem :: CARD_2:49 (card X c= card Y or card X in card Y) & Y is finite implies X is finite; reserve x1,x2,x3,x4,x5,x6,x7,x8 for object; theorem :: CARD_2:50 card {x1,x2} <= 2; theorem :: CARD_2:51 card {x1,x2,x3} <= 3; theorem :: CARD_2:52 card {x1,x2,x3,x4} <= 4; theorem :: CARD_2:53 card {x1,x2,x3,x4,x5} <= 5; theorem :: CARD_2:54 card {x1,x2,x3,x4,x5,x6} <= 6; theorem :: CARD_2:55 card {x1,x2,x3,x4,x5,x6,x7} <= 7; theorem :: CARD_2:56 card {x1,x2,x3,x4,x5,x6,x7,x8} <= 8; theorem :: CARD_2:57 x1 <> x2 implies card {x1,x2} = 2; theorem :: CARD_2:58 x1 <> x2 & x1 <> x3 & x2 <> x3 implies card {x1,x2,x3} = 3; theorem :: CARD_2:59 x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 implies card {x1,x2,x3,x4} = 4; begin :: Addenda :: from GROUP_3 theorem :: CARD_2:60 for X being set st card X = 2 ex x,y being object st x <> y & X = {x,y}; :: from YELLOW_6, 2004.07.25 theorem :: CARD_2:61 for f being Function holds card rng f c= card dom f; theorem :: CARD_2:62 Z <> {} & Z is finite & (for X,Y st X in Z & Y in Z holds X c= Y or Y c= X) implies union Z in Z; theorem :: CARD_2:63 x1,x2,x3,x4,x5 are_mutually_distinct implies card {x1,x2,x3,x4,x5} = 5; :: from MATRIX_1, 2007.07.22, A.T, generalized theorem :: CARD_2:64 for M1, M2 being set st card M1 = 0 & card M2 = 0 holds M1 = M2; :: missing, 2007.06.14, A.T. registration let x,y; cluster [x,y] -> non natural; end; begin :: from CARD_3, 2011.04.16, A.T. reserve A,B,C for Ordinal, K,L,M,N for Cardinal, x,y,y1,y2,z,u for object,X,Y,Z,Z1,Z2 for set, n for Nat, f,f1,g,h for Function, Q,R for Relation; theorem :: CARD_2:65 Sum(M --> N) = M*`N; theorem :: CARD_2:66 Product(N --> M) = exp(M,N); scheme :: CARD_2:sch 1 FinRegularity { X()->finite set, P[object,object] }: ex x st x in X() & for y st y in X() & y <> x holds not P[y,x] provided X() <> {} and for x,y st P[x,y] & P[y,x] holds x = y and for x,y,z st P[x,y] & P[y,z] holds P[x,z]; scheme :: CARD_2:sch 2 MaxFinSetElem { X()->finite set, P[object,object] }: ex x st x in X() & for y st y in X() holds P[x,y] provided X() <> {} and for x,y holds P[x,y] or P[y,x] and for x,y,z st P[x,y] & P[y,z] holds P[x,z]; theorem :: CARD_2:67 Rank n is finite; theorem :: CARD_2:68 0 in M iff 1 c= M; theorem :: CARD_2:69 1 in M iff 2 c= M; reserve n,k for Nat; theorem :: CARD_2:70 A is limit_ordinal iff for B,n st B in A holds B+^ n in A; theorem :: CARD_2:71 A+^succ n = succ A +^ n & A +^ (n+1) = succ A +^ n; theorem :: CARD_2:72 ex n st A*^succ 1 = A +^ n; theorem :: CARD_2:73 A is limit_ordinal implies A *^ succ 1 = A; theorem :: CARD_2:74 omega c= A implies 1+^A = A; registration cluster infinite -> limit_ordinal for Cardinal; end; theorem :: CARD_2:75 not M is finite implies M+`M = M; theorem :: CARD_2:76 not M is finite & (N c= M or N in M) implies M+`N = M & N+`M = M; theorem :: CARD_2:77 not X is finite & (X,Y are_equipotent or Y,X are_equipotent) implies X \/ Y,X are_equipotent & card (X \/ Y) = card X; theorem :: CARD_2:78 not X is finite & Y is finite implies X \/ Y,X are_equipotent & card (X \/ Y) = card X; theorem :: CARD_2:79 not X is finite & (card Y in card X or card Y c= card X) implies X \/ Y,X are_equipotent & card (X \/ Y) = card X; registration let M,N be finite Cardinal; cluster M+`N -> finite; end; theorem :: CARD_2:80 for M,N being finite Cardinal holds M+`N is finite; theorem :: CARD_2:81 not M is finite implies not M+`N is finite & not N+`M is finite; theorem :: CARD_2:82 for M,N being finite Cardinal holds M*`N is finite; theorem :: CARD_2:83 K in L & M in N or K c= L & M in N or K in L & M c= N or K c= L & M c= N implies K+`M c= L+`N & M+`K c= L+`N; theorem :: CARD_2:84 M in N or M c= N implies K+`M c= K+`N & K+`M c= N+`K & M+`K c= K+`N & M+`K c= N+`K; theorem :: CARD_2:85 X is countable & Y is countable implies X \/ Y is countable; theorem :: CARD_2:86 (card dom f c= M & for x st x in dom f holds card (f.x) c= N) implies card Union f c= M*`N; theorem :: CARD_2:87 (card X c= M & for Y st Y in X holds card Y c= N) implies card union X c= M*`N; theorem :: CARD_2:88 for f st dom f is finite & for x st x in dom f holds f.x is finite holds Union f is finite; theorem :: CARD_2:89 (omega)*`(card n) c= omega & (card n)*`(omega) c= omega; theorem :: CARD_2:90 K in L & M in N or K c= L & M in N or K in L & M c= N or K c= L & M c= N implies K*`M c= L*`N & M*`K c= L*`N; theorem :: CARD_2:91 M in N or M c= N implies K*`M c= K*`N & K*`M c= N*`K & M*`K c= K*`N & M*`K c= N*`K; theorem :: CARD_2:92 K in L & M in N or K c= L & M in N or K in L & M c= N or K c= L & M c= N implies K = 0 or exp(K,M) c= exp(L,N); theorem :: CARD_2:93 M in N or M c= N implies K = 0 or exp(K,M) c= exp(K,N) & exp(M,K) c= exp(N,K); theorem :: CARD_2:94 M c= M+`N & N c= M+`N; theorem :: CARD_2:95 N <> 0 implies M c= M*`N & M c= N*`M; theorem :: CARD_2:96 K in L & M in N implies K+`M in L+`N & M+`K in L+`N; theorem :: CARD_2:97 K+`M in K+`N implies M in N; theorem :: CARD_2:98 card X +` card Y = card X & card Y in card X implies card (X \ Y) = card X; theorem :: CARD_2:99 K*`M in K*`N implies M in N; theorem :: CARD_2:100 X is countable & Y is countable implies X \+\ Y is countable; registration let A be finite set, B be set, f be Function of A, Fin B; cluster Union f -> finite; end; registration let f be finite finite-yielding Function; cluster product f -> finite; end; ::from COMPL_SP, 2011.07.30, A.T. theorem :: CARD_2:101 for F be Function st dom F is infinite & rng F is finite ex x st x in rng F & F"{x} is infinite; :: from PRE_POLY, CARD_FIN etc., 2012.06.27, A.T. theorem :: CARD_2:102 for X,Y being finite set st X c= Y & card X=card Y holds X=Y; scheme :: CARD_2:sch 3 { X()->finite set, P[object,object] }: ex x being set st x in X() & for y being set st y in X() & y <> x holds not P[y,x] provided X() <> {} and for x,y being set st P[x,y] & P[y,x] holds x = y and for x,y,z being set st P[x,y] & P[y,z] holds P[x,z];