Volume 1, 1989

University of Bialystok

Copyright (c) 1989 Association of Mizar Users

### The abstract of the Mizar article:

### Partial Functions

**by****Czeslaw Bylinski**- Received September 18, 1989
- MML identifier: PARTFUN1

- [ Mizar article, 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; 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 :: PARTFUN1:1 P c= [:X1,Y1:] & Q c= [:X2,Y2:] implies P \/ Q c= [:X1 \/ X2,Y1 \/ Y2:]; theorem :: PARTFUN1:2 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; theorem :: PARTFUN1:3 for f,g,h being Function st f \/ g = h for x st x in dom f /\ dom g holds f.x = g.x; 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)); :::::::::::::::::::: :: Empty Function :: :::::::::::::::::::: definition cluster empty Function; end; canceled 6; theorem :: PARTFUN1:10 rng {} = {}; definition let X,Y; cluster Function-like Relation of X,Y; end; definition let X,Y; mode PartFunc of X,Y is Function-like Relation of X,Y; end; canceled 13; theorem :: PARTFUN1:24 for f being Function holds f is PartFunc of dom f, rng f; theorem :: PARTFUN1:25 for f being Function st rng f c= Y holds f is PartFunc of dom f, Y; theorem :: PARTFUN1:26 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; theorem :: PARTFUN1:27 for f being PartFunc of X,Y st x in dom f holds f.x in Y; theorem :: PARTFUN1:28 for f being PartFunc of X,Y st dom f c= Z holds f is PartFunc of Z,Y; theorem :: PARTFUN1:29 for f being PartFunc of X,Y st rng f c= Z holds f is PartFunc of X,Z; theorem :: PARTFUN1:30 for f being PartFunc of X,Y st X c= Z holds f is PartFunc of Z,Y; theorem :: PARTFUN1:31 for f being PartFunc of X,Y st Y c= Z holds f is PartFunc of X,Z; theorem :: PARTFUN1:32 for f being PartFunc of X1,Y1 st X1 c= X2 & Y1 c= Y2 holds f is PartFunc of X2,Y2; theorem :: PARTFUN1:33 for f being Function,g being PartFunc of X,Y st f c= g holds f is PartFunc of X,Y; theorem :: PARTFUN1:34 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; theorem :: PARTFUN1:35 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; 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 for x,y st x in X() & P[x,y] holds y in Y() and for x,y1,y2 st x in X() & P[x,y1] & P[x,y2] holds y1 = y2; 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 for x st P[x] holds F(x) in Y(); 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 for x,y,z st x in X() & y in Y() & P[x,y,z] holds z in Z() and for x,y,z1,z2 st x in X() & y in Y() & P[x,y,z1] & P[x,y,z2] holds z1 = z2; 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 for x,y st P[x,y] holds F(x,y) in Z(); 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; end; theorem :: PARTFUN1:36 for f being PartFunc of X,Y holds f*(id X) = f; theorem :: PARTFUN1:37 for f being PartFunc of X,Y holds (id Y)*f = f; theorem :: PARTFUN1:38 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; theorem :: PARTFUN1:39 for f being PartFunc of X,Y st f is one-to-one holds f" is PartFunc of Y,X ; canceled 3; theorem :: PARTFUN1:43 for f being PartFunc of X,Y holds f|Z is PartFunc of Z,Y; theorem :: PARTFUN1:44 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; end; theorem :: PARTFUN1:45 for f being PartFunc of X,Y holds Z|f is PartFunc of X,Z; theorem :: PARTFUN1:46 for f being PartFunc of X,Y holds Z|f is PartFunc of X,Y; theorem :: PARTFUN1:47 for f being Function holds Y|f|X is PartFunc of X,Y; canceled; theorem :: PARTFUN1:49 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; canceled; theorem :: PARTFUN1:51 for f being PartFunc of X,Y holds f.:X = rng f; canceled; theorem :: PARTFUN1:53 for f being PartFunc of X,Y holds f"Y = dom f; :::::::::::::::::::::::::::: :: Empty Function :: :::::::::::::::::::::::::::: theorem :: PARTFUN1:54 for f being PartFunc of {},Y holds dom f = {} & rng f = {}; theorem :: PARTFUN1:55 for f being Function st dom f = {} holds f is PartFunc of X,Y; theorem :: PARTFUN1:56 {} is PartFunc of X,Y; theorem :: PARTFUN1:57 for f being PartFunc of {},Y holds f = {}; theorem :: PARTFUN1:58 for f1 being PartFunc of {},Y1 for f2 being PartFunc of {},Y2 holds f1 = f2; theorem :: PARTFUN1:59 for f being PartFunc of {},Y holds f is one-to-one; theorem :: PARTFUN1:60 for f being PartFunc of {},Y holds f.:P = {}; theorem :: PARTFUN1:61 for f being PartFunc of {},Y holds f"Q = {}; theorem :: PARTFUN1:62 for f being PartFunc of X,{} holds dom f = {} & rng f = {}; theorem :: PARTFUN1:63 for f being Function st rng f = {} holds f is PartFunc of X,Y; theorem :: PARTFUN1:64 for f being PartFunc of X,{} holds f = {}; theorem :: PARTFUN1:65 for f1 being PartFunc of X1,{} for f2 being PartFunc of X2,{} holds f1 = f2; theorem :: PARTFUN1:66 for f being PartFunc of X,{} holds f is one-to-one; theorem :: PARTFUN1:67 for f being PartFunc of X,{} holds f.:P = {}; theorem :: PARTFUN1:68 for f being PartFunc of X,{} holds f"Q = {}; :::::::::::::::::::::::::::::::::::::::::::::::: :: Partial function from a singelton into set :: :::::::::::::::::::::::::::::::::::::::::::::::: theorem :: PARTFUN1:69 for f being PartFunc of {x},Y holds rng f c= {f.x}; theorem :: PARTFUN1:70 for f being PartFunc of {x},Y holds f is one-to-one; theorem :: PARTFUN1:71 for f being PartFunc of {x},Y holds f.:P c= {f.x}; theorem :: PARTFUN1:72 for f being Function st dom f = {x} & x in X & f.x in Y holds f is PartFunc of X,Y; :::::::::::::::::::::::::::::::::::::::::::::::::: :: Partial function from a set into a singelton :: :::::::::::::::::::::::::::::::::::::::::::::::::: theorem :: PARTFUN1:73 for f being PartFunc of X,{y} st x in dom f holds f.x = y; theorem :: PARTFUN1:74 for f1,f2 being PartFunc of X,{y} st dom f1 = dom f2 holds f1 = f2; :::::::::::::::::::::::::::::::::::::::::::::::::::::::: :: 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 :: PARTFUN1:def 3 Y|f|X; end; canceled; theorem :: PARTFUN1:76 for f being Function holds <:f,X,Y:> c= f; theorem :: PARTFUN1:77 for f being Function holds dom <:f,X,Y:> c= dom f & rng <:f,X,Y:> c= rng f; theorem :: PARTFUN1:78 for f being Function holds x in dom <:f,X,Y:> iff x in dom f & x in X & f.x in Y; theorem :: PARTFUN1:79 for f being Function st x in dom f & x in X & f.x in Y holds <:f,X,Y:>.x = f.x; theorem :: PARTFUN1:80 for f being Function st x in dom <:f,X,Y:> holds <:f,X,Y:>.x = f.x; theorem :: PARTFUN1:81 for f,g being Function st f c= g holds <:f,X,Y:> c= <:g,X,Y:>; theorem :: PARTFUN1:82 for f being Function st Z c= X holds <:f,Z,Y:> c= <:f,X,Y:>; theorem :: PARTFUN1:83 for f being Function st Z c= Y holds <:f,X,Z:> c= <:f,X,Y:>; theorem :: PARTFUN1:84 for f being Function st X1 c= X2 & Y1 c= Y2 holds <:f,X1,Y1:> c= <:f,X2,Y2:>; theorem :: PARTFUN1:85 for f being Function st dom f c= X & rng f c= Y holds f = <:f,X,Y:>; theorem :: PARTFUN1:86 for f being Function holds f = <:f,dom f,rng f:>; theorem :: PARTFUN1:87 for f being PartFunc of X,Y holds <:f,X,Y:> = f; canceled 3; theorem :: PARTFUN1:91 <:{},X,Y:> = {}; theorem :: PARTFUN1:92 for f,g being Function holds (<:g,Y,Z:>*<:f,X,Y:>) c= <:g*f,X,Z:>; theorem :: PARTFUN1:93 for f,g being Function st rng f /\ dom g c= Y holds <:g,Y,Z:>*<:f,X,Y:> = <:g*f,X,Z:>; theorem :: PARTFUN1:94 for f being Function st f is one-to-one holds <:f,X,Y:> is one-to-one; theorem :: PARTFUN1:95 for f being Function st f is one-to-one holds <:f,X,Y:>" = <:f",Y,X:>; theorem :: PARTFUN1:96 for f being Function holds <:f,X,Y:>|Z = <:f,X /\ Z,Y:>; theorem :: PARTFUN1:97 for f being Function holds Z|<:f,X,Y:> = <:f,X,Z /\ Y:>; :::::::::::::::::::: :: Total Function :: :::::::::::::::::::: definition let X,Y; let f be Relation of X,Y; attr f is total means :: PARTFUN1:def 4 dom f = X; end; canceled; theorem :: PARTFUN1:99 for f being PartFunc of X,Y st f is total & Y = {} holds X = {}; canceled 12; theorem :: PARTFUN1:112 for f being PartFunc of {},Y holds f is total; theorem :: PARTFUN1:113 for f being Function st <:f,X,Y:> is total holds X c= dom f; theorem :: PARTFUN1:114 <:{},X,Y:> is total implies X = {}; theorem :: PARTFUN1:115 for f being Function st X c= dom f & rng f c= Y holds <:f,X,Y:> is total; theorem :: PARTFUN1:116 for f being Function st <:f,X,Y:> is total holds f.:X c= Y; theorem :: PARTFUN1:117 for f being Function st X c= dom f & f.:X c= Y holds <:f,X,Y:> is total; :::::::::::::::::::::::::::::::::::::::::::::::::::: :: set of partial functions from a set into a set :: :::::::::::::::::::::::::::::::::::::::::::::::::::: definition let X,Y; func PFuncs(X,Y) -> set means :: PARTFUN1:def 5 x in it iff ex f being Function st x = f & dom f c= X & rng f c= Y; end; definition let X,Y; cluster PFuncs(X,Y) -> non empty; end; canceled; theorem :: PARTFUN1:119 for f being PartFunc of X,Y holds f in PFuncs(X,Y); theorem :: PARTFUN1:120 for f being set st f in PFuncs(X,Y) holds f is PartFunc of X,Y; theorem :: PARTFUN1:121 for f being Element of PFuncs(X,Y) holds f is PartFunc of X,Y; theorem :: PARTFUN1:122 PFuncs({},Y) = { {} }; theorem :: PARTFUN1:123 PFuncs(X,{}) = { {} }; canceled; theorem :: PARTFUN1:125 Z c= X implies PFuncs(Z,Y) c= PFuncs(X,Y); theorem :: PARTFUN1:126 PFuncs({},Y) c= PFuncs(X,Y); theorem :: PARTFUN1:127 Z c= Y implies PFuncs(X,Z) c= PFuncs(X,Y); theorem :: PARTFUN1:128 X1 c= X2 & Y1 c= Y2 implies PFuncs(X1,Y1) c= PFuncs(X2,Y2); :::::::::::::::::::::::::::::::::::::::: :: Relation of Tolerance on Functions :: :::::::::::::::::::::::::::::::::::::::: definition let f,g be Function; pred f tolerates g means :: PARTFUN1:def 6 for x st x in dom f /\ dom g holds f.x = g.x; reflexivity; symmetry; end; canceled; theorem :: PARTFUN1:130 for f,g being Function holds f tolerates g iff ex h being Function st f \/ g = h; theorem :: PARTFUN1:131 for f,g being Function holds f tolerates g iff ex h being Function st f c= h & g c= h; theorem :: PARTFUN1:132 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; canceled 2; theorem :: PARTFUN1:135 for f,g being Function st f c= g holds f tolerates g; theorem :: PARTFUN1:136 for f,g being Function st dom f = dom g & f tolerates g holds f = g; canceled; theorem :: PARTFUN1:138 for f,g being Function st dom f misses dom g holds f tolerates g; theorem :: PARTFUN1:139 for f,g,h being Function st f c= h & g c= h holds f tolerates g; theorem :: PARTFUN1:140 for f,g being PartFunc of X,Y for h being Function st f tolerates h & g c= f holds g tolerates h; theorem :: PARTFUN1:141 for f being Function holds {} tolerates f; theorem :: PARTFUN1:142 for f being Function holds <:{},X,Y:> tolerates f ; theorem :: PARTFUN1:143 for f,g being PartFunc of X,{y} holds f tolerates g; theorem :: PARTFUN1:144 for f being Function holds f|X tolerates f; theorem :: PARTFUN1:145 for f being Function holds Y|f tolerates f; theorem :: PARTFUN1:146 for f being Function holds Y|f|X tolerates f; theorem :: PARTFUN1:147 for f being Function holds <:f,X,Y:> tolerates f; theorem :: PARTFUN1:148 for f,g being PartFunc of X,Y st f is total & g is total & f tolerates g holds f = g; canceled 9; theorem :: PARTFUN1:158 for f,g,h being PartFunc of X,Y st f tolerates h & g tolerates h & h is total holds f tolerates g; canceled 3; theorem :: PARTFUN1:162 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; definition let X,Y; let f be PartFunc of X,Y; func TotFuncs f -> set means :: PARTFUN1:def 7 x in it iff ex g being PartFunc of X,Y st g = x & g is total & f tolerates g; end; canceled 5; theorem :: PARTFUN1:168 for f being PartFunc of X,Y for g being set st g in TotFuncs(f) holds g is PartFunc of X,Y; theorem :: PARTFUN1:169 for f,g being PartFunc of X,Y st g in TotFuncs(f) holds g is total; canceled; theorem :: PARTFUN1:171 for f being PartFunc of X,Y for g being Function st g in TotFuncs(f) holds f tolerates g; theorem :: PARTFUN1:172 for f being PartFunc of X,{} st X <> {} holds TotFuncs(f) = {}; canceled; theorem :: PARTFUN1:174 for f being PartFunc of X,Y holds f is total iff TotFuncs f = {f}; theorem :: PARTFUN1:175 for f being PartFunc of {},Y holds TotFuncs f = {f}; theorem :: PARTFUN1:176 for f being PartFunc of {},Y holds TotFuncs f = {{}}; canceled 8; theorem :: PARTFUN1:185 for f,g being PartFunc of X,Y st TotFuncs f meets TotFuncs g holds f tolerates g; theorem :: PARTFUN1:186 for f,g being PartFunc of X,Y st (Y = {} implies X = {}) & f tolerates g holds TotFuncs f meets TotFuncs g; begin definition let X; cluster total reflexive symmetric antisymmetric transitive Relation of X; end; definition cluster symmetric transitive -> reflexive Relation; end; definition let X; cluster id X -> symmetric antisymmetric transitive; end; definition let X; redefine func id X -> total Relation of X; end;

Back to top