:: by Grzegorz Bancerek

::

:: Received September 5, 1990

:: Copyright (c) 1990-2016 Association of Mizar Users

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 )

( 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 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 )

( 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) )

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

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

Y is countable ) holds

union X is countable

proof end;

:: Hessenberg's theorem

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 )

( 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 )

( M *` N c= M & N *` M c= M )

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 )

( [:X,Y:],X are_equipotent & card [:X,Y:] = card X )

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 )

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;