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

begin

theorem :: CARD_4:1

canceled;

theorem :: CARD_4:2

canceled;

theorem :: CARD_4:3

canceled;

theorem :: CARD_4:4

canceled;

theorem :: CARD_4:5

canceled;

theorem :: CARD_4:6

canceled;

theorem :: CARD_4:7

canceled;

theorem :: CARD_4:8

canceled;

theorem :: CARD_4:9

canceled;

theorem :: CARD_4:10

canceled;

theorem :: CARD_4:11

canceled;

theorem :: CARD_4:12

canceled;

theorem :: CARD_4:13

canceled;

theorem :: CARD_4:14

canceled;

theorem :: CARD_4:15

canceled;

theorem :: CARD_4:16

canceled;

theorem :: CARD_4:17

canceled;

theorem :: CARD_4:18

canceled;

theorem :: CARD_4:19

canceled;

theorem :: CARD_4:20

canceled;

theorem :: CARD_4:21

canceled;

theorem :: CARD_4:22

canceled;

theorem :: CARD_4:23

canceled;

theorem :: CARD_4:24

canceled;

theorem :: CARD_4:25

canceled;

theorem :: CARD_4:26

canceled;

theorem :: CARD_4:27

canceled;

theorem :: CARD_4:28

canceled;

theorem :: CARD_4:29

canceled;

theorem :: CARD_4:30

canceled;

theorem :: CARD_4:31

canceled;

theorem :: CARD_4:32

canceled;

theorem :: CARD_4:33

canceled;

theorem :: CARD_4:34

canceled;

theorem :: CARD_4:35

canceled;

theorem :: CARD_4:36

canceled;

theorem :: CARD_4:37

canceled;

theorem :: CARD_4:38

canceled;

theorem :: CARD_4:39

canceled;

theorem :: CARD_4:40

canceled;

theorem :: CARD_4:41

canceled;

theorem :: CARD_4:42

canceled;

theorem :: CARD_4:43

for X being set st X is finite holds
X is countable ;

theorem :: CARD_4:44

omega is countable ;

theorem :: CARD_4:45

canceled;

theorem :: CARD_4:46

canceled;

theorem :: CARD_4:47

canceled;

theorem :: CARD_4:48

canceled;

theorem :: CARD_4:49

canceled;

theorem :: CARD_4:50

canceled;

theorem Th51: :: CARD_4:51

for n being Nat
for r being Real holds
( ( r <> 0 or n = 0 ) iff r |^ n <> 0 )

proof end;

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

proof end;

theorem Th52: :: CARD_4:52

for n1, m1, n2, m2 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 Th53: :: CARD_4:53

( [:NAT,NAT:], NAT are_equipotent & card NAT = card [:NAT,NAT:] )

proof end;

theorem Th54: :: CARD_4:54

omega *` omega = omega by Th53, CARD_1:84, CARD_2:def 2;

theorem Th55: :: CARD_4:55

for X, Y being set st X is countable & Y is countable holds
[:X,Y:] is countable

proof end;

theorem Th56: :: CARD_4:56

for D being non empty set holds
( 1 -tuples_on D,D are_equipotent & card (1 -tuples_on D) = card D )

proof end;

theorem Th57: :: CARD_4:57

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 & card [:(n -tuples_on D),(m -tuples_on D):] = card ((n + m) -tuples_on D) )

proof end;

theorem Th58: :: CARD_4:58

for D being non empty set
for n being Element of NAT st D is countable holds
n -tuples_on D is countable

proof end;

theorem :: CARD_4:59

canceled;

theorem :: CARD_4:60

canceled;

theorem Th61: :: CARD_4:61

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

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

canceled;

theorem :: CARD_4:64

canceled;

theorem :: CARD_4:65

for D being non empty set st D is countable holds
D * is countable

proof end;

theorem :: CARD_4:66

for D being non empty set holds omega c= card (D *)

proof end;

scheme :: CARD_4:sch 1
FraenCoun1{ F₁( set ) -> set , P₁[ set ] } :

{ F₁(n) where n is Element of NAT : P₁[n] } is countable

proof end;

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

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

proof end;

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

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

proof end;

theorem :: CARD_4:67

canceled;

theorem :: CARD_4:68

canceled;

theorem :: CARD_4:69

canceled;

theorem :: CARD_4:70

canceled;

theorem :: CARD_4:71

canceled;

theorem :: CARD_4:72

canceled;

theorem :: CARD_4:73

canceled;

theorem :: CARD_4:74

canceled;

theorem :: CARD_4:75

canceled;

theorem :: CARD_4:76

canceled;

theorem Th77: :: CARD_4:77

for M being Cardinal st not M is finite holds
M *` M = M

proof end;

theorem Th78: :: CARD_4:78

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 Th79: :: CARD_4:79

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

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

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

for K, L, 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 :: CARD_4:83

canceled;

theorem Th84: :: CARD_4:84

for X being set st not X is finite holds
card X = omega *` (card X)

proof end;

theorem :: CARD_4:85

for X, Y being set st X <> {} & X is finite & not Y is finite holds
(card Y) *` (card X) = card Y

proof end;

theorem Th86: :: CARD_4:86

for D being non empty set
for n being Element of 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:87

for D being non empty set st not D is finite holds
card D = card (D *)

proof end;