:: Countable Sets and Hessenberg's Theorem
:: by Grzegorz Bancerek
::
:: Received September 5, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users


theorem :: CARD_4:1
for X being set st X is finite holds
X is countable ;

theorem :: CARD_4:2
omega is countable ;

theorem Th3: :: CARD_4:3
for n being Nat
for r being Real holds
( ( r <> 0 or n = 0 ) iff r |^ n <> 0 )
proof end;

Lm1: for n1, n2, m2, m1 being Nat st (2 |^ n1) * ((2 * m1) + 1) = (2 |^ n2) * ((2 * m2) + 1) holds
n1 <= n2

proof end;

theorem Th4: :: CARD_4:4
for n1, n2, m2, m1 being Nat st (2 |^ n1) * ((2 * m1) + 1) = (2 |^ n2) * ((2 * m2) + 1) holds
( n1 = n2 & m1 = m2 )
proof end;

Lm2: for x being set st x in [:NAT,NAT:] holds
ex n1, n2 being Element of NAT st x = [n1,n2]

proof end;

theorem Th5: :: CARD_4:5
( [:NAT,NAT:], NAT are_equipotent & card NAT = card [:NAT,NAT:] )
proof end;

theorem Th6: :: CARD_4:6
omega *` omega = omega by Th5, CARD_2:def 2;

theorem Th7: :: CARD_4:7
for X, Y being set st X is countable & Y is countable holds
[:X,Y:] is countable
proof end;

theorem Th8: :: CARD_4:8
for D being non empty set holds
( 1 -tuples_on D,D are_equipotent & card (1 -tuples_on D) = card D )
proof end;

theorem Th9: :: CARD_4:9
for D being non empty set
for m, n being Nat holds
( [:(n -tuples_on D),(m -tuples_on D):],(n + m) -tuples_on D are_equipotent & card [:(n -tuples_on D),(m -tuples_on D):] = card ((n + m) -tuples_on D) )
proof end;

theorem Th10: :: CARD_4:10
for D being non empty set
for n being Nat st D is countable holds
n -tuples_on D is countable
proof end;

theorem Th11: :: CARD_4:11
for f being Function st dom f is countable & ( for x being set st x in dom f holds
f . x is countable ) holds
Union f is countable
proof end;

theorem :: CARD_4:12
for X being set st X is countable & ( for Y being set st Y in X holds
Y is countable ) holds
union X is countable
proof end;

theorem :: CARD_4:13
for D being non empty set st D is countable holds
D * is countable
proof end;

theorem :: CARD_4:14
for D being non empty set holds omega c= card (D *)
proof end;

scheme :: CARD_4:sch 1
FraenCoun1{ F1( object ) -> set , P1[ set ] } :
{ F1(n) where n is Nat : P1[n] } is countable
proof end;

scheme :: CARD_4:sch 2
FraenCoun2{ F1( object , object ) -> set , P1[ set , set ] } :
{ F1(n1,n2) where n1, n2 is Nat : P1[n1,n2] } is countable
proof end;

scheme :: CARD_4:sch 3
FraenCoun3{ F1( object , object , object ) -> set , P1[ set , set , set ] } :
{ F1(n1,n2,n3) where n1, n2, n3 is Nat : P1[n1,n2,n3] } is countable
proof end;

:: WP: Hessenberg's theorem
theorem Th15: :: CARD_4:15
for M being Cardinal st not M is finite holds
M *` M = M
proof end;

theorem Th16: :: CARD_4:16
for M, N being Cardinal st not M is finite & 0 in N & ( N c= M or N in M ) holds
( M *` N = M & N *` M = M )
proof end;

theorem Th17: :: CARD_4:17
for M, N being Cardinal st not M is finite & ( N c= M or N in M ) holds
( M *` N c= M & N *` M c= M )
proof end;

theorem :: CARD_4:18
for X being set st not X is finite holds
( [:X,X:],X are_equipotent & card [:X,X:] = card X )
proof end;

theorem :: CARD_4:19
for X, Y being set st not X is finite & Y is finite & Y <> {} holds
( [:X,Y:],X are_equipotent & card [:X,Y:] = card X )
proof end;

theorem :: CARD_4:20
for L, K, M, N being Cardinal st K in L & M in N holds
( K *` M in L *` N & M *` K in L *` N )
proof end;

theorem Th21: :: CARD_4:21
for X being set st not X is finite holds
card X = omega *` (card X)
proof end;

theorem :: CARD_4:22
for X, Y being set st X <> {} & X is finite & not Y is finite holds
(card Y) *` (card X) = card Y
proof end;

theorem Th23: :: CARD_4:23
for D being non empty set
for n being Nat st not D is finite & n <> 0 holds
( n -tuples_on D,D are_equipotent & card (n -tuples_on D) = card D )
proof end;

theorem :: CARD_4:24
for D being non empty set st not D is finite holds
card D = card (D *)
proof end;