:: Cardinal Numbers and Finite Sets :: by Karol P\c{a}k :: :: Received May 24, 2005 :: Copyright (c) 2005-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SUBSET_1, FUNCT_1, NAT_1, TARSKI, FINSET_1, RELAT_1, AFINSQ_1, ARYTM_1, ARYTM_3, FINSEQ_1, XXREAL_0, CARD_1, XBOOLE_0, ORDINAL4, CARD_3, BINOP_1, FINSOP_1, FUNCOP_1, BINOP_2, FUNCT_2, INT_1, VALUED_1, NEWTON, REALSET1, ZFMISC_1, FUNCT_4, EQREL_1, SETFAM_1, STIRL2_1, CARD_FIN; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, RELAT_1, FUNCT_1, XCMPLX_0, NAT_1, FINSET_1, XXREAL_0, NAT_D, AFINSQ_1, VALUED_1, RELSET_1, PARTFUN1, DOMAIN_1, FUNCT_2, FUNCT_4, FUNCOP_1, INT_1, ENUMSET1, BINOP_1, BINOP_2, RECDEF_1, AFINSQ_2, ZFMISC_1, NEWTON, STIRL2_1, YELLOW20; constructors PARTFUN3, BINOM, WELLORD2, DOMAIN_1, SETWISEO, REAL_1, NAT_D, YELLOW20, RECDEF_1, BINOP_2, RELSET_1, ORDINAL4, AFINSQ_1, SEQ_4, AFINSQ_2, STIRL2_1, NUMBERS, NEWTON; registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2, FUNCOP_1, FUNCT_4, FINSET_1, FRAENKEL, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, BINOP_2, CARD_1, WSIERP_1, AFINSQ_1, RELSET_1, VALUED_1, VALUED_0, AFINSQ_2, NEWTON; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin reserve x, x1, x2, y, z, X9 for set, X, Y for finite set, n, k, m for Nat, f for Function; ::$CT theorem :: CARD_FIN:2 for X,Y,x,y 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}; theorem :: CARD_FIN:3 for X,Y,x,y 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}; :: card Funcs(X,Y) theorem :: CARD_FIN:4 (Y={} implies X={}) implies card Funcs(X,Y) = card Y |^ card X; theorem :: CARD_FIN:5 for X,Y,x,y 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}; theorem :: CARD_FIN:6 n!/((n-'k)!) is Element of NAT; :: one-to-one theorem :: CARD_FIN:7 card X <= card Y implies card {F where F is Function of X,Y:F is one-to-one} = card Y!/((card Y-'card X)!); :: Permutation of X theorem :: CARD_FIN:8 card{F where F is Function of X,X:F is Permutation of X}=card X!; definition let X,k; let x1,x2 be object; func Choose(X,k,x1,x2) -> Subset of Funcs(X,{x1,x2}) means :: CARD_FIN:def 1 x in it iff ex f be Function of X,{x1,x2} st f = x & card (f"{x1})=k; end; theorem :: CARD_FIN:9 card X<>k implies Choose(X,k,x1,x1) is empty; theorem :: CARD_FIN:10 for x1,x2 being object holds card X < k implies Choose(X,k,x1,x2) is empty; theorem :: CARD_FIN:11 for x1,x2 being object holds x1<>x2 implies card Choose(X,0,x1,x2)=1; theorem :: CARD_FIN:12 for x1,x2 being object holds card Choose(X,card X,x1,x2)=1; theorem :: CARD_FIN:13 for z,x,y being object holds not z in X implies 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}; theorem :: CARD_FIN:14 for z,x,y being object holds not z in X & x<>y implies card Choose(X,k,x,y)= card{f where f is Function of X\/{z},{x,y}:card (f"{x})=k & f.z=y}; theorem :: CARD_FIN:15 for z,x,y being object holds x<>y & not z in X implies card Choose(X\/{z},k+1,x,y)= card Choose(X,k+1,x,y)+ card Choose(X,k,x,y); :: n choose k ::$N Formula for the Number of Combinations theorem :: CARD_FIN:16 for x,y being object holds x<>y implies card Choose(X,k,x,y)=card X choose k; theorem :: CARD_FIN:17 for x,y being object holds x<>y implies (Y-->y)+*(X-->x) in Choose(X\/Y,card X,x,y); theorem :: CARD_FIN:18 x<>y & X misses Y implies (X-->x)+*(Y-->y) in Choose(X\/Y,card X ,x,y); definition let F,Ch be Function,y be object; func Intersection(F,Ch,y) -> Subset of union rng F means :: CARD_FIN:def 2 z in it iff z in union rng F & for x st x in dom Ch & Ch.x=y holds z in F.x; end; reserve F,Ch for Function; theorem :: CARD_FIN:19 for F,Ch st dom F/\Ch"{x} is non empty holds y in Intersection(F ,Ch,x) iff for z st z in dom Ch & Ch.z=x holds y in F.z; theorem :: CARD_FIN:20 Intersection(F,Ch,y) is non empty implies Ch"{y} c= dom F; theorem :: CARD_FIN:21 Intersection(F,Ch,y) is non empty implies for x1,x2 st x1 in Ch"{y} & x2 in Ch"{y} holds F.x1 meets F.x2; theorem :: CARD_FIN:22 z in Intersection(F,Ch,y) & y in rng Ch implies ex x st x in dom Ch & Ch.x=y & z in F.x; theorem :: CARD_FIN:23 F is empty or union rng F is empty implies Intersection(F,Ch,y)=union rng F; theorem :: CARD_FIN:24 for y being object holds F|Ch"{y}=(Ch"{y}-->union rng F) implies Intersection(F,Ch,y) = union rng F; theorem :: CARD_FIN:25 union rng F is non empty & Intersection(F,Ch,y)=union rng F implies F| Ch"{y}=(Ch"{y}-->union rng F); theorem :: CARD_FIN:26 for y being object holds Intersection(F,{},y)=union rng F; theorem :: CARD_FIN:27 for y being object holds Intersection(F,Ch,y) c= Intersection(F,Ch|X9,y); theorem :: CARD_FIN:28 Ch"{y}=(Ch|X9)"{y} implies Intersection(F,Ch,y)=Intersection(F, Ch|X9,y); theorem :: CARD_FIN:29 Intersection(F|X9,Ch,y) c= Intersection(F,Ch,y); theorem :: CARD_FIN:30 y in rng Ch & Ch"{y} c= X9 implies Intersection(F|X9,Ch,y) = Intersection(F,Ch,y); theorem :: CARD_FIN:31 for x,y being object holds x in Ch"{y} implies Intersection(F,Ch,y) c= F.x; theorem :: CARD_FIN:32 for x,y being object holds x in Ch"{y} implies Intersection(F,Ch|(dom Ch\{x}),y)/\F.x= Intersection(F,Ch,y); theorem :: CARD_FIN:33 for x1,x2 being object for Ch1,Ch2 be Function st Ch1"{x1}=Ch2"{x2} holds Intersection( F,Ch1,x1)=Intersection(F,Ch2,x2); theorem :: CARD_FIN:34 for y being object holds Ch"{y}={} implies Intersection(F,Ch,y)=union rng F; theorem :: CARD_FIN:35 for x,y being object holds {x}=Ch"{y} implies Intersection(F,Ch,y)=F.x; theorem :: CARD_FIN:36 {x1,x2}=Ch"{y} implies Intersection(F,Ch,y)=F.x1 /\ F.x2; theorem :: CARD_FIN:37 for F st F is non empty holds y in Intersection(F,(dom F-->x),x) iff for z st z in dom F holds y in F.z; registration let F be finite-yielding Function,X be set; cluster F|X -> finite-yielding; end; registration let F be finite-yielding Function,G be Function; cluster F*G -> finite-yielding; cluster Intersect(F,G) -> finite-yielding; end; reserve Fy for finite-yielding Function; theorem :: CARD_FIN:38 y in rng Ch implies Intersection(Fy,Ch,y) is finite; theorem :: CARD_FIN:39 dom Fy is finite implies union rng Fy is finite; theorem :: CARD_FIN:40 x in Choose(n,k,1,0) iff ex F be XFinSequence of NAT st F = x & dom F = n & rng F c= {0,1} & Sum F=k; definition ::$CD let k; let F be finite-yielding Function; assume dom F is finite; func Card_Intersection(F,k) -> Element of NAT means :: CARD_FIN:def 4 for x,y be object,X be finite set, P be Function of card Choose(X,k,x,y),Choose(X,k,x,y) st dom F=X & P is one-to-one & x<>y ex XFS be XFinSequence of NAT st dom XFS=dom P & (for z,f st z in dom XFS & f=P.z holds XFS.z=card(Intersection(F,f,x))) & it=Sum XFS ; end; theorem :: CARD_FIN:41 for x,y be set,X be finite set, P be Function of card Choose(X,k,x,y), Choose(X,k,x,y) st dom Fy=X & P is one-to-one & x<>y for XFS be XFinSequence of NAT st dom XFS=dom P & (for z,f 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:42 dom Fy is finite & k=0 implies Card_Intersection(Fy,k)=card (union rng Fy); theorem :: CARD_FIN:43 dom Fy=X & k > card X implies Card_Intersection(Fy,k)=0; theorem :: CARD_FIN:44 for Fy,X st dom Fy=X for P be Function of card X,X st P is one-to-one holds ex XFS be XFinSequence of NAT st dom XFS=card X & (for z st z in dom XFS holds XFS.z=card ((Fy*P).z))& Card_Intersection(Fy,1)=Sum XFS; theorem :: CARD_FIN:45 for x being object holds dom Fy=X implies Card_Intersection(Fy,card X)=card Intersection( Fy,X-->x,x); theorem :: CARD_FIN:46 for x being object holds Fy=x.-->X implies Card_Intersection(Fy,1)=card X; theorem :: CARD_FIN:47 x<>y & Fy=(x,y)-->(X,Y) implies Card_Intersection(Fy,1)=card X + card Y & Card_Intersection(Fy,2)=card (X/\Y); theorem :: CARD_FIN:48 for Fy,x st dom Fy is finite & x in dom Fy holds Card_Intersection(Fy,1)=Card_Intersection(Fy|(dom Fy\{x}),1)+ card (Fy.x); theorem :: CARD_FIN:49 dom Intersect(F,dom F-->X9)=dom F & for x st x in dom F holds Intersect(F,dom F-->X9).x = F.x /\ X9; theorem :: CARD_FIN:50 (union rng F)/\X9=union rng Intersect(F,dom F-->X9); theorem :: CARD_FIN:51 Intersection(F,Ch,y)/\X9= Intersection(Intersect(F,dom F-->X9), Ch,y); theorem :: CARD_FIN:52 for F, G be XFinSequence st F is one-to-one & G is one-to-one & rng F misses rng G holds F^G is one-to-one; theorem :: CARD_FIN:53 for Fy,X,x,n 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); theorem :: CARD_FIN:54 x in dom F implies union rng F=union rng (F|(dom F\{x}))\/F.x; theorem :: CARD_FIN:55 for Fy be finite-yielding Function,X ex XFS be XFinSequence of INT st dom XFS = card X & for n st n in dom XFS holds XFS.n=((-1)|^n)* Card_Intersection(Fy,n+1); :: The principle of inclusions and the disconnections ::$N Principle of Inclusion/Exclusion theorem :: CARD_FIN:56 for Fy be finite-yielding Function,X st dom Fy=X for XFS be XFinSequence of INT st dom XFS= card X & for n st n in dom XFS holds XFS.n=((-1 )|^n)*Card_Intersection(Fy,n+1) holds card union rng Fy=Sum XFS; theorem :: CARD_FIN:57 for Fy,X,n,k st dom Fy=X holds (ex x,y st x<>y & for f st f in Choose(X,k,x,y) holds card(Intersection(Fy,f,x))=n) implies Card_Intersection( Fy,k)=n*(card X choose k); theorem :: CARD_FIN:58 for Fy,X st dom Fy=X for XF be XFinSequence of NAT st dom XF= card X & for n st n in dom XF holds ex x,y st x<>y & for f st f in Choose(X,n+1 ,x,y) holds card(Intersection(Fy,f,x))=XF.n holds ex F be XFinSequence of INT st dom F=card X & card union rng Fy = Sum F & for n st n in dom F holds F.n=((- 1)|^n)*XF.n*(card X choose (n+1)); :: onto theorem :: CARD_FIN:59 for X,Y be finite set st X is non empty & Y is non empty ex F be 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 st n in dom F holds F.n=((-1)|^n)*(card Y choose n)*( (card Y-n) |^ card X); :: n block k theorem :: CARD_FIN:60 for n,k st k <= n ex F be XFinSequence of INT st n block k = 1/(k!) * Sum F & dom F = k+1 & for m st m in dom F holds F.m=((-1)|^m)*(k choose m)*((k- m) |^ n); theorem :: CARD_FIN:61 for X1,Y1,X be finite set st (Y1 is empty implies X1 is empty) & X c= X1 for F be 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 st x in X holds f.x=F.x}; theorem :: CARD_FIN:62 for F be Function st dom F=X & F is one-to-one ex XF be XFinSequence of INT st Sum XF=card {h where h is Function of X,rng F: h is one-to-one & for x st x in X holds h.x<>F.x}& dom XF = card X +1 & for n st n in dom XF holds XF.n=((-1)|^n)*(card X!)/(n!); :: disorders theorem :: CARD_FIN:63 ex XF be XFinSequence of INT st Sum XF=card {h where h is Function of X,X: h is one-to-one & for x st x in X holds h.x<>x}& dom XF = card X+1 & for n st n in dom XF holds XF.n=((-1)|^n)*(card X!)/(n!);