:: Cardinal Numbers and Finite Sets
:: by Karol P\c{a}k
::
:: Received May 24, 2005
:: Copyright (c) 2005 Association of Mizar Users
theorem Th1: :: CARD_FIN:1
theorem Th2: :: CARD_FIN:2
theorem Th3: :: CARD_FIN:3
theorem Th4: :: CARD_FIN:4
theorem Th5: :: CARD_FIN:5
theorem :: CARD_FIN:6
theorem Th7: :: CARD_FIN:7
theorem Th8: :: CARD_FIN:8
definition
let X be
finite set ;
let k be
Element of
NAT ;
let x1,
x2 be
set ;
func Choose X,
k,
x1,
x2 -> Subset of
(Funcs X,{x1,x2}) means :
Def1:
:: CARD_FIN:def 1
for
x being
set holds
(
x in it iff ex
f being
Function of
X,
{x1,x2} st
(
f = x &
card (f " {x1}) = k ) );
existence
ex b1 being Subset of (Funcs X,{x1,x2}) st
for x being set holds
( x in b1 iff ex f being Function of X,{x1,x2} st
( f = x & card (f " {x1}) = k ) )
uniqueness
for b1, b2 being Subset of (Funcs X,{x1,x2}) st ( for x being set holds
( x in b1 iff ex f being Function of X,{x1,x2} st
( f = x & card (f " {x1}) = k ) ) ) & ( for x being set holds
( x in b2 iff ex f being Function of X,{x1,x2} st
( f = x & card (f " {x1}) = k ) ) ) holds
b1 = b2
end;
:: deftheorem Def1 defines Choose CARD_FIN:def 1 :
theorem :: CARD_FIN:9
theorem Th10: :: CARD_FIN:10
theorem Th11: :: CARD_FIN:11
theorem Th12: :: CARD_FIN:12
theorem Th13: :: CARD_FIN:13
theorem Th14: :: CARD_FIN:14
theorem Th15: :: CARD_FIN:15
theorem Th16: :: CARD_FIN:16
Lm1:
for x, y, z being set
for X being finite set
for k being Element of NAT st x <> y & not z in X holds
( { f where f is Function of X \/ {z},{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) } \/ { f where f is Function of X \/ {z},{x,y} : ( card (f " {x}) = k + 1 & f . z = y ) } = Choose (X \/ {z}),(k + 1),x,y & { f where f is Function of X \/ {z},{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) } misses { f where f is Function of X \/ {z},{x,y} : ( card (f " {x}) = k + 1 & f . z = y ) } )
theorem Th17: :: CARD_FIN:17
for
x,
y,
z being
set for
X being
finite set for
k being
Element of
NAT st
x <> y & not
z in X holds
card (Choose (X \/ {z}),(k + 1),x,y) = (card (Choose X,(k + 1),x,y)) + (card (Choose X,k,x,y))
theorem Th18: :: CARD_FIN:18
theorem Th19: :: CARD_FIN:19
theorem Th20: :: CARD_FIN:20
:: deftheorem Def2 defines Intersection CARD_FIN:def 2 :
theorem Th21: :: CARD_FIN:21
theorem Th22: :: CARD_FIN:22
theorem :: CARD_FIN:23
theorem Th24: :: CARD_FIN:24
theorem :: CARD_FIN:25
theorem Th26: :: CARD_FIN:26
theorem :: CARD_FIN:27
theorem Th28: :: CARD_FIN:28
theorem Th29: :: CARD_FIN:29
theorem Th30: :: CARD_FIN:30
theorem Th31: :: CARD_FIN:31
theorem Th32: :: CARD_FIN:32
theorem Th33: :: CARD_FIN:33
theorem Th34: :: CARD_FIN:34
theorem Th35: :: CARD_FIN:35
theorem Th36: :: CARD_FIN:36
theorem Th37: :: CARD_FIN:37
theorem Th38: :: CARD_FIN:38
theorem :: CARD_FIN:39
:: deftheorem Def3 defines finite-yielding CARD_FIN:def 3 :
theorem :: CARD_FIN:40
theorem Th41: :: CARD_FIN:41
Lm2:
for k being Element of NAT
for F being XFinSequence st k <= len F holds
len (F | k) = k
theorem Th42: :: CARD_FIN:42
theorem :: CARD_FIN:43
theorem Th44: :: CARD_FIN:44
theorem Th45: :: CARD_FIN:45
theorem :: CARD_FIN:46
theorem Th47: :: CARD_FIN:47
theorem Th48: :: CARD_FIN:48
Lm3:
for X being finite set ex P being Function of card X,X st P is one-to-one
definition
let k be
Element of
NAT ;
let F be
finite-yielding Function;
assume A1:
dom F is
finite
;
func Card_Intersection F,
k -> Element of
NAT means :
Def4:
:: CARD_FIN:def 4
for
x,
y being
set for
X being
finite set for
P being
Function of
card (Choose X,k,x,y),
Choose X,
k,
x,
y st
dom F = X &
P is
one-to-one &
x <> y holds
ex
XFS being
XFinSequence of
NAT st
(
dom XFS = dom P & ( for
z being
set for
f being
Function st
z in dom XFS &
f = P . z holds
XFS . z = card (Intersection F,f,x) ) &
it = Sum XFS );
existence
ex b1 being Element of NAT st
for x, y being set
for X being finite set
for P being Function of card (Choose X,k,x,y), Choose X,k,x,y st dom F = X & P is one-to-one & x <> y holds
ex XFS being XFinSequence of NAT st
( dom XFS = dom P & ( for z being set
for f being Function st z in dom XFS & f = P . z holds
XFS . z = card (Intersection F,f,x) ) & b1 = Sum XFS )
uniqueness
for b1, b2 being Element of NAT st ( for x, y being set
for X being finite set
for P being Function of card (Choose X,k,x,y), Choose X,k,x,y st dom F = X & P is one-to-one & x <> y holds
ex XFS being XFinSequence of NAT st
( dom XFS = dom P & ( for z being set
for f being Function st z in dom XFS & f = P . z holds
XFS . z = card (Intersection F,f,x) ) & b1 = Sum XFS ) ) & ( for x, y being set
for X being finite set
for P being Function of card (Choose X,k,x,y), Choose X,k,x,y st dom F = X & P is one-to-one & x <> y holds
ex XFS being XFinSequence of NAT st
( dom XFS = dom P & ( for z being set
for f being Function st z in dom XFS & f = P . z holds
XFS . z = card (Intersection F,f,x) ) & b2 = Sum XFS ) ) holds
b1 = b2
end;
:: deftheorem Def4 defines Card_Intersection CARD_FIN:def 4 :
for
k being
Element of
NAT for
F being
finite-yielding Function st
dom F is
finite holds
for
b3 being
Element of
NAT holds
(
b3 = Card_Intersection F,
k iff for
x,
y being
set for
X being
finite set for
P being
Function of
card (Choose X,k,x,y),
Choose X,
k,
x,
y st
dom F = X &
P is
one-to-one &
x <> y holds
ex
XFS being
XFinSequence of
NAT st
(
dom XFS = dom P & ( for
z being
set for
f being
Function st
z in dom XFS &
f = P . z holds
XFS . z = card (Intersection F,f,x) ) &
b3 = Sum XFS ) );
theorem :: CARD_FIN:49
for
k being
Element of
NAT for
Fy being
finite-yielding Function for
x,
y being
set for
X being
finite set for
P being
Function of
card (Choose X,k,x,y),
Choose X,
k,
x,
y st
dom Fy = X &
P is
one-to-one &
x <> y holds
for
XFS being
XFinSequence of
NAT st
dom XFS = dom P & ( for
z being
set for
f being
Function st
z in dom XFS &
f = P . z holds
XFS . z = card (Intersection Fy,f,x) ) holds
Card_Intersection Fy,
k = Sum XFS
theorem :: CARD_FIN:50
theorem Th51: :: CARD_FIN:51
theorem Th52: :: CARD_FIN:52
theorem Th53: :: CARD_FIN:53
theorem Th54: :: CARD_FIN:54
theorem :: CARD_FIN:55
theorem Th56: :: CARD_FIN:56
theorem Th57: :: CARD_FIN:57
theorem Th58: :: CARD_FIN:58
theorem Th59: :: CARD_FIN:59
theorem Th60: :: CARD_FIN:60
theorem Th61: :: CARD_FIN:61
theorem Th62: :: CARD_FIN:62
:: deftheorem defines Sum CARD_FIN:def 5 :
theorem Th63: :: CARD_FIN:63
theorem Th64: :: CARD_FIN:64
theorem Th65: :: CARD_FIN:65
theorem Th66: :: CARD_FIN:66
theorem Th67: :: CARD_FIN:67
theorem Th68: :: CARD_FIN:68
theorem Th69: :: CARD_FIN:69
Lm4:
for X, Y being finite set st not X is empty & not Y is empty holds
ex F being XFinSequence of INT st
( dom F = card Y & ((card Y) |^ (card X)) - (Sum F) = card { f where f is Function of X,Y : f is onto } & ( for n being Element of NAT st n in dom F holds
F . n = (((- 1) |^ n) * ((card Y) choose (n + 1))) * ((((card Y) - n) - 1) |^ (card X)) ) )
theorem Th70: :: CARD_FIN:70
theorem :: CARD_FIN:71
theorem Th72: :: CARD_FIN:72
Lm5:
for X, Y being finite set
for F being Function of X,Y st dom F = X & F is one-to-one holds
ex XF being XFinSequence of INT st
( dom XF = card X & ((card X) ! ) - (Sum XF) = card { h where h is Function of X, rng F : ( h is one-to-one & ( for x being set st x in X holds
h . x <> F . x ) ) } & ( for n being Element of NAT st n in dom XF holds
XF . n = (((- 1) |^ n) * ((card X) ! )) / ((n + 1) ! ) ) )
theorem Th73: :: CARD_FIN:73
theorem :: CARD_FIN:74