begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem
theorem Th7:
theorem Th8:
definition
let X be
finite set ;
let k be
Nat;
let x1,
x2 be
set ;
func Choose X,
k,
x1,
x2 -> Subset of
(Funcs X,{x1,x2}) means :
Def1:
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
theorem Th10:
theorem Th11:
theorem Th12:
theorem
canceled;
theorem Th14:
theorem
canceled;
theorem Th16:
Lm1:
for x, y, z being set
for X being finite set
for k being Nat st x <> y 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:
for
x,
y,
z being
set for
X being
finite set for
k being
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:
theorem Th19:
theorem Th20:
:: deftheorem Def2 defines Intersection CARD_FIN:def 2 :
theorem Th21:
theorem Th22:
theorem
theorem Th24:
theorem
theorem Th26:
theorem
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem
:: deftheorem Def3 defines finite-yielding CARD_FIN:def 3 :
theorem
theorem Th41:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem
canceled;
Lm3:
for X being finite set ex P being Function of (card X),X st P is one-to-one
definition
let k be
Nat;
let F be
finite-yielding Function;
assume A1:
dom F is
finite
;
func Card_Intersection F,
k -> Element of
NAT means :
Def4:
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
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
for
k being
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
theorem Th51:
theorem Th52:
theorem Th53:
theorem Th54:
theorem
theorem Th56:
theorem Th57:
theorem Th58:
theorem Th59:
theorem Th60:
theorem Th61:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th65:
theorem Th66:
theorem Th67:
theorem Th68:
theorem Th69:
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 Nat st n in dom F holds
F . n = (((- 1) |^ n) * ((card Y) choose (n + 1))) * ((((card Y) - n) - 1) |^ (card X)) ) )
theorem Th70:
theorem
theorem Th72:
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 Nat st n in dom XF holds
XF . n = (((- 1) |^ n) * ((card X) ! )) / ((n + 1) ! ) ) )
theorem Th73:
theorem