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

environ

vocabularies HIDDEN, NUMBERS, XBOOLE_0, NAT_1, ORDINAL1, CARD_1, FUNCT_1, FINSET_1, CARD_3, REAL_1, NEWTON, ARYTM_3, RELAT_1, XXREAL_0, SUBSET_1, ZFMISC_1, MCART_1, TARSKI, CARD_2, FINSEQ_2, FINSEQ_1, ORDINAL4, PARTFUN1, FUNCT_4, RECDEF_2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, NAT_1, NAT_D, RELAT_1, FUNCT_1, FINSEQ_1, FINSET_1, WELLORD2, XTUPLE_0, MCART_1, DOMAIN_1, CARD_2, FINSEQ_2, RELSET_1, FUNCT_2, BINOP_1, FUNCT_4, PARTFUN1, NEWTON, CARD_3;
definitions TARSKI, FUNCT_1, WELLORD2, RELAT_1, XBOOLE_0, CARD_3;
theorems TARSKI, ZFMISC_1, NAT_1, ORDINAL1, ORDINAL3, WELLORD2, FUNCT_1, FUNCT_2, FUNCT_4, PARTFUN1, MCART_1, CARD_3, ORDERS_1, CARD_1, CARD_2, NEWTON, FINSEQ_1, FINSEQ_2, RELAT_1, XBOOLE_0, XBOOLE_1, XCMPLX_1, XREAL_1, XXREAL_0, NAT_D, XTUPLE_0;
schemes NAT_1, FUNCT_1, XBOOLE_0, BINOP_1, CLASSES1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1, XXREAL_0, NAT_1, CARD_1, FINSEQ_1, FINSEQ_2, CARD_3, XCMPLX_0, RELSET_1, XTUPLE_0, NEWTON, XREAL_0;
constructors HIDDEN, PARTFUN1, WELLORD2, BINOP_1, DOMAIN_1, FUNCOP_1, FUNCT_4, ORDINAL3, XXREAL_0, NAT_1, NAT_D, MEMBERED, CARD_2, CARD_3, NEWTON, FINSUB_1, RELSET_1, FINSEQ_2, XTUPLE_0;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
equalities BINOP_1, CARD_3, XTUPLE_0, CARD_1, ORDINAL1;
expansions TARSKI, FUNCT_1, WELLORD2, XBOOLE_0, CARD_3;


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;