:: Partial Functions
:: by Czes{\l}aw Byli\'nski
::
:: Received September 18, 1989
:: Copyright (c) 1990-2016 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 ex h being Function st f \/ g = h;
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 ex h being Function st f \/ g = h;
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};