begin
definition
let X be
finite set ;
let k be
Nat;
let x1,
x2 be
set ;
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;
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 Th15:
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)))
Lm2:
for X being finite set ex P being Function of (card X),X st P is one-to-one
definition
canceled;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 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 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 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 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 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 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
Lm3:
for X, Y being finite set st not X is empty & not Y is empty holds
ex F being XFinSequence of 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)) ) )
Lm4:
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 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) !) ) )