:: Cardinal Arithmetics
:: by Grzegorz Bancerek
::
:: Received March 6, 1990
:: Copyright (c) 1990 Association of Mizar Users
theorem :: CARD_2:1
canceled;
theorem Th2: :: CARD_2:2
theorem :: CARD_2:3
theorem :: CARD_2:4
theorem :: CARD_2:5
theorem :: CARD_2:6
deffunc H1( set ) -> set = $1 `1 ;
theorem :: CARD_2:7
Lm1:
for A, B being Ordinal
for x1, x2 being set st x1 <> x2 holds
( A +^ B,[:A,{x1}:] \/ [:B,{x2}:] are_equipotent & card (A +^ B) = card ([:A,{x1}:] \/ [:B,{x2}:]) )
deffunc H2( set , set ) -> set = [:$1,{0 }:] \/ [:$2,{1}:];
Lm2:
for X, Y being set holds
( [:X,Y:],[:Y,X:] are_equipotent & card [:X,Y:] = card [:Y,X:] )
definition
let M,
N be
Cardinal;
func M +` N -> Cardinal equals :: CARD_2:def 1
card (M +^ N);
coherence
card (M +^ N) is Cardinal
;
commutativity
for b1, M, N being Cardinal st b1 = card (M +^ N) holds
b1 = card (N +^ M)
func M *` N -> Cardinal equals :: CARD_2:def 2
card [:M,N:];
coherence
card [:M,N:] is Cardinal
;
commutativity
for b1, M, N being Cardinal st b1 = card [:M,N:] holds
b1 = card [:N,M:]
by Lm2;
func exp M,
N -> Cardinal equals :: CARD_2:def 3
card (Funcs N,M);
coherence
card (Funcs N,M) is Cardinal
;
end;
:: deftheorem defines +` CARD_2:def 1 :
:: deftheorem defines *` CARD_2:def 2 :
:: deftheorem defines exp CARD_2:def 3 :
theorem :: CARD_2:8
canceled;
theorem :: CARD_2:9
canceled;
theorem :: CARD_2:10
canceled;
theorem :: CARD_2:11
theorem Th12: :: CARD_2:12
for
X,
Y,
Z being
set holds
(
[:[:X,Y:],Z:],
[:X,[:Y,Z:]:] are_equipotent &
card [:[:X,Y:],Z:] = card [:X,[:Y,Z:]:] )
theorem Th13: :: CARD_2:13
Lm3:
for X, Y being set holds [:X,Y:],[:(card X),Y:] are_equipotent
theorem Th14: :: CARD_2:14
for
X,
Y being
set holds
(
[: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 Th15: :: CARD_2:15
for
X1,
Y1,
X2,
Y2 being
set st
X1,
Y1 are_equipotent &
X2,
Y2 are_equipotent holds
(
[:X1,X2:],
[:Y1,Y2:] are_equipotent &
card [:X1,X2:] = card [:Y1,Y2:] )
theorem :: CARD_2:16
theorem Th17: :: CARD_2:17
theorem Th18: :: CARD_2:18
deffunc H3( set , set ) -> set = [:$1,{0 }:] \/ [:$2,{1}:];
deffunc H4( set , set , set , set ) -> set = [:$1,{$3}:] \/ [:$2,{$4}:];
theorem :: CARD_2:19
canceled;
theorem :: CARD_2:20
canceled;
theorem :: CARD_2:21
canceled;
theorem :: CARD_2:22
canceled;
theorem Th23: :: CARD_2:23
for
X1,
Y1,
X2,
Y2,
x1,
x2,
y1,
y2 being
set st
X1,
Y1 are_equipotent &
X2,
Y2 are_equipotent &
x1 <> x2 &
y1 <> y2 holds
(
[:X1,{x1}:] \/ [:X2,{x2}:],
[:Y1,{y1}:] \/ [:Y2,{y2}:] are_equipotent &
card ([:X1,{x1}:] \/ [:X2,{x2}:]) = card ([:Y1,{y1}:] \/ [:Y2,{y2}:]) )
theorem Th24: :: CARD_2:24
theorem Th25: :: CARD_2:25
theorem :: CARD_2:26
for
X,
Y being
set holds
(
[:X,{0 }:] \/ [:Y,{1}:],
[:Y,{0 }:] \/ [:X,{1}:] are_equipotent &
card ([:X,{0 }:] \/ [:Y,{1}:]) = card ([:Y,{0 }:] \/ [:X,{1}:]) )
by Th23;
theorem Th27: :: CARD_2:27
for
X1,
X2,
Y1,
Y2 being
set holds
(
[:X1,X2:] \/ [:Y1,Y2:],
[:X2,X1:] \/ [:Y2,Y1:] are_equipotent &
card ([:X1,X2:] \/ [:Y1,Y2:]) = card ([:X2,X1:] \/ [:Y2,Y1:]) )
theorem Th28: :: CARD_2:28
theorem :: CARD_2:29
Lm4:
for x, y, X, Y being set st x <> y holds
[:X,{x}:] misses [:Y,{y}:]
theorem :: CARD_2:30
canceled;
theorem Th31: :: CARD_2:31
theorem :: CARD_2:32
theorem :: CARD_2:33
theorem :: CARD_2:34
canceled;
theorem Th35: :: CARD_2:35
theorem Th36: :: CARD_2:36
theorem Th37: :: CARD_2:37
theorem :: CARD_2:38
theorem :: CARD_2:39
theorem :: CARD_2:40
theorem :: CARD_2:41
theorem :: CARD_2:42
theorem :: CARD_2:43
theorem :: CARD_2:44
theorem :: CARD_2:45
theorem :: CARD_2:46
theorem Th47: :: CARD_2:47
theorem Th48: :: CARD_2:48
theorem Th49: :: CARD_2:49
theorem Th50: :: CARD_2:50
theorem Th51: :: CARD_2:51
theorem Th52: :: CARD_2:52
theorem Th53: :: CARD_2:53
theorem Th54: :: CARD_2:54
theorem :: CARD_2:55
canceled;
theorem :: CARD_2:56
canceled;
theorem :: CARD_2:57
canceled;
theorem :: CARD_2:58
canceled;
theorem :: CARD_2:59
canceled;
theorem Th60: :: CARD_2:60
theorem :: CARD_2:61
canceled;
theorem Th62: :: CARD_2:62
theorem Th63: :: CARD_2:63
theorem :: CARD_2:64
theorem :: CARD_2:65
theorem :: CARD_2:66
theorem :: CARD_2:67
theorem :: CARD_2:68
theorem Th69: :: CARD_2:69
theorem Th70: :: CARD_2:70
theorem Th71: :: CARD_2:71
for
x1,
x2,
x3,
x4 being
set holds
card {x1,x2,x3,x4} <= 4
theorem Th72: :: CARD_2:72
for
x1,
x2,
x3,
x4,
x5 being
set holds
card {x1,x2,x3,x4,x5} <= 5
theorem Th73: :: CARD_2:73
for
x1,
x2,
x3,
x4,
x5,
x6 being
set holds
card {x1,x2,x3,x4,x5,x6} <= 6
theorem Th74: :: CARD_2:74
for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set holds
card {x1,x2,x3,x4,x5,x6,x7} <= 7
theorem :: CARD_2:75
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 being
set holds
card {x1,x2,x3,x4,x5,x6,x7,x8} <= 8
theorem Th76: :: CARD_2:76
theorem Th77: :: CARD_2:77
for
x1,
x2,
x3 being
set st
x1 <> x2 &
x1 <> x3 &
x2 <> x3 holds
card {x1,x2,x3} = 3
theorem Th78: :: CARD_2:78
for
x1,
x2,
x3,
x4 being
set st
x1 <> x2 &
x1 <> x3 &
x1 <> x4 &
x2 <> x3 &
x2 <> x4 &
x3 <> x4 holds
card {x1,x2,x3,x4} = 4
theorem :: CARD_2:79
theorem :: CARD_2:80
Lm5:
now
let n be
Element of
NAT ;
:: thesis: ( ( for Z being finite set st card Z = n & Z <> {} & ( for X, Y being set st X in Z & Y in Z & not X c= Y holds
Y c= X ) holds
union Z in Z ) implies for Z being finite set st card Z = n + 1 & Z <> {} & ( for X, Y being set st X in Z & Y in Z & not X c= Y holds
Y c= X ) holds
union b3 in b3 )assume A1:
for
Z being
finite set st
card Z = n &
Z <> {} & ( for
X,
Y being
set st
X in Z &
Y in Z & not
X c= Y holds
Y c= X ) holds
union Z in Z
;
:: thesis: for Z being finite set st card Z = n + 1 & Z <> {} & ( for X, Y being set st X in Z & Y in Z & not X c= Y holds
Y c= X ) holds
union b3 in b3let Z be
finite set ;
:: thesis: ( card Z = n + 1 & Z <> {} & ( for X, Y being set st X in Z & Y in Z & not X c= Y holds
Y c= X ) implies union b2 in b2 )assume that A2:
card Z = n + 1
and A3:
Z <> {}
and A4:
for
X,
Y being
set st
X in Z &
Y in Z & not
X c= Y holds
Y c= X
;
:: thesis: union b2 in b2consider y being
Element of
Z;
per cases
( n = 0 or n <> 0 )
;
suppose A6:
n <> 0
;
:: thesis: union b2 in b2
set Y =
Z \ {y};
reconsider Y =
Z \ {y} as
finite set ;
{y} c= Z
by A3, ZFMISC_1:37;
then A7:
card Y =
(n + 1) - (card {y})
by A2, Th63
.=
(n + 1) - 1
by CARD_1:50
.=
n
;
for
a,
b being
set st
a in Y &
b in Y & not
a c= b holds
b c= a
by A4;
then A8:
union Y in Y
by A1, A6, A7, CARD_1:47;
then A9:
union Y in Z
;
A10:
(
y c= union Y or
union Y c= y )
by A4, A8;
A11:
y in Z
by A3;
Z = (Z \ {y}) \/ {y}
then union Z =
(union Y) \/ (union {y})
by ZFMISC_1:96
.=
(union Y) \/ y
by ZFMISC_1:31
;
hence
union Z in Z
by A9, A10, A11, XBOOLE_1:12;
:: thesis: verum
end;
end;
end;
Lm6:
for Z being finite set st Z <> {} & ( for X, Y being set st X in Z & Y in Z & not X c= Y holds
Y c= X ) holds
union Z in Z
theorem :: CARD_2:81
theorem :: CARD_2:82
for
x1,
x2,
x3,
x4,
x5 being
set st
x1,
x2,
x3,
x4,
x5 are_mutually_different holds
card {x1,x2,x3,x4,x5} = 5
theorem :: CARD_2:83