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


begin

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 )
proofend;

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

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

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

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

theorem Th6: :: CARD_4:6
omega *` omega = omega by Th5, CARD_1:47, CARD_2:def_2;

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

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

theorem Th9: :: CARD_4:9
for D being non empty set
for n, m being Element of NAT holds
( [:(n -tuples_on D),(m -tuples_on D):],(n + m) -tuples_on D are_equipotent &amp; card [:(n -tuples_on D),(m -tuples_on D):] = card ((n + m) -tuples_on D) )
proofend;

theorem Th10: :: CARD_4:10
for D being non empty set
for n being Element of NAT st D is countable holds
n -tuples_on D is countable
proofend;

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

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

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

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

scheme :: CARD_4:sch 1
FraenCoun1{ F1( set ) ->  set , P1[ set ] } :
  {  F1(n) where n is Element of NAT : P1[n]  }  is countable
proofend;

scheme :: CARD_4:sch 2
FraenCoun2{ F1( set , set ) ->  set , P1[ set , set ] } :
  {  F1(n1,n2) where n1, n2 is Element of NAT : P1[n1,n2]  }  is countable
proofend;

scheme :: CARD_4:sch 3
FraenCoun3{ F1( set , set , set ) ->  set , P1[ set , set , set ] } :
  {  F1(n1,n2,n3) where n1, n2, n3 is Element of NAT : P1[n1,n2,n3]  }  is countable
proofend;

:: [WP: ] Hessenberg's_theorem
theorem Th15: :: CARD_4:15
for M being Cardinal st not M is finite holds
M *` M = M
proofend;

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

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

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

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

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

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

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

theorem Th23: :: CARD_4:23
for D being non empty set
for n being Element of NAT st not D is finite &amp; n <> 0 holds
( n -tuples_on D,D are_equipotent &amp; card (n -tuples_on D) = card D )
proofend;

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