Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

### 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;

```