:: by Karol P\c{a}k

::

:: Received May 24, 2005

:: Copyright (c) 2005-2021 Association of Mizar Users

::$CT

theorem Th1: :: CARD_FIN:2

for X, Y being finite set

for x, y being set st ( Y = {} implies X = {} ) & not x in X holds

card (Funcs (X,Y)) = card { F where F is Function of (X \/ {x}),(Y \/ {y}) : ( rng (F | X) c= Y & F . x = y ) }

for x, y being set st ( Y = {} implies X = {} ) & not x in X holds

card (Funcs (X,Y)) = card { F where F is Function of (X \/ {x}),(Y \/ {y}) : ( rng (F | X) c= Y & F . x = y ) }

proof end;

theorem Th2: :: CARD_FIN:3

for X, Y being finite set

for x, y being set st not x in X & y in Y holds

card (Funcs (X,Y)) = card { F where F is Function of (X \/ {x}),Y : F . x = y }

for x, y being set st not x in X & y in Y holds

card (Funcs (X,Y)) = card { F where F is Function of (X \/ {x}),Y : F . x = y }

proof end;

:: card Funcs(X,Y)

theorem Th3: :: CARD_FIN:4

for X, Y being finite set st ( Y = {} implies X = {} ) holds

card (Funcs (X,Y)) = (card Y) |^ (card X)

card (Funcs (X,Y)) = (card Y) |^ (card X)

proof end;

theorem Th4: :: CARD_FIN:5

for X, Y being finite set

for x, y being set st ( Y is empty implies X is empty ) & not x in X & not y in Y holds

card { F where F is Function of X,Y : F is one-to-one } = card { F where F is Function of (X \/ {x}),(Y \/ {y}) : ( F is one-to-one & F . x = y ) }

for x, y being set st ( Y is empty implies X is empty ) & not x in X & not y in Y holds

card { F where F is Function of X,Y : F is one-to-one } = card { F where F is Function of (X \/ {x}),(Y \/ {y}) : ( F is one-to-one & F . x = y ) }

proof end;

:: one-to-one

theorem Th6: :: CARD_FIN:7

for X, Y being finite set st card X <= card Y holds

card { F where F is Function of X,Y : F is one-to-one } = ((card Y) !) / (((card Y) -' (card X)) !)

card { F where F is Function of X,Y : F is one-to-one } = ((card Y) !) / (((card Y) -' (card X)) !)

proof end;

:: Permutation of X

theorem Th7: :: CARD_FIN:8

for X being finite set holds card { F where F is Function of X,X : F is Permutation of X } = (card X) !

proof end;

definition

let X be finite set ;

let k be Nat;

let x1, x2 be object ;

ex b_{1} being Subset of (Funcs (X,{x1,x2})) st

for x being set holds

( x in b_{1} iff ex f being Function of X,{x1,x2} st

( f = x & card (f " {x1}) = k ) )

for b_{1}, b_{2} being Subset of (Funcs (X,{x1,x2})) st ( for x being set holds

( x in b_{1} iff ex f being Function of X,{x1,x2} st

( f = x & card (f " {x1}) = k ) ) ) & ( for x being set holds

( x in b_{2} iff ex f being Function of X,{x1,x2} st

( f = x & card (f " {x1}) = k ) ) ) holds

b_{1} = b_{2}

end;
let k be Nat;

let x1, x2 be object ;

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 for x being set holds

( x in it iff ex f being Function of X,{x1,x2} st

( f = x & card (f " {x1}) = k ) );

ex b

for x being set holds

( x in b

( f = x & card (f " {x1}) = k ) )

proof end;

uniqueness for b

( x in b

( f = x & card (f " {x1}) = k ) ) ) & ( for x being set holds

( x in b

( f = x & card (f " {x1}) = k ) ) ) holds

b

proof end;

:: deftheorem Def1 defines Choose CARD_FIN:def 1 :

for X being finite set

for k being Nat

for x1, x2 being object

for b_{5} being Subset of (Funcs (X,{x1,x2})) holds

( b_{5} = Choose (X,k,x1,x2) iff for x being set holds

( x in b_{5} iff ex f being Function of X,{x1,x2} st

( f = x & card (f " {x1}) = k ) ) );

for X being finite set

for k being Nat

for x1, x2 being object

for b

( b

( x in b

( f = x & card (f " {x1}) = k ) ) );

theorem :: CARD_FIN:9

for x1 being set

for X being finite set

for k being Nat st card X <> k holds

Choose (X,k,x1,x1) is empty

for X being finite set

for k being Nat st card X <> k holds

Choose (X,k,x1,x1) is empty

proof end;

theorem Th9: :: CARD_FIN:10

for X being finite set

for k being Nat

for x1, x2 being object st card X < k holds

Choose (X,k,x1,x2) is empty

for k being Nat

for x1, x2 being object st card X < k holds

Choose (X,k,x1,x2) is empty

proof end;

theorem Th12: :: CARD_FIN:13

for X being finite set

for k being Nat

for z, x, y being object st not z in X holds

card (Choose (X,k,x,y)) = card { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) }

for k being Nat

for z, x, y being object st not z in X holds

card (Choose (X,k,x,y)) = card { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) }

proof end;

theorem Th13: :: CARD_FIN:14

for X being finite set

for k being Nat

for z, x, y being object st not z in X & x <> y holds

card (Choose (X,k,x,y)) = card { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k & f . z = y ) }

for k being Nat

for z, x, y being object st not z in X & x <> y holds

card (Choose (X,k,x,y)) = card { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k & f . z = y ) }

proof end;

Lm1: for X being finite set

for k being Nat

for z, x, y being object 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 ) } )

proof end;

theorem Th14: :: CARD_FIN:15

for X being finite set

for k being Nat

for z, x, y being object 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)))

for k being Nat

for z, x, y being object 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)))

proof end;

theorem Th15: :: CARD_FIN:16

for X being finite set

for k being Nat

for x, y being object st x <> y holds

card (Choose (X,k,x,y)) = (card X) choose k

for k being Nat

for x, y being object st x <> y holds

card (Choose (X,k,x,y)) = (card X) choose k

proof end;

theorem Th16: :: CARD_FIN:17

for X, Y being finite set

for x, y being object st x <> y holds

(Y --> y) +* (X --> x) in Choose ((X \/ Y),(card X),x,y)

for x, y being object st x <> y holds

(Y --> y) +* (X --> x) in Choose ((X \/ Y),(card X),x,y)

proof end;

theorem Th17: :: CARD_FIN:18

for x, y being set

for X, Y being finite set st x <> y & X misses Y holds

(X --> x) +* (Y --> y) in Choose ((X \/ Y),(card X),x,y)

for X, Y being finite set st x <> y & X misses Y holds

(X --> x) +* (Y --> y) in Choose ((X \/ Y),(card X),x,y)

proof end;

definition

let F, Ch be Function;

let y be object ;

ex b_{1} being Subset of (union (rng F)) st

for z being set holds

( z in b_{1} iff ( z in union (rng F) & ( for x being set st x in dom Ch & Ch . x = y holds

z in F . x ) ) )

for b_{1}, b_{2} being Subset of (union (rng F)) st ( for z being set holds

( z in b_{1} iff ( z in union (rng F) & ( for x being set st x in dom Ch & Ch . x = y holds

z in F . x ) ) ) ) & ( for z being set holds

( z in b_{2} iff ( z in union (rng F) & ( for x being set st x in dom Ch & Ch . x = y holds

z in F . x ) ) ) ) holds

b_{1} = b_{2}

end;
let y be object ;

func Intersection (F,Ch,y) -> Subset of (union (rng F)) means :Def2: :: CARD_FIN:def 2

for z being set holds

( z in it iff ( z in union (rng F) & ( for x being set st x in dom Ch & Ch . x = y holds

z in F . x ) ) );

existence for z being set holds

( z in it iff ( z in union (rng F) & ( for x being set st x in dom Ch & Ch . x = y holds

z in F . x ) ) );

ex b

for z being set holds

( z in b

z in F . x ) ) )

proof end;

uniqueness for b

( z in b

z in F . x ) ) ) ) & ( for z being set holds

( z in b

z in F . x ) ) ) ) holds

b

proof end;

:: deftheorem Def2 defines Intersection CARD_FIN:def 2 :

for F, Ch being Function

for y being object

for b_{4} being Subset of (union (rng F)) holds

( b_{4} = Intersection (F,Ch,y) iff for z being set holds

( z in b_{4} iff ( z in union (rng F) & ( for x being set st x in dom Ch & Ch . x = y holds

z in F . x ) ) ) );

for F, Ch being Function

for y being object

for b

( b

( z in b

z in F . x ) ) ) );

theorem Th18: :: CARD_FIN:19

for x, y being set

for F, Ch being Function st not (dom F) /\ (Ch " {x}) is empty holds

( y in Intersection (F,Ch,x) iff for z being set st z in dom Ch & Ch . z = x holds

y in F . z )

for F, Ch being Function st not (dom F) /\ (Ch " {x}) is empty holds

( y in Intersection (F,Ch,x) iff for z being set st z in dom Ch & Ch . z = x holds

y in F . z )

proof end;

theorem Th19: :: CARD_FIN:20

for y being set

for F, Ch being Function st not Intersection (F,Ch,y) is empty holds

Ch " {y} c= dom F

for F, Ch being Function st not Intersection (F,Ch,y) is empty holds

Ch " {y} c= dom F

proof end;

theorem :: CARD_FIN:21

for y being set

for F, Ch being Function st not Intersection (F,Ch,y) is empty holds

for x1, x2 being set st x1 in Ch " {y} & x2 in Ch " {y} holds

F . x1 meets F . x2

for F, Ch being Function st not Intersection (F,Ch,y) is empty holds

for x1, x2 being set st x1 in Ch " {y} & x2 in Ch " {y} holds

F . x1 meets F . x2

proof end;

theorem Th21: :: CARD_FIN:22

for y, z being set

for F, Ch being Function st z in Intersection (F,Ch,y) & y in rng Ch holds

ex x being set st

( x in dom Ch & Ch . x = y & z in F . x )

for F, Ch being Function st z in Intersection (F,Ch,y) & y in rng Ch holds

ex x being set st

( x in dom Ch & Ch . x = y & z in F . x )

proof end;

theorem :: CARD_FIN:23

for y being set

for F, Ch being Function st ( F is empty or union (rng F) is empty ) holds

Intersection (F,Ch,y) = union (rng F) by RELAT_1:38, ZFMISC_1:2;

for F, Ch being Function st ( F is empty or union (rng F) is empty ) holds

Intersection (F,Ch,y) = union (rng F) by RELAT_1:38, ZFMISC_1:2;

theorem Th23: :: CARD_FIN:24

for F, Ch being Function

for y being object st F | (Ch " {y}) = (Ch " {y}) --> (union (rng F)) holds

Intersection (F,Ch,y) = union (rng F)

for y being object st F | (Ch " {y}) = (Ch " {y}) --> (union (rng F)) holds

Intersection (F,Ch,y) = union (rng F)

proof end;

theorem :: CARD_FIN:25

for y being set

for F, Ch being Function st not union (rng F) is empty & Intersection (F,Ch,y) = union (rng F) holds

F | (Ch " {y}) = (Ch " {y}) --> (union (rng F))

for F, Ch being Function st not union (rng F) is empty & Intersection (F,Ch,y) = union (rng F) holds

F | (Ch " {y}) = (Ch " {y}) --> (union (rng F))

proof end;

theorem Th26: :: CARD_FIN:27

for X9 being set

for F, Ch being Function

for y being object holds Intersection (F,Ch,y) c= Intersection (F,(Ch | X9),y)

for F, Ch being Function

for y being object holds Intersection (F,Ch,y) c= Intersection (F,(Ch | X9),y)

proof end;

theorem Th27: :: CARD_FIN:28

for y, X9 being set

for F, Ch being Function st Ch " {y} = (Ch | X9) " {y} holds

Intersection (F,Ch,y) = Intersection (F,(Ch | X9),y)

for F, Ch being Function st Ch " {y} = (Ch | X9) " {y} holds

Intersection (F,Ch,y) = Intersection (F,(Ch | X9),y)

proof end;

theorem Th28: :: CARD_FIN:29

for y, X9 being set

for F, Ch being Function holds Intersection ((F | X9),Ch,y) c= Intersection (F,Ch,y)

for F, Ch being Function holds Intersection ((F | X9),Ch,y) c= Intersection (F,Ch,y)

proof end;

theorem Th29: :: CARD_FIN:30

for y, X9 being set

for F, Ch being Function st y in rng Ch & Ch " {y} c= X9 holds

Intersection ((F | X9),Ch,y) = Intersection (F,Ch,y)

for F, Ch being Function st y in rng Ch & Ch " {y} c= X9 holds

Intersection ((F | X9),Ch,y) = Intersection (F,Ch,y)

proof end;

theorem Th30: :: CARD_FIN:31

for F, Ch being Function

for x, y being object st x in Ch " {y} holds

Intersection (F,Ch,y) c= F . x

for x, y being object st x in Ch " {y} holds

Intersection (F,Ch,y) c= F . x

proof end;

theorem Th31: :: CARD_FIN:32

for F, Ch being Function

for x, y being object st x in Ch " {y} holds

(Intersection (F,(Ch | ((dom Ch) \ {x})),y)) /\ (F . x) = Intersection (F,Ch,y)

for x, y being object st x in Ch " {y} holds

(Intersection (F,(Ch | ((dom Ch) \ {x})),y)) /\ (F . x) = Intersection (F,Ch,y)

proof end;

theorem Th32: :: CARD_FIN:33

for F being Function

for x1, x2 being object

for Ch1, Ch2 being Function st Ch1 " {x1} = Ch2 " {x2} holds

Intersection (F,Ch1,x1) = Intersection (F,Ch2,x2)

for x1, x2 being object

for Ch1, Ch2 being Function st Ch1 " {x1} = Ch2 " {x2} holds

Intersection (F,Ch1,x1) = Intersection (F,Ch2,x2)

proof end;

theorem Th33: :: CARD_FIN:34

for F, Ch being Function

for y being object st Ch " {y} = {} holds

Intersection (F,Ch,y) = union (rng F)

for y being object st Ch " {y} = {} holds

Intersection (F,Ch,y) = union (rng F)

proof end;

theorem Th34: :: CARD_FIN:35

for F, Ch being Function

for x, y being object st {x} = Ch " {y} holds

Intersection (F,Ch,y) = F . x

for x, y being object st {x} = Ch " {y} holds

Intersection (F,Ch,y) = F . x

proof end;

theorem Th35: :: CARD_FIN:36

for x1, x2, y being set

for F, Ch being Function st {x1,x2} = Ch " {y} holds

Intersection (F,Ch,y) = (F . x1) /\ (F . x2)

for F, Ch being Function st {x1,x2} = Ch " {y} holds

Intersection (F,Ch,y) = (F . x1) /\ (F . x2)

proof end;

theorem :: CARD_FIN:37

for x, y being set

for F being Function st not F is empty holds

( y in Intersection (F,((dom F) --> x),x) iff for z being set st z in dom F holds

y in F . z )

for F being Function st not F is empty holds

( y in Intersection (F,((dom F) --> x),x) iff for z being set st z in dom F holds

y in F . z )

proof end;

registration
end;

registration

let F be finite-yielding Function;

let G be Function;

coherence

F * G is finite-yielding

Intersect (F,G) is finite-yielding

end;
let G be Function;

coherence

F * G is finite-yielding

proof end;

coherence Intersect (F,G) is finite-yielding

proof end;

theorem :: CARD_FIN:38

for y being set

for Ch being Function

for Fy being finite-yielding Function st y in rng Ch holds

Intersection (Fy,Ch,y) is finite

for Ch being Function

for Fy being finite-yielding Function st y in rng Ch holds

Intersection (Fy,Ch,y) is finite

proof end;

theorem :: CARD_FIN:40

for x being set

for n, k being Nat holds

( x in Choose (n,k,1,0) iff ex F being XFinSequence of NAT st

( F = x & dom F = n & rng F c= {0,1} & Sum F = k ) )

for n, k being Nat holds

( x in Choose (n,k,1,0) iff ex F being XFinSequence of NAT st

( F = x & dom F = n & rng F c= {0,1} & Sum F = k ) )

proof end;

Lm2: for X being finite set ex P being Function of (card X),X st P is one-to-one

proof end;

definition

let k be Nat;

let F be finite-yielding Function;

assume A1: dom F is finite ;

ex b_{1} being Element of NAT st

for x, y being object

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)) ) & b_{1} = Sum XFS )

for b_{1}, b_{2} being Element of NAT st ( for x, y being object

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)) ) & b_{1} = Sum XFS ) ) & ( for x, y being object

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)) ) & b_{2} = Sum XFS ) ) holds

b_{1} = b_{2}

end;
let F be finite-yielding Function;

assume A1: dom F is finite ;

func Card_Intersection (F,k) -> Element of NAT means :Def3: :: CARD_FIN:def 4

for x, y being object

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 for x, y being object

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

ex b

for x, y being object

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)) ) & b

proof end;

uniqueness for b

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)) ) & b

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)) ) & b

b

proof end;

:: deftheorem Def3 defines Card_Intersection CARD_FIN:def 4 :

for k being Nat

for F being finite-yielding Function st dom F is finite holds

for b_{3} being Element of NAT holds

( b_{3} = Card_Intersection (F,k) iff for x, y being object

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)) ) & b_{3} = Sum XFS ) );

for k being Nat

for F being finite-yielding Function st dom F is finite holds

for b

( b

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)) ) & b

theorem :: CARD_FIN:41

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

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

proof end;

theorem :: CARD_FIN:42

for k being Nat

for Fy being finite-yielding Function st dom Fy is finite & k = 0 holds

Card_Intersection (Fy,k) = card (union (rng Fy))

for Fy being finite-yielding Function st dom Fy is finite & k = 0 holds

Card_Intersection (Fy,k) = card (union (rng Fy))

proof end;

theorem Th42: :: CARD_FIN:43

for X being finite set

for k being Nat

for Fy being finite-yielding Function st dom Fy = X & k > card X holds

Card_Intersection (Fy,k) = 0

for k being Nat

for Fy being finite-yielding Function st dom Fy = X & k > card X holds

Card_Intersection (Fy,k) = 0

proof end;

theorem Th43: :: CARD_FIN:44

for Fy being finite-yielding Function

for X being finite set st dom Fy = X holds

for P being Function of (card X),X st P is one-to-one holds

ex XFS being XFinSequence of NAT st

( dom XFS = card X & ( for z being set st z in dom XFS holds

XFS . z = card ((Fy * P) . z) ) & Card_Intersection (Fy,1) = Sum XFS )

for X being finite set st dom Fy = X holds

for P being Function of (card X),X st P is one-to-one holds

ex XFS being XFinSequence of NAT st

( dom XFS = card X & ( for z being set st z in dom XFS holds

XFS . z = card ((Fy * P) . z) ) & Card_Intersection (Fy,1) = Sum XFS )

proof end;

theorem Th44: :: CARD_FIN:45

for X being finite set

for Fy being finite-yielding Function

for x being object st dom Fy = X holds

Card_Intersection (Fy,(card X)) = card (Intersection (Fy,(X --> x),x))

for Fy being finite-yielding Function

for x being object st dom Fy = X holds

Card_Intersection (Fy,(card X)) = card (Intersection (Fy,(X --> x),x))

proof end;

theorem Th45: :: CARD_FIN:46

for X being finite set

for Fy being finite-yielding Function

for x being object st Fy = x .--> X holds

Card_Intersection (Fy,1) = card X

for Fy being finite-yielding Function

for x being object st Fy = x .--> X holds

Card_Intersection (Fy,1) = card X

proof end;

theorem :: CARD_FIN:47

for x, y being set

for X, Y being finite set

for Fy being finite-yielding Function st x <> y & Fy = (x,y) --> (X,Y) holds

( Card_Intersection (Fy,1) = (card X) + (card Y) & Card_Intersection (Fy,2) = card (X /\ Y) )

for X, Y being finite set

for Fy being finite-yielding Function st x <> y & Fy = (x,y) --> (X,Y) holds

( Card_Intersection (Fy,1) = (card X) + (card Y) & Card_Intersection (Fy,2) = card (X /\ Y) )

proof end;

theorem Th47: :: CARD_FIN:48

for Fy being finite-yielding Function

for x being set st dom Fy is finite & x in dom Fy holds

Card_Intersection (Fy,1) = (Card_Intersection ((Fy | ((dom Fy) \ {x})),1)) + (card (Fy . x))

for x being set st dom Fy is finite & x in dom Fy holds

Card_Intersection (Fy,1) = (Card_Intersection ((Fy | ((dom Fy) \ {x})),1)) + (card (Fy . x))

proof end;

theorem Th48: :: CARD_FIN:49

for X9 being set

for F being Function holds

( dom (Intersect (F,((dom F) --> X9))) = dom F & ( for x being set st x in dom F holds

(Intersect (F,((dom F) --> X9))) . x = (F . x) /\ X9 ) )

for F being Function holds

( dom (Intersect (F,((dom F) --> X9))) = dom F & ( for x being set st x in dom F holds

(Intersect (F,((dom F) --> X9))) . x = (F . x) /\ X9 ) )

proof end;

theorem Th49: :: CARD_FIN:50

for X9 being set

for F being Function holds (union (rng F)) /\ X9 = union (rng (Intersect (F,((dom F) --> X9))))

for F being Function holds (union (rng F)) /\ X9 = union (rng (Intersect (F,((dom F) --> X9))))

proof end;

theorem Th50: :: CARD_FIN:51

for y, X9 being set

for F, Ch being Function holds (Intersection (F,Ch,y)) /\ X9 = Intersection ((Intersect (F,((dom F) --> X9))),Ch,y)

for F, Ch being Function holds (Intersection (F,Ch,y)) /\ X9 = Intersection ((Intersect (F,((dom F) --> X9))),Ch,y)

proof end;

theorem Th51: :: CARD_FIN:52

for F, G being XFinSequence st F is one-to-one & G is one-to-one & rng F misses rng G holds

F ^ G is one-to-one

F ^ G is one-to-one

proof end;

theorem Th52: :: CARD_FIN:53

for k being Nat

for Fy being finite-yielding Function

for X being finite set

for x being set

for n being Nat st dom Fy = X & x in dom Fy & k > 0 holds

Card_Intersection (Fy,(k + 1)) = (Card_Intersection ((Fy | ((dom Fy) \ {x})),(k + 1))) + (Card_Intersection ((Intersect ((Fy | ((dom Fy) \ {x})),(((dom Fy) \ {x}) --> (Fy . x)))),k))

for Fy being finite-yielding Function

for X being finite set

for x being set

for n being Nat st dom Fy = X & x in dom Fy & k > 0 holds

Card_Intersection (Fy,(k + 1)) = (Card_Intersection ((Fy | ((dom Fy) \ {x})),(k + 1))) + (Card_Intersection ((Intersect ((Fy | ((dom Fy) \ {x})),(((dom Fy) \ {x}) --> (Fy . x)))),k))

proof end;

theorem Th53: :: CARD_FIN:54

for x being set

for F being Function st x in dom F holds

union (rng F) = (union (rng (F | ((dom F) \ {x})))) \/ (F . x)

for F being Function st x in dom F holds

union (rng F) = (union (rng (F | ((dom F) \ {x})))) \/ (F . x)

proof end;

theorem Th54: :: CARD_FIN:55

for Fy being finite-yielding Function

for X being finite set ex XFS being XFinSequence of INT st

( dom XFS = card X & ( for n being Nat st n in dom XFS holds

XFS . n = ((- 1) |^ n) * (Card_Intersection (Fy,(n + 1))) ) )

for X being finite set ex XFS being XFinSequence of INT st

( dom XFS = card X & ( for n being Nat st n in dom XFS holds

XFS . n = ((- 1) |^ n) * (Card_Intersection (Fy,(n + 1))) ) )

proof end;

theorem Th55: :: CARD_FIN:56

for Fy being finite-yielding Function

for X being finite set st dom Fy = X holds

for XFS being XFinSequence of INT st dom XFS = card X & ( for n being Nat st n in dom XFS holds

XFS . n = ((- 1) |^ n) * (Card_Intersection (Fy,(n + 1))) ) holds

card (union (rng Fy)) = Sum XFS

for X being finite set st dom Fy = X holds

for XFS being XFinSequence of INT st dom XFS = card X & ( for n being Nat st n in dom XFS holds

XFS . n = ((- 1) |^ n) * (Card_Intersection (Fy,(n + 1))) ) holds

card (union (rng Fy)) = Sum XFS

proof end;

theorem Th56: :: CARD_FIN:57

for Fy being finite-yielding Function

for X being finite set

for n, k being Nat st dom Fy = X & ex x, y being set st

( x <> y & ( for f being Function st f in Choose (X,k,x,y) holds

card (Intersection (Fy,f,x)) = n ) ) holds

Card_Intersection (Fy,k) = n * ((card X) choose k)

for X being finite set

for n, k being Nat st dom Fy = X & ex x, y being set st

( x <> y & ( for f being Function st f in Choose (X,k,x,y) holds

card (Intersection (Fy,f,x)) = n ) ) holds

Card_Intersection (Fy,k) = n * ((card X) choose k)

proof end;

theorem Th57: :: CARD_FIN:58

for Fy being finite-yielding Function

for X being finite set st dom Fy = X holds

for XF being XFinSequence of NAT st dom XF = card X & ( for n being Nat st n in dom XF holds

ex x, y being set st

( x <> y & ( for f being Function st f in Choose (X,(n + 1),x,y) holds

card (Intersection (Fy,f,x)) = XF . n ) ) ) holds

ex F being XFinSequence of INT st

( dom F = card X & card (union (rng Fy)) = Sum F & ( for n being Nat st n in dom F holds

F . n = (((- 1) |^ n) * (XF . n)) * ((card X) choose (n + 1)) ) )

for X being finite set st dom Fy = X holds

for XF being XFinSequence of NAT st dom XF = card X & ( for n being Nat st n in dom XF holds

ex x, y being set st

( x <> y & ( for f being Function st f in Choose (X,(n + 1),x,y) holds

card (Intersection (Fy,f,x)) = XF . n ) ) ) holds

ex F being XFinSequence of INT st

( dom F = card X & card (union (rng Fy)) = Sum F & ( for n being Nat st n in dom F holds

F . n = (((- 1) |^ n) * (XF . n)) * ((card X) choose (n + 1)) ) )

proof end;

Lm3: 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)) ) )

proof end;

:: onto

theorem Th58: :: CARD_FIN:59

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) + 1 & 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)) * (((card Y) - n) |^ (card X)) ) )

ex F being XFinSequence of INT st

( dom F = (card Y) + 1 & 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)) * (((card Y) - n) |^ (card X)) ) )

proof end;

:: n block k

theorem :: CARD_FIN:60

for n, k being Nat st k <= n holds

ex F being XFinSequence of INT st

( n block k = (1 / (k !)) * (Sum F) & dom F = k + 1 & ( for m being Nat st m in dom F holds

F . m = (((- 1) |^ m) * (k choose m)) * ((k - m) |^ n) ) )

ex F being XFinSequence of INT st

( n block k = (1 / (k !)) * (Sum F) & dom F = k + 1 & ( for m being Nat st m in dom F holds

F . m = (((- 1) |^ m) * (k choose m)) * ((k - m) |^ n) ) )

proof end;

theorem Th60: :: CARD_FIN:61

for X1, Y1, X being finite set st ( Y1 is empty implies X1 is empty ) & X c= X1 holds

for F being Function of X1,Y1 st F is one-to-one & card X1 = card Y1 holds

((card X1) -' (card X)) ! = card { f where f is Function of X1,Y1 : ( f is one-to-one & rng (f | (X1 \ X)) c= F .: (X1 \ X) & ( for x being set st x in X holds

f . x = F . x ) ) }

for F being Function of X1,Y1 st F is one-to-one & card X1 = card Y1 holds

((card X1) -' (card X)) ! = card { f where f is Function of X1,Y1 : ( f is one-to-one & rng (f | (X1 \ X)) c= F .: (X1 \ X) & ( for x being set st x in X holds

f . x = F . x ) ) }

proof end;

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

proof end;

theorem Th61: :: CARD_FIN:62

for X being finite set

for F being Function st dom F = X & F is one-to-one holds

ex XF being XFinSequence of INT st

( 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 ) ) } & dom XF = (card X) + 1 & ( for n being Nat st n in dom XF holds

XF . n = (((- 1) |^ n) * ((card X) !)) / (n !) ) )

for F being Function st dom F = X & F is one-to-one holds

ex XF being XFinSequence of INT st

( 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 ) ) } & dom XF = (card X) + 1 & ( for n being Nat st n in dom XF holds

XF . n = (((- 1) |^ n) * ((card X) !)) / (n !) ) )

proof end;

:: disorders

theorem :: CARD_FIN:63

for X being finite set ex XF being XFinSequence of INT st

( Sum XF = card { h where h is Function of X,X : ( h is one-to-one & ( for x being set st x in X holds

h . x <> x ) ) } & dom XF = (card X) + 1 & ( for n being Nat st n in dom XF holds

XF . n = (((- 1) |^ n) * ((card X) !)) / (n !) ) )

( Sum XF = card { h where h is Function of X,X : ( h is one-to-one & ( for x being set st x in X holds

h . x <> x ) ) } & dom XF = (card X) + 1 & ( for n being Nat st n in dom XF holds

XF . n = (((- 1) |^ n) * ((card X) !)) / (n !) ) )

proof end;