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