### The Mizar article:

### Partial Functions

**by****Czeslaw Bylinski**

- Received September 18, 1989
Copyright (c) 1989 Association of Mizar Users

- MML identifier: PARTFUN1
- [ MML identifier index ]

environ vocabulary BOOLE, FUNCT_1, RELAT_1, PARTFUN1, RELAT_2; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2, RELSET_1, FUNCT_1; constructors TARSKI, FUNCT_1, RELSET_1, RELAT_2, XBOOLE_0; clusters RELAT_1, FUNCT_1, RELSET_1, SUBSET_1, ZFMISC_1, XBOOLE_0; requirements SUBSET, BOOLE; definitions TARSKI, FUNCT_1, XBOOLE_0, RELAT_2; theorems TARSKI, FUNCT_1, GRFUNC_1, ZFMISC_1, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, RELAT_2; schemes FUNCT_1, XBOOLE_0; begin reserve p,x,x1,x2,y,y',y1,y2,z,z1,z2,P,Q,X,X1,X2,Y,Y1,Y2,V,Z for set; :::::::::::::::::::::::: :: Auxiliary theorems :: :::::::::::::::::::::::: theorem Th1: P c= [:X1,Y1:] & Q c= [:X2,Y2:] implies P \/ Q c= [:X1 \/ X2,Y1 \/ Y2:] proof X1 c= X1 \/ X2 & Y2 c= Y1 \/ Y2 & X2 c= X1 \/ X2 & Y1 c= Y1 \/ Y2 by XBOOLE_1:7; then [:X1,Y1:] c= [:X1 \/ X2,Y1 \/ Y2:] & [:X2,Y2:] c= [:X1 \/ X2,Y1 \/ Y2:] & [:X1 \/ X2,Y1 \/ Y2:] \/ [:X1 \/ X2,Y1 \/ Y2:] = [:X1 \/ X2,Y1 \/ Y2:] by ZFMISC_1:119; then A1: [:X1,Y1:] \/ [:X2,Y2:] c= [:X1 \/ X2,Y1 \/ Y2:] by XBOOLE_1:13; assume P c= [:X1,Y1:] & Q c= [:X2,Y2:]; then P \/ Q c= [:X1,Y1:] \/ [:X2,Y2:] by XBOOLE_1:13; hence thesis by A1,XBOOLE_1:1; end; theorem Th2: for f,g being Function st for x st x in dom f /\ dom g holds f.x = g.x ex h being Function st f \/ g = h proof let f,g be Function such that A1: for x st x in dom f /\ dom g holds f.x = g.x; defpred P[set,set] means [$1,$2] in f \/ g; A2: for x,y1,y2 st P[x,y1] & P[x,y2] holds y1 = y2 proof let x,y1,y2 such that A3: [x,y1] in f \/ g and A4: [x,y2] in f \/ g; now A5: [x,y1] in f or [x,y1] in g by A3,XBOOLE_0:def 2; A6: [x,y2] in f or [x,y2] in g by A4,XBOOLE_0:def 2; then A7: (x in dom f & f.x = y1 or x in dom g & g.x = y1) & (x in dom f & f.x = y2 or x in dom g & g.x = y2) by A5,FUNCT_1:8; per cases by A6,RELAT_1:def 4; suppose x in dom f & x in dom g; then x in dom f /\ dom g by XBOOLE_0:def 3; hence y1 = y2 by A1,A7; suppose x in dom f & not x in dom g; hence y1 = y2 by A7; suppose not x in dom f & x in dom g; hence y1 = y2 by A7; end; hence y1 = y2; end; consider h being Function such that A8: for x,y holds [x,y] in h iff x in dom f \/ dom g & P[x,y] from GraphFunc(A2); take h; f c= [:dom f,rng f:] & g c= [:dom g,rng g:] by RELAT_1:21; then A9: h c= [:dom h,rng h:] & f \/ g c= [:dom f \/ dom g,rng f \/ rng g:] by Th1,RELAT_1:21; now let x,y; thus [x,y] in f \/ g implies [x,y] in h proof assume A10: [x,y] in f \/ g; then [x,y] in f or [x,y] in g by XBOOLE_0:def 2; then x in dom f or x in dom g by RELAT_1:def 4; then x in dom f \/ dom g by XBOOLE_0:def 2; hence [x,y] in h by A8,A10; end; thus [x,y] in h implies [x,y] in f \/ g by A8; end; hence thesis by A9,ZFMISC_1:110; end; theorem Th3: for f,g,h being Function st f \/ g = h for x st x in dom f /\ dom g holds f.x = g.x proof let f,g,h be Function such that A1: f \/ g = h; let x; assume x in dom f /\ dom g; then x in dom f & x in dom g by XBOOLE_0:def 3; then h.x = f.x & h.x = g.x by A1,GRFUNC_1:34; hence thesis; end; scheme LambdaC{A()->set,C[set],F(set)->set,G(set)->set}: ex f being Function st dom f = A() & for x st x in A() holds (C[x] implies f.x = F(x)) & (not C[x] implies f.x = G(x)) proof defpred P[set,set] means (C[$1] implies $2 = F($1)) & (not C[$1] implies $2 = G($1)); A1: for x,y1,y2 st x in A() & P[x,y1] & P[x,y2] holds y1 = y2; A2: for x st x in A() ex y st P[x,y] proof let x; not C[x] implies (C[x] implies G(x) = F(x)) & (not C[x] implies G(x) = G(x)); hence thesis; end; thus ex f being Function st dom f = A() & for x st x in A() holds P[x,f.x] from FuncEx(A1,A2); end; :::::::::::::::::::: :: Empty Function :: :::::::::::::::::::: definition cluster empty Function; existence proof {} is Function; hence thesis; end; end; Lm1: dom {} = {}; canceled 6; theorem Th10: rng {} = {}; Lm2: now let X,Y; reconsider E = {} as Function; take E; thus dom E c= X & rng E c= Y by Lm1,Th10,XBOOLE_1:2; end; Lm3: for R be Relation holds R is Relation of X,Y iff dom R c= X & rng R c= Y proof let R be Relation; thus R is Relation of X,Y implies dom R c= X & rng R c= Y by RELSET_1:12; thus thesis by RELSET_1:11; end; definition let X,Y; cluster Function-like Relation of X,Y; existence proof consider E being Function such that A1: dom E c= X & rng E c= Y by Lm2; reconsider E as Relation of X,Y by A1,Lm3; take E; thus thesis; end; end; definition let X,Y; mode PartFunc of X,Y is Function-like Relation of X,Y; end; canceled 13; theorem for f being Function holds f is PartFunc of dom f, rng f by Lm3; theorem for f being Function st rng f c= Y holds f is PartFunc of dom f, Y by Lm3; theorem for f being PartFunc of X,Y st y in rng f ex x being Element of X st x in dom f & y = f.x proof let f be PartFunc of X,Y; assume y in rng f; then consider x such that A1: x in dom f and A2: y = f.x by FUNCT_1:def 5; thus thesis by A1,A2; end; theorem Th27: for f being PartFunc of X,Y st x in dom f holds f.x in Y proof let f be PartFunc of X,Y; assume x in dom f; then f.x in rng f & rng f c= Y by Lm3,FUNCT_1:def 5; hence f.x in Y; end; theorem for f being PartFunc of X,Y st dom f c= Z holds f is PartFunc of Z,Y proof let f be PartFunc of X,Y; assume dom f c= Z; then dom f c= Z & rng f c= Y by Lm3; hence thesis by Lm3; end; theorem for f being PartFunc of X,Y st rng f c= Z holds f is PartFunc of X,Z proof let f be PartFunc of X,Y; assume rng f c= Z; then dom f c= X & rng f c= Z; hence thesis by Lm3; end; theorem Th30: for f being PartFunc of X,Y st X c= Z holds f is PartFunc of Z,Y proof let f be PartFunc of X,Y; assume X c= Z; then dom(f) c= Z & rng(f) c= Y by Lm3,XBOOLE_1:1; hence thesis by Lm3; end; theorem Th31: for f being PartFunc of X,Y st Y c= Z holds f is PartFunc of X,Z proof let f be PartFunc of X,Y such that A1: Y c= Z; A2: dom(f) c= X; rng f c= Y by Lm3; then rng f c= Z by A1,XBOOLE_1:1; hence thesis by A2,Lm3; end; theorem Th32: for f being PartFunc of X1,Y1 st X1 c= X2 & Y1 c= Y2 holds f is PartFunc of X2,Y2 proof let f be PartFunc of X1,Y1; assume A1: X1 c= X2 & Y1 c= Y2; dom(f) c= X1 & rng f c= Y1 by Lm3; then dom(f) c= X2 & rng f c= Y2 by A1,XBOOLE_1:1; hence thesis by Lm3; end; theorem for f being Function,g being PartFunc of X,Y st f c= g holds f is PartFunc of X,Y proof let f be Function,g be PartFunc of X,Y; assume f c= g; then dom f c= dom g & rng f c= rng g & dom g c= X & rng g c= Y by Lm3,RELAT_1:25; then dom f c= X & rng f c= Y by XBOOLE_1:1; hence thesis by Lm3; end; theorem for f1,f2 being PartFunc of X,Y st dom f1 = dom f2 & for x being Element of X st x in dom f1 holds f1.x = f2.x holds f1 = f2 proof let f1,f2 be PartFunc of X,Y such that A1: dom f1 = dom f2 and A2: for x being Element of X st x in dom f1 holds f1.x = f2.x; for x st x in dom f1 holds f1.x = f2.x by A2; hence thesis by A1,FUNCT_1:9; end; theorem for f1,f2 being PartFunc of [:X,Y:],Z st dom f1 = dom f2 & for x,y st [x,y] in dom f1 holds f1.[x,y]=f2.[x,y] holds f1 = f2 proof let f1,f2 be PartFunc of [:X,Y:],Z such that A1: dom f1 = dom f2 and A2: for x,y st [x,y] in dom f1 holds f1.[x,y] = f2.[x,y]; z in dom f1 implies f1.z = f2.z proof assume A3: z in dom f1; then ex x,y st x in X & y in Y & z = [x,y] by ZFMISC_1:def 2; hence thesis by A2,A3; end; hence thesis by A1,FUNCT_1:9; end; scheme PartFuncEx{X,Y()->set,P[set,set]}: ex f being PartFunc of X(),Y() st (for x holds x in dom f iff x in X() & ex y st P[x,y]) & (for x st x in dom f holds P[x,f.x]) provided A1: for x,y st x in X() & P[x,y] holds y in Y() and A2: for x,y1,y2 st x in X() & P[x,y1] & P[x,y2] holds y1 = y2 proof A3: now assume A4: Y() = {}; consider f being Function such that A5: dom f c= X() and A6: rng f c= Y() by Lm2; reconsider f as PartFunc of X(),Y() by A5,A6,Lm3; take f; rng f c= {} by A4,Lm3; then A7: rng f = {} by XBOOLE_1:3; hence for x holds x in dom f iff x in X() & ex y st P[x,y] by A1,A4, RELAT_1:65; thus for x st x in dom f holds P[x,f.x] by A7,RELAT_1:65; end; now assume Y() <> {}; consider y1; defpred Q[set,set] means ((ex y st P[$1,y]) implies P[$1,$2]) & ((for y holds not P[$1,y]) implies $2=y1); A8: for x st x in X() ex z st Q[x,z] proof let x such that x in X(); (for y holds not P[x,y]) implies ((ex y st P[x,y]) implies P[x,y1]) & ((for y holds not P[x,y]) implies y1=y1); hence thesis; end; A9: for x,z1,z2 st x in X() & Q[x,z1] & Q[x,z2] holds z1 = z2 by A2; consider g being Function such that A10: dom g = X() and A11: for x st x in X() holds Q[x,g.x] from FuncEx(A9,A8); defpred R[set] means ex y st P[$1,y]; consider X being set such that A12: for x holds x in X iff x in X() & R[x] from Separation; set f=g|X; A13: dom f c= X() by A10,FUNCT_1:76; rng f c= Y() proof let y; assume y in rng f; then consider x such that A14: x in dom f and A15: y = f.x by FUNCT_1:def 5; dom f c= X by RELAT_1:87; then x in X() & ex y st P[x,y] by A12,A14; then x in X() & P[x,g.x] by A11; then x in X() & P[x,y] by A14,A15,FUNCT_1:70; hence thesis by A1; end; then reconsider f as PartFunc of X(),Y() by A13,Lm3; take f; thus for x holds x in dom f iff x in X() & ex y st P[x,y] proof let x; dom f c= X by RELAT_1:87; hence x in dom f implies x in X() & ex y st P[x,y] by A12; assume x in X() & ex y st P[x,y]; then x in X & x in dom g by A10,A12; then x in dom g /\ X by XBOOLE_0:def 3; hence thesis by RELAT_1:90; end; let x; assume A16: x in dom f; dom f c= X by RELAT_1:87; then x in X() & ex y st P[x,y] by A12,A16; then P[x,g.x] by A11; hence P[x,f.x] by A16,FUNCT_1:70; end; hence thesis by A3; end; scheme LambdaR{X,Y()->set,F(set)->set,P[set]}: ex f being PartFunc of X(),Y() st (for x holds x in dom f iff x in X() & P[x]) & (for x st x in dom f holds f.x = F(x)) provided A1: for x st P[x] holds F(x) in Y() proof defpred Q[set,set] means P[$1] & $2 = F($1); A2: for x,y st x in X() & Q[x,y] holds y in Y() by A1; A3: for x,y1,y2 st x in X() & Q[x,y1] & Q[x,y2] holds y1 = y2; consider f being PartFunc of X(),Y() such that A4: for x holds x in dom f iff x in X() & ex y st Q[x,y] and A5: for x st x in dom f holds Q[x,f.x] from PartFuncEx(A2,A3); take f; thus for x holds x in dom f iff x in X() & P[x] proof let x; thus x in dom f implies x in X() & P[x] proof assume x in dom f; then x in X() & ex y st P[x] & y = F(x) by A4; hence thesis; end; assume x in X() & P[x]; then x in X() & ex y st P[x] & y = F(x); hence thesis by A4; end; thus thesis by A5; end; scheme PartFuncEx2{X,Y,Z()->set,P[set,set,set]}: ex f being PartFunc of [:X(),Y():],Z() st (for x,y holds [x,y] in dom f iff x in X() & y in Y() & ex z st P[x,y,z]) & (for x,y st [x,y] in dom f holds P[x,y,f.[x,y]]) provided A1: for x,y,z st x in X() & y in Y() & P[x,y,z] holds z in Z() and A2: for x,y,z1,z2 st x in X() & y in Y() & P[x,y,z1] & P[x,y,z2] holds z1 = z2 proof defpred Q[set,set] means for x1,y1 st $1 = [x1,y1] holds P[x1,y1,$2]; A3: for x,z st x in [:X(),Y():] & Q[x,z] holds z in Z() proof let x,z; assume x in [:X(),Y():]; then consider x1,y1 such that A4: x1 in X() & y1 in Y() and A5: x = [x1,y1] by ZFMISC_1:def 2; assume for x1,y1 st x = [x1,y1] holds P[x1,y1,z]; then P[x1,y1,z] by A5; hence z in Z() by A1,A4; end; A6: for x,z1,z2 st x in [:X(),Y():] & Q[x,z1] & Q[x,z2] holds z1 = z2 proof let x,z1,z2 such that A7: x in [:X(),Y():] and A8: (for x1,y1 st x = [x1,y1] holds P[x1,y1,z1]) and A9: (for x1,y1 st x = [x1,y1] holds P[x1,y1,z2]); consider x1,y1 such that A10: x1 in X() & y1 in Y() and A11: x = [x1,y1] by A7,ZFMISC_1:def 2; P[x1,y1,z1] & P[x1,y1,z2] by A8,A9,A11; hence thesis by A2,A10; end; consider f being PartFunc of [:X(),Y():],Z() such that A12: for x holds x in dom f iff x in [:X(),Y():] & ex z st Q[x,z] and A13: for x st x in dom f holds Q[x,f.x] from PartFuncEx(A3,A6); take f; thus for x,y holds [x,y] in dom f iff x in X() & y in Y() & ex z st P[x,y,z] proof let x,y; thus [x,y] in dom f implies x in X() & y in Y() & ex z st P[x,y,z] proof assume A14: [x,y] in dom f; hence x in X() & y in Y() by ZFMISC_1:106; consider z such that A15: for x1,y1 st [x,y] = [x1,y1] holds P[x1,y1,z] by A12,A14; take z; thus thesis by A15; end; assume x in X() & y in Y(); then A16: [x,y] in [:X(),Y():] by ZFMISC_1:def 2; given z such that A17: P[x,y,z]; now take z; let x1,y1; assume [x,y] = [x1,y1]; then x=x1 & y=y1 by ZFMISC_1:33; hence P[x1,y1,z] by A17; end; hence thesis by A12,A16; end; thus thesis by A13; end; scheme LambdaR2{X,Y,Z()->set,F(set,set)->set,P[set,set]}: ex f being PartFunc of [:X(),Y():],Z() st (for x,y holds [x,y] in dom f iff x in X() & y in Y() & P[x,y]) & (for x,y st [x,y] in dom f holds f.[x,y] = F(x,y)) provided A1: for x,y st P[x,y] holds F(x,y) in Z() proof defpred Q[set,set,set] means P[$1,$2] & $3 = F($1,$2); A2: for x,y,z st x in X() & y in Y() & Q[x,y,z] holds z in Z() by A1; A3: for x,y,z1,z2 st x in X() & y in Y() & Q[x,y,z1] & Q[x,y,z2] holds z1 = z2; consider f being PartFunc of [:X(),Y():],Z() such that A4: for x,y holds [x,y] in dom f iff x in X() & y in Y() & ex z st Q[x,y,z] and A5: for x,y st [x,y] in dom f holds Q[x,y,f.[x,y]] from PartFuncEx2(A2,A3); take f; thus for x,y holds [x,y] in dom f iff x in X() & y in Y() & P[x,y] proof let x,y; thus [x,y] in dom f implies x in X() & y in Y() & P[x,y] proof assume [x,y] in dom f; then x in X() & y in Y() & ex z st P[x,y] & z = F(x,y) by A4; hence thesis; end; assume x in X() & y in Y() & P[x,y]; then x in X() & y in Y() & ex z st P[x,y] & z = F(x,y); hence thesis by A4; end; thus thesis by A5; end; definition let X,Y,V,Z; let f be PartFunc of X,Y; let g be PartFunc of V,Z; redefine func g*f -> PartFunc of X,Z; coherence proof dom f c= X & dom(g*f) c= dom f & rng g c= Z & rng(g*f) c= rng g by Lm3,RELAT_1:44,45; then dom(g*f) c= X & rng(g*f) c= Z by XBOOLE_1:1; hence g*f is PartFunc of X,Z by Lm3; end; end; theorem for f being PartFunc of X,Y holds f*(id X) = f proof let f be PartFunc of X,Y; dom f c= X; hence thesis by RELAT_1:77; end; theorem for f being PartFunc of X,Y holds (id Y)*f = f proof let f be PartFunc of X,Y; rng f c= Y by Lm3; hence thesis by RELAT_1:79; end; theorem for f being PartFunc of X,Y st (for x1,x2 being Element of X st x1 in dom f & x2 in dom f & f.x1 = f.x2 holds x1 = x2) holds f is one-to-one proof let f be PartFunc of X,Y; assume for x1,x2 being Element of X st x1 in dom f & x2 in dom f & f.x1 = f.x2 holds x1 = x2; then for x1,x2 st x1 in dom f & x2 in dom f & f.x1 = f.x2 holds x1 = x2; hence thesis by FUNCT_1:def 8; end; theorem for f being PartFunc of X,Y st f is one-to-one holds f" is PartFunc of Y,X proof let f be PartFunc of X,Y such that A1: f is one-to-one; dom f c= X & rng f c= Y by Lm3; then dom(f") c= Y & rng(f") c= X by A1,FUNCT_1:55; hence thesis by Lm3; end; canceled 3; theorem for f being PartFunc of X,Y holds f|Z is PartFunc of Z,Y proof let f be PartFunc of X,Y; A1: dom(f|Z) c= Z by RELAT_1:87; rng(f|Z) c= Y by Lm3; hence thesis by A1,Lm3; end; theorem Th44: for f being PartFunc of X,Y holds f|Z is PartFunc of X,Y; definition let X,Y; let f be PartFunc of X,Y; let Z be set; redefine func f|Z -> PartFunc of X,Y; coherence by Th44; end; theorem for f being PartFunc of X,Y holds Z|f is PartFunc of X,Z proof let f be PartFunc of X,Y; dom(Z|f) c= X & rng(Z|f) c= Z by RELAT_1:116; hence thesis by Lm3; end; theorem for f being PartFunc of X,Y holds Z|f is PartFunc of X,Y; theorem Th47: for f being Function holds Y|f|X is PartFunc of X,Y proof let f be Function; Y|f|X = Y|(f|X) by RELAT_1:140; then dom(Y|f|X) c= X & rng(Y|f|X) c= Y by RELAT_1:87,116; hence thesis by Lm3; end; canceled; theorem for f being PartFunc of X,Y st y in f.:X holds ex x being Element of X st x in dom f & y = f.x proof let f be PartFunc of X,Y; assume y in f.:X; then consider x such that A1: x in dom f and x in X and A2: y = f.x by FUNCT_1:def 12; thus thesis by A1,A2; end; canceled; theorem for f being PartFunc of X,Y holds f.:X = rng f proof let f be PartFunc of X,Y; f.:(dom f) c= f.:X by RELAT_1:156; then rng f c= f.:X & f.:X c= rng f by RELAT_1:144,146; hence thesis by XBOOLE_0:def 10; end; canceled; theorem for f being PartFunc of X,Y holds f"Y = dom f proof let f be PartFunc of X,Y; rng f c= Y by Lm3; then f"(rng f) c= f"Y by RELAT_1:178; then dom f c= f"Y & f"Y c= dom f by RELAT_1:167,169; hence thesis by XBOOLE_0:def 10; end; :::::::::::::::::::::::::::: :: Empty Function :: :::::::::::::::::::::::::::: theorem Th54: for f being PartFunc of {},Y holds dom f = {} & rng f = {} proof let f be PartFunc of {},Y; thus dom f = {} by XBOOLE_1:3; hence thesis by RELAT_1:65; end; theorem Th55: for f being Function st dom f = {} holds f is PartFunc of X,Y proof let f be Function; assume A1: dom f = {}; then rng f = {} by RELAT_1:65; then dom f c= X & rng f c= Y by A1,XBOOLE_1:2; hence thesis by Lm3; end; theorem {} is PartFunc of X,Y by Lm1,Th55; theorem Th57: for f being PartFunc of {},Y holds f = {} proof let f be PartFunc of {},Y; dom f = {} & for x st x in {} holds f.x = {}.x by Th54; hence thesis by Lm1,FUNCT_1:9; end; theorem for f1 being PartFunc of {},Y1 for f2 being PartFunc of {},Y2 holds f1 = f2 proof let f1 be PartFunc of {},Y1; let f2 be PartFunc of {},Y2; f1 = {} & f2 = {} by Th57; hence thesis; end; theorem for f being PartFunc of {},Y holds f is one-to-one by Th57; theorem for f being PartFunc of {},Y holds f.:P = {} proof let f be PartFunc of {},Y; f = {} by Th57; hence thesis by RELAT_1:150 ; end; theorem for f being PartFunc of {},Y holds f"Q = {} proof let f be PartFunc of {},Y; f = {} by Th57; hence thesis by RELAT_1:172 ; end; theorem Th62: for f being PartFunc of X,{} holds dom f = {} & rng f = {} proof let f be PartFunc of X,{}; rng f c= {} by Lm3; then rng f = {} by XBOOLE_1:3; hence thesis by RELAT_1:65; end; theorem for f being Function st rng f = {} holds f is PartFunc of X,Y proof let f be Function; assume A1: rng f = {}; then dom f = {} by RELAT_1:65; then dom f c= X & rng f c= Y by A1,XBOOLE_1:2; hence thesis by Lm3; end; theorem Th64: for f being PartFunc of X,{} holds f = {} proof let f be PartFunc of X,{}; dom f = {} & for x st x in {} holds f.x = {}.x by Th62; hence thesis by Lm1,FUNCT_1:9; end; theorem for f1 being PartFunc of X1,{} for f2 being PartFunc of X2,{} holds f1 = f2 proof let f1 be PartFunc of X1,{}; let f2 be PartFunc of X2,{}; f1 = {} & f2 = {} by Th64; hence thesis; end; theorem for f being PartFunc of X,{} holds f is one-to-one by Th64; theorem for f being PartFunc of X,{} holds f.:P = {} proof let f be PartFunc of X,{}; f = {} by Th64; hence thesis by RELAT_1:150 ; end; theorem for f being PartFunc of X,{} holds f"Q = {} proof let f be PartFunc of X,{}; f = {} by Th64; hence thesis by RELAT_1:172 ; end; :::::::::::::::::::::::::::::::::::::::::::::::: :: Partial function from a singelton into set :: :::::::::::::::::::::::::::::::::::::::::::::::: theorem Th69: for f being PartFunc of {x},Y holds rng f c= {f.x} proof let f be PartFunc of {x},Y; dom f = {} or dom f = {x} by ZFMISC_1:39; then rng f = {} or rng f = {f.x} by FUNCT_1:14,RELAT_1:65; hence thesis by ZFMISC_1:39; end; theorem for f being PartFunc of {x},Y holds f is one-to-one proof let f be PartFunc of {x},Y; let x1,x2; assume x1 in dom f & x2 in dom f; then (dom f<>{} implies x1 = x & x2 = x) & dom f<>{} by TARSKI:def 1; hence f.x1 = f.x2 implies x1 = x2; end; theorem for f being PartFunc of {x},Y holds f.:P c= {f.x} proof let f be PartFunc of {x},Y; f.:P c= rng f & rng f c= {f.x} by Th69,RELAT_1:144; hence thesis by XBOOLE_1:1; end; theorem for f being Function st dom f = {x} & x in X & f.x in Y holds f is PartFunc of X,Y proof let f be Function; assume that A1: dom f = {x} and A2: x in X & f.x in Y; rng f = {f.x} by A1,FUNCT_1:14; then dom f c= X & rng f c= Y by A1,A2,ZFMISC_1:37; hence thesis by Lm3; end; :::::::::::::::::::::::::::::::::::::::::::::::::: :: Partial function from a set into a singelton :: :::::::::::::::::::::::::::::::::::::::::::::::::: theorem Th73: for f being PartFunc of X,{y} st x in dom f holds f.x = y proof let f be PartFunc of X,{y}; x in dom f implies f.x in {y} by Th27; hence thesis by TARSKI:def 1; end; theorem for f1,f2 being PartFunc of X,{y} st dom f1 = dom f2 holds f1 = f2 proof let f1,f2 be PartFunc of X,{y} such that A1: dom f1 = dom f2; x in dom f1 implies f1.x = f2.x proof assume x in dom f1; then f1.x = y & f2.x = y by A1,Th73; hence thesis; end; hence f1 = f2 by A1,FUNCT_1:9; end; :::::::::::::::::::::::::::::::::::::::::::::::::::::::: :: Construction of a Partial Function from a Function :: :::::::::::::::::::::::::::::::::::::::::::::::::::::::: definition let f be Function; let X,Y be set; canceled 2; func <:f,X,Y:> -> PartFunc of X,Y equals :Def3: Y|f|X; coherence by Th47; end; canceled; theorem Th76: for f being Function holds <:f,X,Y:> c= f proof let f be Function; <:f,X,Y:> = Y|f|X & (Y|f|X) c= (Y|f) & (Y|f) c= f by Def3,RELAT_1:88,117; hence thesis by XBOOLE_1:1; end; theorem Th77: for f being Function holds dom <:f,X,Y:> c= dom f & rng <:f,X,Y:> c= rng f proof let f be Function; <:f,X,Y:> c= f by Th76; hence thesis by RELAT_1:25; end; theorem Th78: for f being Function holds x in dom <:f,X,Y:> iff x in dom f & x in X & f.x in Y proof let f be Function; thus x in dom <:f,X,Y:> implies x in dom f & x in X & f.x in Y proof assume x in dom <:f,X,Y:>; then x in dom(Y|f|X) by Def3; then x in dom(Y|f) /\ X by RELAT_1:90; then x in X & x in dom(Y|f) by XBOOLE_0:def 3; hence x in dom f & x in X & f.x in Y by FUNCT_1:86; end; assume x in dom f & x in X & f.x in Y; then x in X & x in dom(Y|f) by FUNCT_1:86; then x in dom(Y|f) /\ X by XBOOLE_0:def 3; then x in dom(Y|f|X) by RELAT_1:90; hence thesis by Def3; end; theorem Th79: for f being Function st x in dom f & x in X & f.x in Y holds <:f,X,Y:>.x = f.x proof let f be Function such that A1: x in dom f and A2: x in X and A3: f.x in Y; x in dom(Y|f) by A1,A3,FUNCT_1:86; then f.x = (Y|f).x by FUNCT_1:87 .= (Y|f|X).x by A2,FUNCT_1:72; hence thesis by Def3; end; theorem Th80: for f being Function st x in dom <:f,X,Y:> holds <:f,X,Y:>.x = f.x proof let f be Function; assume x in dom <:f,X,Y:>; then x in dom f & x in X & f.x in Y by Th78; hence thesis by Th79; end; theorem for f,g being Function st f c= g holds <:f,X,Y:> c= <:g,X,Y:> proof let f,g be Function such that A1: f c= g; A2: dom <:f,X,Y:> c= dom f by Th77; now thus A3: dom <:f,X,Y:> c= dom <:g,X,Y:> proof let x; assume A4: x in dom <:f,X,Y:>; then x in dom f & dom f c= dom g & dom <:f,X,Y:> c= X by A1,A2,RELAT_1:25; then x in dom g & x in X & f.x in Y & f.x = g.x by A1,A4,Th78,GRFUNC_1:8; hence x in dom <:g,X,Y:> by Th78; end; let x; assume x in dom <:f,X,Y:>; then <:f,X,Y:>.x = f.x & <:g,X,Y:>.x = g.x & f.x = g.x by A1,A2,A3,Th80,GRFUNC_1:8; hence <:f,X,Y:>.x = <:g,X,Y:>.x; end; hence thesis by GRFUNC_1:8; end; theorem Th82: for f being Function st Z c= X holds <:f,Z,Y:> c= <:f,X,Y:> proof let f be Function such that A1: Z c= X; A2: dom <:f,Z,Y:> c= dom <:f,X,Y:> proof let x; assume A3: x in dom <:f,Z,Y:>; then x in Z; then x in dom f & x in X & f.x in Y by A1,A3,Th78; hence thesis by Th78; end; now let x; assume x in dom <:f,Z,Y:>; then <:f,Z,Y:>.x = f.x & x in dom <:f,X,Y:> by A2,Th80; hence <:f,Z,Y:>.x = <:f,X,Y:>.x by Th80; end; hence thesis by A2,GRFUNC_1:8; end; theorem Th83: for f being Function st Z c= Y holds <:f,X,Z:> c= <:f,X,Y:> proof let f be Function such that A1: Z c= Y; A2: dom <:f,X,Z:> c= dom <:f,X,Y:> proof let x; assume A3: x in dom <:f,X,Z:>; then f.x in Z by Th78; then x in dom f & x in X & f.x in Y by A1,A3,Th78; hence thesis by Th78; end; now let x; assume x in dom <:f,X,Z:>; then <:f,X,Z:>.x = f.x & x in dom <:f,X,Y:> by A2,Th80; hence <:f,X,Z:>.x = <:f,X,Y:>.x by Th80; end; hence thesis by A2,GRFUNC_1:8; end; theorem for f being Function st X1 c= X2 & Y1 c= Y2 holds <:f,X1,Y1:> c= <:f,X2,Y2:> proof let f be Function; assume X1 c= X2 & Y1 c= Y2; then <:f,X1,Y1:> c= <:f,X2,Y1:> & <:f,X2,Y1:> c= <:f,X2,Y2:> by Th82,Th83; hence thesis by XBOOLE_1:1; end; theorem Th85: for f being Function st dom f c= X & rng f c= Y holds f = <:f,X,Y:> proof let f be Function such that A1: dom f c= X and A2: rng f c= Y; A3: dom f c= dom <:f,X,Y:> proof let x; assume A4: x in dom f; then f.x in rng f by FUNCT_1:def 5; hence thesis by A1,A2,A4,Th78; end; dom <:f,X,Y:> c= dom f by Th77; then A5: dom f = dom <:f,X,Y:> by A3,XBOOLE_0:def 10; for x st x in dom f holds f.x = <:f,X,Y:>.x by A3,Th80; hence f = <:f,X,Y:> by A5,FUNCT_1:9; end; theorem for f being Function holds f = <:f,dom f,rng f:> by Th85; theorem for f being PartFunc of X,Y holds <:f,X,Y:> = f proof let f be PartFunc of X,Y; dom f c= X & rng f c= Y by Lm3; hence thesis by Th85; end; canceled 3; theorem Th91: <:{},X,Y:> = {} proof dom {} c= X & rng {} c= Y by XBOOLE_1:2; hence thesis by Th85; end; theorem Th92: for f,g being Function holds (<:g,Y,Z:>*<:f,X,Y:>) c= <:g*f,X,Z:> proof let f,g be Function; A1: dom (<:g,Y,Z:>*<:f,X,Y:>) c= dom <:g*f,X,Z:> proof let x; assume x in dom (<:g,Y,Z:>*<:f,X,Y:>); then x in dom<:f,X,Y:> & <:f,X,Y:>.x in dom<:g,Y,Z:> by FUNCT_1:21; then x in dom f & x in X & f.x in dom<:g,Y,Z:> by Th78,Th80; then x in dom f & x in X & f.x in dom g & g.(f.x) in Z by Th78; then x in dom (g*f) & x in X & (g*f).x in Z by FUNCT_1:21,23; hence x in dom <:g*f,X,Z:> by Th78; end; for x st x in dom (<:g,Y,Z:>*<:f,X,Y:>) holds (<:g,Y,Z:>*<:f,X,Y:>).x = <:g*f,X,Z:>.x proof let x; assume A2: x in dom (<:g,Y,Z:>*<:f,X,Y:>); then A3: x in dom<:f,X,Y:> & <:f,X,Y:>.x in dom<:g,Y,Z:> by FUNCT_1:21; then A4: x in dom f & x in X & f.x in dom<:g,Y,Z:> by Th78,Th80; then x in dom f & x in X & f.x in dom g & g.(f.x) in Z by Th78; then x in dom (g*f) & x in X & (g*f).x in Z by FUNCT_1:21,23; then A5: x in dom <:g*f,X,Z:> by Th78; thus (<:g,Y,Z:>*<:f,X,Y:>).x = <:g,Y,Z:>.(<:f,X,Y:>.x) by A2,FUNCT_1:22 .= <:g,Y,Z:>.(f.x) by A3,Th80 .= g.(f.x) by A4,Th80 .= (g*f).x by A4,FUNCT_1:23 .= <:g*f,X,Z:>.x by A5,Th80; end; hence thesis by A1,GRFUNC_1:8; end; theorem for f,g being Function st rng f /\ dom g c= Y holds <:g,Y,Z:>*<:f,X,Y:> = <:g*f,X,Z:> proof let f,g be Function such that A1: rng f /\ dom g c= Y; A2: (<:g,Y,Z:>*<:f,X,Y:>) c= <:g*f,X,Z:> by Th92; A3: dom <:g*f,X,Z:> c= dom (<:g,Y,Z:>*<:f,X,Y:>) proof let x; assume x in dom <:g*f,X,Z:>; then x in dom (g*f) & x in X & (g*f).x in Z by Th78; then x in dom f & x in X & f.x in dom g & g.(f.x) in Z by FUNCT_1:21,22; then x in dom f & x in X & f.x in rng f & f.x in dom g & g.(f.x) in Z by FUNCT_1:def 5; then x in dom f & x in X & f.x in dom g & f.x in rng f /\ dom g & g.(f.x) in Z by XBOOLE_0:def 3; then x in dom <:f,X,Y:> & f.x in dom <:g,Y,Z:> & <:f,X,Y:>.x = f.x by A1,Th78,Th79; hence thesis by FUNCT_1:21; end; for x st x in dom <:g*f,X,Z:> holds <:g*f,X,Z:>.x = (<:g,Y,Z:>*<:f,X,Y:>).x proof let x; assume A4: x in dom <:g*f,X,Z:>; then A5: x in dom (g*f) & x in X & (g*f).x in Z by Th78; then x in dom f & x in X & f.x in dom g & g.(f.x) in Z by FUNCT_1:21,22; then x in dom f & x in X & f.x in rng f & f.x in dom g & g.(f.x) in Z by FUNCT_1:def 5; then x in dom f & x in X & f.x in dom g & f.x in rng f /\ dom g & g.(f.x) in Z by XBOOLE_0:def 3; then A6: x in dom <:f,X,Y:> & f.x in dom <:g,Y,Z:> by A1,Th78; thus <:g*f,X,Z:>.x = (g*f).x by A4,Th80 .= g.(f.x) by A5,FUNCT_1:22 .= <:g,Y,Z:>.(f.x) by A6,Th80 .= <:g,Y,Z:>.(<:f,X,Y:>.x) by A6,Th80 .= (<:g,Y,Z:>*<:f,X,Y:>).x by A3,A4,FUNCT_1:22; end; then <:g*f,X,Z:> c= (<:g,Y,Z:>*<:f,X,Y:>) by A3,GRFUNC_1:8; hence thesis by A2,XBOOLE_0:def 10; end; theorem Th94: for f being Function st f is one-to-one holds <:f,X,Y:> is one-to-one proof let f be Function; assume f is one-to-one; then Y|f is one-to-one by FUNCT_1:99; then Y|f|X is one-to-one by FUNCT_1:84; hence thesis by Def3; end; theorem for f being Function st f is one-to-one holds <:f,X,Y:>" = <:f",Y,X:> proof let f be Function; assume A1: f is one-to-one; then A2: <:f,X,Y:> is one-to-one by Th94; y in dom (<:f,X,Y:>") iff y in dom <:f",Y,X:> proof thus y in dom (<:f,X,Y:>") implies y in dom <:f",Y,X:> proof assume y in dom (<:f,X,Y:>"); then A3: y in rng <:f,X,Y:> by A2,FUNCT_1:55; then consider x such that A4: x in dom <:f,X,Y:> and A5: y = <:f,X,Y:>.x by FUNCT_1:def 5; dom <:f,X,Y:> c= dom f & rng <:f,X,Y:> c= rng f by Th77; then x in dom f & y in rng f & f.x = y by A3,A4,A5,Th80; then y in dom(f") & y in Y & (f").y = x & x in X by A1,A4,Th78,FUNCT_1:54; hence thesis by Th78; end; assume A6: y in dom <:f",Y,X:>; dom <:f",Y,X:> c= dom (f") by Th77; then y in dom(f") by A6; then y in rng f by A1,FUNCT_1:55; then consider x such that A7: x in dom f and A8: y = f.x by FUNCT_1:def 5; x =(f").(f.x) by A1,A7,FUNCT_1:56; then x in X & f.x in Y by A6,A8,Th78; then x in dom <:f,X,Y:> by A7,Th78; then <:f,X,Y:>.x in rng <:f,X,Y:> & <:f,X,Y:>.x = f.x by Th80,FUNCT_1:def 5 ; hence thesis by A2,A8,FUNCT_1:55; end; then A9: dom (<:f,X,Y:>") = dom <:f",Y,X:> by TARSKI:2; for y st y in dom <:f",Y,X:> holds <:f",Y,X:>.y = (<:f,X,Y:>").y proof let y; assume A10: y in dom <:f",Y,X:>; then y in rng <:f,X,Y:> & rng <:f,X,Y:> c= rng f by A2,A9,Th77,FUNCT_1:55; then consider x such that A11: x in dom f and A12: y = f.x by FUNCT_1:def 5; A13: x =(f").(f.x) by A1,A11,FUNCT_1:56; then x in X & f.x in Y by A10,A12,Th78; then x in dom<:f,X,Y:> by A11,Th78; then (<:f,X,Y:>").(<:f,X,Y:>.x) = x & <:f,X,Y:>.x = f.x by A2,Th80,FUNCT_1:56; hence <:f",Y,X:>.y = (<:f,X,Y:>").y by A10,A12,A13,Th80; end; hence thesis by A9,FUNCT_1:9; end; theorem for f being Function holds <:f,X,Y:>|Z = <:f,X /\ Z,Y:> proof let f be Function; <:f,X,Y:> = Y|f|X & (Y|f|X)|Z = Y|f|(X /\ Z) by Def3,RELAT_1:100; hence thesis by Def3; end; theorem for f being Function holds Z|<:f,X,Y:> = <:f,X,Z /\ Y:> proof let f be Function; <:f,X,Y:> = Y|f|X by Def3; hence Z|<:f,X,Y:> = Z|(Y|(f|X)) by RELAT_1:140 .= (Z /\ Y)|(f|X) by RELAT_1:127 .= (Z /\ Y)|f|X by RELAT_1:140 .= <:f,X,Z /\ Y:> by Def3; end; :::::::::::::::::::: :: Total Function :: :::::::::::::::::::: definition let X,Y; let f be Relation of X,Y; attr f is total means :Def4: dom f = X; end; canceled; theorem for f being PartFunc of X,Y st f is total & Y = {} holds X = {} proof let f be PartFunc of X,Y; assume f is total & Y = {}; then dom f = X & f = {} by Def4,Th64; hence thesis by Lm1; end; canceled 12; theorem Th112: for f being PartFunc of {},Y holds f is total proof let f be PartFunc of {},Y; thus dom f = {} by Th54; end; theorem Th113: for f being Function st <:f,X,Y:> is total holds X c= dom f proof let f be Function such that A1: dom <:f,X,Y:> = X; let x such that A2: x in X; dom <:f,X,Y:> c= dom f by Th77; hence thesis by A1,A2; end; theorem <:{},X,Y:> is total implies X = {} proof assume <:{},X,Y:> is total; then X c= {} by Lm1,Th113; hence thesis by XBOOLE_1:3; end; theorem for f being Function st X c= dom f & rng f c= Y holds <:f,X,Y:> is total proof let f be Function such that A1: X c= dom f and A2: rng f c= Y; X c= dom <:f,X,Y:> proof let x; assume A3: x in X; then f.x in rng f by A1,FUNCT_1:def 5; hence thesis by A1,A2,A3,Th78; end; hence dom <:f,X,Y:> = X by XBOOLE_0:def 10; end; theorem for f being Function st <:f,X,Y:> is total holds f.:X c= Y proof let f be Function such that A1: dom <:f,X,Y:> = X; let y; assume y in f.:X; then consider x such that A2: x in dom f & x in X & y = f.x by FUNCT_1:def 12; <:f,X,Y:>.x = y & <:f,X,Y:>.x in rng <:f,X,Y:> & rng <:f,X,Y:> c= Y by A1,A2,Lm3,Th80,FUNCT_1:def 5; hence thesis; end; theorem for f being Function st X c= dom f & f.:X c= Y holds <:f,X,Y:> is total proof let f be Function such that A1: X c= dom f and A2: f.:X c= Y; X c= dom <:f,X,Y:> proof let x; assume A3: x in X; then f.x in f.:X by A1,FUNCT_1:def 12; hence thesis by A1,A2,A3,Th78; end; hence dom <:f,X,Y:> = X by XBOOLE_0:def 10; end; :::::::::::::::::::::::::::::::::::::::::::::::::::: :: set of partial functions from a set into a set :: :::::::::::::::::::::::::::::::::::::::::::::::::::: definition let X,Y; func PFuncs(X,Y) -> set means :Def5: x in it iff ex f being Function st x = f & dom f c= X & rng f c= Y; existence proof defpred P[set] means ex f be Function st $1 = f & dom f c= X & rng f c= Y; consider F being set such that A1: z in F iff z in bool [:X,Y:] & P[z] from Separation; take F; let z; thus z in F implies ex f being Function st z = f & dom f c= X & rng f c= Y by A1; given f being Function such that A2: z = f and A3: dom f c= X and A4: rng f c= Y; f c= [:X,Y:] proof let p; assume A5: p in f; then consider x,y such that A6: p = [x,y] by RELAT_1:def 1; A7: x in dom f by A5,A6,RELAT_1:def 4; then y = f.x by A5,A6,FUNCT_1:def 4; then y in rng f by A7,FUNCT_1:def 5; hence p in [:X,Y:] by A3,A4,A6,A7,ZFMISC_1:def 2; end; hence z in F by A1,A2,A3,A4; end; uniqueness proof let F1,F2 be set such that A8: x in F1 iff ex f being Function st x = f & dom f c= X & rng f c= Y and A9: x in F2 iff ex f being Function st x = f & dom f c= X & rng f c= Y; x in F1 iff x in F2 proof x in F1 iff ex f being Function st x = f & dom f c= X & rng f c= Y by A8 ; hence thesis by A9; end; hence thesis by TARSKI:2; end; end; definition let X,Y; cluster PFuncs(X,Y) -> non empty; coherence proof ex f being Function st dom f c= X & rng f c= Y by Lm2; hence thesis by Def5; end; end; canceled; theorem Th119: for f being PartFunc of X,Y holds f in PFuncs(X,Y) proof let f be PartFunc of X,Y; dom f c= X & rng f c= Y by Lm3; hence thesis by Def5; end; theorem Th120: for f being set st f in PFuncs(X,Y) holds f is PartFunc of X,Y proof let f be set; assume f in PFuncs(X,Y); then ex F being Function st f = F & dom F c= X & rng F c= Y by Def5; hence f is PartFunc of X,Y by Lm3; end; theorem for f being Element of PFuncs(X,Y) holds f is PartFunc of X,Y by Th120; theorem PFuncs({},Y) = { {} } proof x in PFuncs({},Y) iff x = {} proof thus x in PFuncs({},Y) implies x = {} proof assume x in PFuncs({},Y); then x is PartFunc of {},Y by Th120; hence thesis by Th57; end; {} is PartFunc of {},Y by Lm1,Th55; hence thesis by Th119; end; hence thesis by TARSKI:def 1; end; theorem PFuncs(X,{}) = { {} } proof x in PFuncs(X,{}) iff x = {} proof thus x in PFuncs(X,{}) implies x = {} proof assume x in PFuncs(X,{}); then x is PartFunc of X,{} by Th120; hence thesis by Th64; end; {} is PartFunc of X,{} by Lm1,Th55; hence thesis by Th119; end; hence thesis by TARSKI:def 1; end; canceled; theorem Th125: Z c= X implies PFuncs(Z,Y) c= PFuncs(X,Y) proof assume A1: Z c= X; let f be set; assume f in PFuncs(Z,Y); then f is PartFunc of Z,Y by Th120; then f is PartFunc of X,Y by A1,Th30; hence thesis by Th119; end; theorem PFuncs({},Y) c= PFuncs(X,Y) proof {} c= X by XBOOLE_1:2; hence thesis by Th125; end; theorem Z c= Y implies PFuncs(X,Z) c= PFuncs(X,Y) proof assume A1: Z c= Y; let f be set; assume f in PFuncs(X,Z); then f is PartFunc of X,Z by Th120; then f is PartFunc of X,Y by A1,Th31; hence thesis by Th119; end; theorem X1 c= X2 & Y1 c= Y2 implies PFuncs(X1,Y1) c= PFuncs(X2,Y2) proof assume A1: X1 c= X2 & Y1 c= Y2; let f be set; assume f in PFuncs(X1,Y1); then f is PartFunc of X1,Y1 by Th120; then f is PartFunc of X2,Y2 by A1,Th32; hence thesis by Th119; end; :::::::::::::::::::::::::::::::::::::::: :: Relation of Tolerance on Functions :: :::::::::::::::::::::::::::::::::::::::: definition let f,g be Function; pred f tolerates g means :Def6: for x st x in dom f /\ dom g holds f.x = g.x; reflexivity; symmetry; end; canceled; theorem Th130: for f,g being Function holds f tolerates g iff ex h being Function st f \/ g = h proof let f,g be Function; (for x st x in dom f /\ dom g holds f.x = g.x) iff (ex h being Function st f \/ g = h) by Th2,Th3; hence f tolerates g iff ex h being Function st f \/ g = h by Def6; end; theorem Th131: for f,g being Function holds f tolerates g iff ex h being Function st f c= h & g c= h proof let f,g be Function; now thus (ex h being Function st f c= h & g c= h) implies (ex h being Function st f \/ g = h) proof given h being Function such that A1: f c= h & g c= h; f \/ g c= h by A1,XBOOLE_1:8; then f \/ g is Function by GRFUNC_1:6; hence thesis; end; given h being Function such that A2: f \/ g = h; f c= h & g c= h by A2,XBOOLE_1:7; hence ex h being Function st f c= h & g c= h; end; hence thesis by Th130; end; theorem Th132: for f,g being Function st dom f c= dom g holds f tolerates g iff for x st x in dom f holds f.x = g.x proof let f,g be Function; assume dom f c= dom g; then dom f /\ dom g = dom f by XBOOLE_1:28; hence thesis by Def6; end; canceled 2; theorem for f,g being Function st f c= g holds f tolerates g by Th131; theorem Th136: for f,g being Function st dom f = dom g & f tolerates g holds f = g proof let f,g be Function; assume that A1: dom f = dom g and A2: f tolerates g; for x st x in dom f holds f.x = g.x by A1,A2,Th132; hence thesis by A1,FUNCT_1:9; end; canceled; theorem for f,g being Function st dom f misses dom g holds f tolerates g proof let f,g be Function; assume dom f misses dom g; then f \/ g is Function by GRFUNC_1:31; hence thesis by Th130; end; theorem for f,g,h being Function st f c= h & g c= h holds f tolerates g by Th131; theorem for f,g being PartFunc of X,Y for h being Function st f tolerates h & g c= f holds g tolerates h proof let f,g be (PartFunc of X,Y),h be Function such that A1: f tolerates h and A2: g c= f; let x; assume x in dom g /\ dom h; then x in dom g & x in dom h & dom g c= dom f by A2,RELAT_1:25,XBOOLE_0:def 3 ; then x in dom f /\ dom h & f.x = g.x by A2,GRFUNC_1:8,XBOOLE_0:def 3; hence g.x = h.x by A1,Def6; end; theorem Th141: for f being Function holds {} tolerates f proof let f be Function; {} \/ f = f; hence {} tolerates f by Th130; end; theorem Th142: for f being Function holds <:{},X,Y:> tolerates f proof let f be Function; <:{},X,Y:> = {} by Th91; hence thesis by Th141; end ; theorem for f,g being PartFunc of X,{y} holds f tolerates g proof let f,g be PartFunc of X,{y}; let x; assume x in dom f /\ dom g; then x in dom f & x in dom g by XBOOLE_0:def 3; then f.x = y & g.x = y by Th73; hence thesis; end; theorem for f being Function holds f|X tolerates f proof let f be Function; (f|X) c= f by RELAT_1:88; hence f|X tolerates f by Th131; thus thesis; end; theorem for f being Function holds Y|f tolerates f proof let f be Function; (Y|f) c= f by RELAT_1:117; hence Y|f tolerates f by Th131; end; theorem Th146: for f being Function holds Y|f|X tolerates f proof let f be Function; (Y|f|X) c= (Y|f) & (Y|f) c= f by RELAT_1:88,117; then (Y|f|X) c= f by XBOOLE_1:1; hence Y|f|X tolerates f by Th131; end; theorem for f being Function holds <:f,X,Y:> tolerates f proof let f be Function; <:f,X,Y:> = Y|f|X by Def3; hence thesis by Th146; end; theorem Th148: for f,g being PartFunc of X,Y st f is total & g is total & f tolerates g holds f = g proof let f,g be PartFunc of X,Y; assume dom f = X & dom g = X; hence thesis by Th136; end; canceled 9; theorem Th158: for f,g,h being PartFunc of X,Y st f tolerates h & g tolerates h & h is total holds f tolerates g proof let f,g,h be PartFunc of X,Y such that A1: f tolerates h and A2: g tolerates h and A3: dom h = X; let x; assume x in dom f /\ dom g; then x in dom f & x in dom g & dom f c= X & dom g c= X by XBOOLE_0:def 3; then x in dom f /\ dom h & x in dom g /\ dom h by A3,XBOOLE_0:def 3; then f.x = h.x & g.x = h.x by A1,A2,Def6; hence thesis; end; canceled 3; theorem Th162: for f,g being PartFunc of X,Y st (Y = {} implies X = {}) & f tolerates g ex h being PartFunc of X,Y st h is total & f tolerates h & g tolerates h proof let f,g be PartFunc of X,Y such that A1: Y = {} implies X = {} and A2: f tolerates g; now per cases; suppose Y = {}; then <:{},X,Y:> is total & f tolerates <:{},X,Y:> & g tolerates <:{},X,Y :> by A1,Th112,Th142; hence ex h being PartFunc of X,Y st h is total & f tolerates h & g tolerates h; suppose A3: Y <> {}; consider y being Element of Y; defpred P[set,set] means ($1 in dom f implies $2 = f.$1) & ($1 in dom g implies $2 = g.$1) & (not $1 in dom f & not $1 in dom g implies $2 = y); A4: for x st x in X ex y' st P[x,y'] proof let x such that x in X; now per cases; suppose A5: x in dom f & x in dom g; take y' = f.x; thus x in dom f implies y' = f.x; x in dom f /\ dom g by A5,XBOOLE_0:def 3; hence x in dom g implies y' = g.x by A2,Def6; thus not x in dom f & not x in dom g implies y' = y by A5; suppose A6: x in dom f & not x in dom g; take y' = f.x; thus (x in dom f implies y' = f.x) & (x in dom g implies y' = g.x) & (not x in dom f & not x in dom g implies y' = y) by A6; suppose A7: not x in dom f & x in dom g; take y' = g.x; thus (x in dom f implies y' = f.x) & (x in dom g implies y' = g.x) & (not x in dom f & not x in dom g implies y' = y) by A7; suppose not x in dom f & not x in dom g; hence ex y' st (x in dom f implies y' = f.x) & (x in dom g implies y' = g.x) & (not x in dom f & not x in dom g implies y' = y); end; hence thesis; end; A8: for x,y1,y2 st x in X & P[x,y1] & P[x,y2] holds y1 = y2; consider h being Function such that A9: dom h = X and A10: for x st x in X holds P[x,h.x] from FuncEx(A8,A4); A11: f tolerates h proof let x; assume x in dom f /\ dom h; then x in dom f & x in dom h by XBOOLE_0:def 3; hence thesis by A10; end; A12: g tolerates h proof let x; assume x in dom g /\ dom h; then x in dom g & x in dom h by XBOOLE_0:def 3; hence thesis by A10; end; rng h c= Y proof let z; assume z in rng h; then consider x such that A13: x in dom h and A14: z = h.x by FUNCT_1:def 5; per cases; suppose A15: x in dom f & x in dom g; then z = f.x by A10,A14; hence z in Y by A15,Th27; suppose A16: x in dom f & not x in dom g; then z = f.x by A10,A14; hence z in Y by A16,Th27; suppose A17: not x in dom f & x in dom g; then z = g.x by A10,A14; hence z in Y by A17,Th27; suppose not x in dom f & not x in dom g; then z = y by A9,A10,A13,A14; hence z in Y by A3; end; then reconsider h' = h as PartFunc of X,Y by A9,Lm3; h' is total by A9,Def4; hence ex h being PartFunc of X,Y st h is total & f tolerates h & g tolerates h by A11,A12; end; hence thesis; end; definition let X,Y; let f be PartFunc of X,Y; func TotFuncs f -> set means :Def7: x in it iff ex g being PartFunc of X,Y st g = x & g is total & f tolerates g; existence proof defpred P[set] means ex g being PartFunc of X,Y st g = $1 & g is total & f tolerates g; now consider F being set such that A1: for x holds x in F iff x in PFuncs(X,Y) & P[x] from Separation; take F; let x; thus x in F implies ex g being PartFunc of X,Y st g = x & g is total & f tolerates g by A1; given g being PartFunc of X,Y such that A2: g = x and A3: g is total and A4: f tolerates g; g in PFuncs(X,Y) by Th119; hence x in F by A1,A2,A3,A4; end; hence thesis; end; uniqueness proof defpred P[set] means ex g being PartFunc of X,Y st g = $1 & g is total & f tolerates g; let F1,F2 be set such that A5: for x holds x in F1 iff P[x] and A6: for x holds x in F2 iff P[x]; thus thesis from Extensionality(A5,A6); end; end; canceled 5; theorem Th168: for f being PartFunc of X,Y for g being set st g in TotFuncs(f) holds g is PartFunc of X,Y proof let f be PartFunc of X,Y; let g be set; assume g in TotFuncs(f); then ex g' being PartFunc of X,Y st g' = g & g' is total & f tolerates g' by Def7; hence thesis; end; theorem Th169: for f,g being PartFunc of X,Y st g in TotFuncs(f) holds g is total proof let f,g be PartFunc of X,Y; assume g in TotFuncs(f); then ex g' being PartFunc of X,Y st g' = g & g' is total & f tolerates g' by Def7; hence thesis; end; canceled; theorem Th171: for f being PartFunc of X,Y for g being Function st g in TotFuncs(f) holds f tolerates g proof let f be PartFunc of X,Y; let g be Function; assume g in TotFuncs(f); then ex g' being PartFunc of X,Y st g' = g & g' is total & f tolerates g' by Def7; hence f tolerates g; end; theorem for f being PartFunc of X,{} st X <> {} holds TotFuncs(f) = {} proof let f be PartFunc of X,{}; assume A1: X <> {}; assume A2: TotFuncs(f) <> {}; consider g being Element of TotFuncs(f); consider g' being PartFunc of X,{} such that g' = g and A3: g' is total and f tolerates g' by A2,Def7; dom g' = {} by Th62; hence contradiction by A1,A3,Def4; end; canceled; theorem Th174: for f being PartFunc of X,Y holds f is total iff TotFuncs f = {f} proof let f be PartFunc of X,Y; thus f is total implies TotFuncs f = {f} proof assume A1: f is total; for g being set holds g in TotFuncs f iff f = g proof let g be set; thus g in TotFuncs f implies f = g proof assume g in TotFuncs f; then ex g' being PartFunc of X,Y st g' = g & g' is total & f tolerates g' by Def7; hence thesis by A1,Th148; end; thus thesis by A1,Def7; end; hence thesis by TARSKI:def 1; end; assume TotFuncs f = {f}; then f in TotFuncs f by TARSKI:def 1; hence thesis by Th169; end; theorem Th175: for f being PartFunc of {},Y holds TotFuncs f = {f} proof let f be PartFunc of {},Y; f is total by Th112; hence thesis by Th174; end; theorem for f being PartFunc of {},Y holds TotFuncs f = {{}} proof let f be PartFunc of {},Y; f = {} by Th57; hence thesis by Th175; end; canceled 8; theorem for f,g being PartFunc of X,Y st TotFuncs f meets TotFuncs g holds f tolerates g proof let f,g be PartFunc of X,Y; assume A1: TotFuncs f /\ TotFuncs g <> {}; consider h being Element of TotFuncs f /\ TotFuncs g; A2: h in TotFuncs f & h in TotFuncs g by A1,XBOOLE_0:def 3; then reconsider h as PartFunc of X,Y by Th168; h is total & f tolerates h & g tolerates h by A2,Th169,Th171; hence thesis by Th158; end; theorem for f,g being PartFunc of X,Y st (Y = {} implies X = {}) & f tolerates g holds TotFuncs f meets TotFuncs g proof let f,g be PartFunc of X,Y; assume (Y = {} implies X = {}) & f tolerates g; then consider h being PartFunc of X,Y such that A1: h is total & f tolerates h & g tolerates h by Th162; h in TotFuncs f & h in TotFuncs g by A1,Def7; hence TotFuncs f /\ TotFuncs g <> {} by XBOOLE_0:def 3; end; begin :: id X as a relation of X Lm4: for R being Relation of X st R = id X holds R is total proof let R be Relation of X; assume R = id X; hence dom R = X by RELAT_1:71; end; Lm5: for R being Relation st R = id X holds R is reflexive symmetric antisymmetric transitive proof let R be Relation; assume A1: R = id X; then A2: dom R = X by RELAT_1:71; rng R = X by A1,RELAT_1:71; then A3: field R = X \/ X by A2,RELAT_1:def 6; thus R is_reflexive_in field R proof let x; thus thesis by A1,A3,RELAT_1:def 10; end; thus R is_symmetric_in field R proof let x,y; assume A4: x in field R & y in field R; assume [x,y] in R; then x = y by A1,RELAT_1:def 10; hence [y,x] in R by A1,A3,A4,RELAT_1:def 10; end; thus R is_antisymmetric_in field R proof let x; thus thesis by A1,RELAT_1:def 10; end; thus R is_transitive_in field R proof let x; thus thesis by A1,RELAT_1:def 10; end; end; Lm6: id X is Relation of X proof dom id X c= X & rng id X c= X by RELAT_1:71; hence thesis by RELSET_1:11; end; definition let X; cluster total reflexive symmetric antisymmetric transitive Relation of X; existence proof reconsider R = id X as Relation of X by Lm6; take R; thus thesis by Lm4,Lm5; end; end; definition cluster symmetric transitive -> reflexive Relation; coherence proof let R be Relation; assume that A1: R is_symmetric_in field R and A2: R is_transitive_in field R; let x; assume A3: x in field R; then x in dom R \/ rng R by RELAT_1:def 6; then x in dom R or x in rng R by XBOOLE_0:def 2; then consider y such that A4: [x,y] in R or [y,x] in R by RELAT_1:def 4,def 5; A5: field R = dom R \/ rng R by RELAT_1:def 6; y in rng R or y in dom R by A4,RELAT_1:def 4,def 5; then A6: y in field R by A5,XBOOLE_0:def 2; then [x,y] in R & [y,x] in R by A1,A3,A4,RELAT_2:def 3; hence [x,x] in R by A2,A3,A6,RELAT_2:def 8; end; end; definition let X; cluster id X -> symmetric antisymmetric transitive; coherence by Lm5; end; definition let X; redefine func id X -> total Relation of X; coherence by Lm4,Lm6; end;

Back to top