:: 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{ F₁( object ) -> set , P₁[ set ] } :

{ F₁(n) where n is Nat : P₁[n] } is countable

proof end;

scheme :: CARD_4:sch 2
FraenCoun2{ F₁( object , object ) -> set , P₁[ set , set ] } :

{ F₁(n1,n2) where n1, n2 is Nat : P₁[n1,n2] } is countable

proof end;

scheme :: CARD_4:sch 3
FraenCoun3{ F₁( object , object , object ) -> set , P₁[ set , set , set ] } :

{ F₁(n1,n2,n3) where n1, n2, n3 is Nat : P₁[n1,n2,n3] } is countable

proof end;

:: 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;