:: Cardinal Arithmetics
:: by Grzegorz Bancerek
::
:: Received March 6, 1990
:: Copyright (c) 1990-2016 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];