:: Partial Functions :: by Czes{\l}aw Byli\'nski :: :: Received September 18, 1989 :: Copyright (c) 1990-2018 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 FUNCT_1, RELAT_1, XBOOLE_0, TARSKI, SUBSET_1, ZFMISC_1, RELAT_2, PARTFUN1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2, RELSET_1, FUNCT_1; constructors FUNCT_1, RELAT_2, RELSET_1; registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1; requirements SUBSET, BOOLE; begin reserve x,x1,x2,y,y9,y1,y2,z,z1,z2 for object,P,X,X1,X2,Y,Y1,Y2,V,Z for set; :: Auxiliary theorems theorem :: PARTFUN1:1 for f,g being Function st for x being object st x in dom f /\ dom g holds f.x = g.x holds f \/ g is Function; theorem :: PARTFUN1:2 for f,g,h being Function st f \/ g = h for x being object st x in dom f /\ dom g holds f.x = g.x; scheme :: PARTFUN1:sch 1 LambdaC{A()->set,C[object],F,G(object)->object}: ex f being Function st dom f = A() & for x being object st x in A() holds (C[x] implies f.x = F(x)) & (not C[x] implies f.x = G(x)); registration let X,Y; cluster Function-like for Relation of X,Y; end; definition let X,Y; mode PartFunc of X,Y is Function-like Relation of X,Y; end; theorem :: PARTFUN1:3 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:4 for f being Y-valued Function st x in dom f holds f.x in Y; theorem :: PARTFUN1:5 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; scheme :: PARTFUN1:sch 2 PartFuncEx{X,Y()->set,P[object,object]}: ex f being PartFunc of X(),Y() st (for x being object holds x in dom f iff x in X() & ex y being object st P[x,y]) & for x being object st x in dom f holds P[x,f.x] provided for x,y being object st x in X() & P[x,y] holds y in Y() and for x,y1,y2 being object st x in X() & P[x,y1] & P[x,y2] holds y1 = y2; scheme :: PARTFUN1:sch 3 LambdaR{X,Y()->set,F(object)->object,P[object]}: ex f being PartFunc of X(),Y() st (for x being object holds x in dom f iff x in X() & P[x]) & for x being object st x in dom f holds f.x = F(x) provided for x being object st P[x] holds F(x) in Y(); 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:6 for f being Relation of X,Y holds (id X)*f = f; theorem :: PARTFUN1:7 for f being Relation of X,Y holds f*(id Y) = f; theorem :: PARTFUN1:8 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:9 for f being PartFunc of X,Y st f is one-to-one holds f" is PartFunc of Y,X; theorem :: PARTFUN1:10 for f being PartFunc of X,Y holds f|Z is PartFunc of Z,Y; theorem :: PARTFUN1:11 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:12 for f being PartFunc of X,Y holds Z|`f is PartFunc of X,Z; theorem :: PARTFUN1:13 for f being PartFunc of X,Y holds Z|`f is PartFunc of X,Y; theorem :: PARTFUN1:14 for f being Function holds Y|`f|X is PartFunc of X,Y; theorem :: PARTFUN1:15 for f being PartFunc of X,Y st y in f.:X ex x being Element of X st x in dom f & y = f.x; :: Partial function from a singelton into set theorem :: PARTFUN1:16 for f being PartFunc of {x},Y holds rng f c= {f.x}; theorem :: PARTFUN1:17 for f being PartFunc of {x},Y holds f is one-to-one; theorem :: PARTFUN1:18 for f being PartFunc of {x},Y holds f.:P c= {f.x}; theorem :: PARTFUN1:19 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:20 for f being PartFunc of X,{y} st x in dom f holds f.x = y; theorem :: PARTFUN1:21 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; func <:f,X,Y:> -> PartFunc of X,Y equals :: PARTFUN1:def 1 Y|`f|X; end; theorem :: PARTFUN1:22 for f being Function holds <:f,X,Y:> c= f; theorem :: PARTFUN1:23 for f being Function holds dom <:f,X,Y:> c= dom f & rng <:f,X,Y :> c= rng f; theorem :: PARTFUN1:24 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:25 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:26 for f being Function st x in dom <:f,X,Y:> holds <:f,X,Y:>.x = f .x; theorem :: PARTFUN1:27 for f,g being Function st f c= g holds <:f,X,Y:> c= <:g,X,Y:>; theorem :: PARTFUN1:28 for f being Function st Z c= X holds <:f,Z,Y:> c= <:f,X,Y:>; theorem :: PARTFUN1:29 for f being Function st Z c= Y holds <:f,X,Z:> c= <:f,X,Y:>; theorem :: PARTFUN1:30 for f being Function st X1 c= X2 & Y1 c= Y2 holds <:f,X1,Y1:> c= <:f, X2,Y2:> ; theorem :: PARTFUN1:31 for f being Function st dom f c= X & rng f c= Y holds f = <:f,X, Y:>; theorem :: PARTFUN1:32 for f being Function holds f = <:f,dom f,rng f:>; theorem :: PARTFUN1:33 for f being PartFunc of X,Y holds <:f,X,Y:> = f; theorem :: PARTFUN1:34 <:{},X,Y:> = {}; theorem :: PARTFUN1:35 for f,g being Function holds (<:g,Y,Z:>*<:f,X,Y:>) c= <:g*f,X,Z :>; theorem :: PARTFUN1:36 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:37 for f being Function st f is one-to-one holds <:f,X,Y:> is one-to-one; theorem :: PARTFUN1:38 for f being Function st f is one-to-one holds <:f,X,Y:>" = <:f",Y,X:>; theorem :: PARTFUN1:39 for f being Function holds Z|`<:f,X,Y:> = <:f,X,Z /\ Y:>; :: Total Function definition let X; let f be X-defined Relation; attr f is total means :: PARTFUN1:def 2 dom f = X; end; registration let X be empty set, Y be set; cluster -> total for Relation of X,Y; end; registration let X be non empty set, Y be empty set; cluster -> non total for Relation of X,Y; end; theorem :: PARTFUN1:40 for f being Function st <:f,X,Y:> is total holds X c= dom f; theorem :: PARTFUN1:41 <:{},X,Y:> is total implies X = {}; theorem :: PARTFUN1:42 for f being Function st X c= dom f & rng f c= Y holds <:f,X,Y:> is total; theorem :: PARTFUN1:43 for f being Function st <:f,X,Y:> is total holds f.:X c= Y; theorem :: PARTFUN1:44 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 3 x in it iff ex f being Function st x = f & dom f c= X & rng f c= Y; end; registration let X,Y; cluster PFuncs(X,Y) -> non empty; end; theorem :: PARTFUN1:45 for f being PartFunc of X,Y holds f in PFuncs(X,Y); theorem :: PARTFUN1:46 for f being set st f in PFuncs(X,Y) holds f is PartFunc of X,Y; theorem :: PARTFUN1:47 for f being Element of PFuncs(X,Y) holds f is PartFunc of X,Y; theorem :: PARTFUN1:48 PFuncs({},Y) = { {} }; theorem :: PARTFUN1:49 PFuncs(X,{}) = { {} }; theorem :: PARTFUN1:50 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 4 for x being object st x in dom f /\ dom g holds f.x = g.x; reflexivity; symmetry; end; theorem :: PARTFUN1:51 for f,g being Function holds f tolerates g iff f \/ g is Function; theorem :: PARTFUN1:52 for f,g being Function holds f tolerates g iff ex h being Function st f c= h & g c= h; theorem :: PARTFUN1:53 for f,g being Function st dom f c= dom g holds f tolerates g iff for x being object st x in dom f holds f.x = g.x; theorem :: PARTFUN1:54 for f,g being Function st f c= g holds f tolerates g; theorem :: PARTFUN1:55 for f,g being Function st dom f = dom g & f tolerates g holds f = g; theorem :: PARTFUN1:56 for f,g being Function st dom f misses dom g holds f tolerates g; theorem :: PARTFUN1:57 for f,g,h being Function st f c= h & g c= h holds f tolerates g; theorem :: PARTFUN1:58 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:59 for f being Function holds {} tolerates f; theorem :: PARTFUN1:60 for f being Function holds <:{},X,Y:> tolerates f; theorem :: PARTFUN1:61 for f,g being PartFunc of X,{y} holds f tolerates g; theorem :: PARTFUN1:62 for f being Function holds f|X tolerates f; theorem :: PARTFUN1:63 for f being Function holds Y|`f tolerates f; theorem :: PARTFUN1:64 for f being Function holds Y|`f|X tolerates f; theorem :: PARTFUN1:65 for f being Function holds <:f,X,Y:> tolerates f; theorem :: PARTFUN1:66 for f,g being PartFunc of X,Y st f is total & g is total & f tolerates g holds f = g; theorem :: PARTFUN1:67 for f,g,h being PartFunc of X,Y st f tolerates h & g tolerates h & h is total holds f tolerates g; theorem :: PARTFUN1:68 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 5 for x being object holds x in it iff ex g being PartFunc of X,Y st g = x & g is total & f tolerates g; end; theorem :: PARTFUN1:69 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:70 for f,g being PartFunc of X,Y st g in TotFuncs(f) holds g is total; theorem :: PARTFUN1:71 for f being PartFunc of X,Y for g being Function st g in TotFuncs(f) holds f tolerates g; registration let X be non empty set, Y be empty set; let f be PartFunc of X,Y; cluster TotFuncs f -> empty; end; theorem :: PARTFUN1:72 for f being PartFunc of X,Y holds f is total iff TotFuncs f = { f}; theorem :: PARTFUN1:73 for f being PartFunc of {},Y holds TotFuncs f = {f}; theorem :: PARTFUN1:74 for f being PartFunc of {},Y holds TotFuncs f = {{}}; theorem :: PARTFUN1:75 for f,g being PartFunc of X,Y st TotFuncs f meets TotFuncs g holds f tolerates g; theorem :: PARTFUN1:76 for f,g being PartFunc of X,Y st (Y = {} implies X = {}) & f tolerates g holds TotFuncs f meets TotFuncs g; begin registration let X; cluster total reflexive symmetric antisymmetric transitive for Relation of X; end; registration cluster symmetric transitive -> reflexive for Relation; end; registration let X; cluster id X -> symmetric antisymmetric transitive; end; definition let X; redefine func id X -> total Relation of X; end; scheme :: PARTFUN1:sch 4 LambdaC9{ A() -> non empty set, C[object], F,G(object) -> object } : ex f being Function st dom f = A() & for x be Element of A() holds (C[x] implies f.x = F(x)) & (not C[x] implies f.x = G(x)); begin :: Addenda :: from AMI_1, 2007,07,20, A.T. reserve A for set, f,g,h for Function; theorem :: PARTFUN1:77 for x,y,z being object holds f tolerates g & [x,y] in f & [x,z] in g implies y = z; theorem :: PARTFUN1:78 A is functional & (for f,g being Function st f in A & g in A holds f tolerates g) implies union A is Function; :: Moved from FINSEQ_4 by AK on 2007.10.09 definition let D be set, p be D-valued Function, i be object; assume i in dom p; func p/.i -> Element of D equals :: PARTFUN1:def 6 p.i; end; :: missing, 2008.09.15, A.T. registration let X,Y be non empty set; cluster non empty for PartFunc of X,Y; end; :: from FRAENKEL, 2009.05.06, A.K. registration let A, B be set; cluster PFuncs(A,B) -> functional; end; :: from CIRCCOMB, 2011.04.19, A.T. theorem :: PARTFUN1:79 for f1,f2, g being Function st rng g c= dom f1 & rng g c= dom f2 & f1 tolerates f2 holds f1*g = f2*g; :: missing, 2011.06.06, A.T. theorem :: PARTFUN1:80 for f being Y-valued Function st x in dom(f|X) holds (f|X)/.x = f/.x; scheme :: PARTFUN1:sch 5 LambdaCS{A()->set,C[object],F,G(object)->object}: ex f being Function st dom f = A() & for x being set st x in A() holds (C[x] implies f.x = F(x)) & (not C[x] implies f.x = G(x)); theorem :: PARTFUN1:81 for f,g being Function st f.x = g.x holds f | {x} tolerates g | {x}; theorem :: PARTFUN1:82 for f,g being Function st f.x = g.x & f.y = g.y holds f | {x,y} tolerates g | {x,y};