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;