The abstract of the Mizar article:

Partial Functions from a Domain to a Domain

by

Jaroslaw Kotowicz

Received May 31, 1990

MML identifier: PARTFUN2

[ Mizar article, MML identifier index ]

environ

 vocabulary PARTFUN1, RELAT_1, FINSEQ_4, FUNCT_1, BOOLE, FUNCOP_1, PARTFUN2;
 notation TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, RELSET_1, FUNCT_1, FUNCT_2,
      FUNCOP_1, PARTFUN1, FINSEQ_4;
 constructors FUNCOP_1, PARTFUN1, FINSEQ_4, MEMBERED, XBOOLE_0;
 clusters RELAT_1, FUNCT_1, RELSET_1, FUNCOP_1, MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin

 reserve x,y,X,Y for set;
 reserve C,D,E for non empty set;
 reserve SC for Subset of C;
 reserve SD for Subset of D;
 reserve SE for Subset of E;
 reserve c,c1,c2 for Element of C;
 reserve d,d1,d2 for Element of D;
 reserve e for Element of E;
 reserve f,f1,g for PartFunc of C,D;
 reserve t for PartFunc of D,C;
 reserve s for PartFunc of D,E;
 reserve h for PartFunc of C,E;
 reserve F for PartFunc of D,D;

canceled 2;

theorem :: PARTFUN2:3
dom f = dom g & (for c st c in dom f holds f/.c = g/.c) implies f = g;

theorem :: PARTFUN2:4    :: ograniczyc do implikacji
y in rng f iff ex c st c in dom f & y = f/.c;

canceled;

theorem :: PARTFUN2:6
h = s*f iff (for c holds c in dom h iff c in dom f & f/.c in dom s) &
             for c st c in dom h holds h/.c = s/.(f/.c);

canceled 2;

theorem :: PARTFUN2:9
c in dom f & f/.c in dom s implies (s*f)/.c = s/.(f/.c);

theorem :: PARTFUN2:10
  rng f c= dom s & c in dom f implies (s*f)/.c = s/.(f/.c);

definition let D; let SD;
redefine func id SD -> PartFunc of D,D;
end;

canceled;

theorem :: PARTFUN2:12
F = id SD iff dom F = SD & for d st d in SD holds F/.d = d;

canceled;

theorem :: PARTFUN2:14
  d in dom F /\ SD implies F/.d = (F*id SD)/.d;

theorem :: PARTFUN2:15
  d in dom((id SD)*F) iff d in dom F & F/.d in SD;

theorem :: PARTFUN2:16
   (for c1,c2 st c1 in dom f & c2 in dom f & f/.c1 = f/.c2 holds c1 = c2)
 implies f is one-to-one;

theorem :: PARTFUN2:17
  f is one-to-one & x in dom f & y in dom f & f/.x = f/.y implies x = y;

definition
 cluster {} -> one-to-one;
end;

definition let X,Y;
 cluster one-to-one PartFunc of X,Y;
end;

definition let X,Y; let f be one-to-one PartFunc of X,Y;
 redefine func f" -> PartFunc of Y,X;
end;

theorem :: PARTFUN2:18
for f being one-to-one PartFunc of C,D holds
 for g be PartFunc of D,C holds g = f" iff dom g = rng f &
            for d,c holds d in rng f & c = g/.d iff c in dom f & d = f/.c;

canceled 3;

theorem :: PARTFUN2:22
   for f being one-to-one PartFunc of C,D st c in dom f
  holds c = f"/.(f/.c) & c = (f"*f)/.c;

theorem :: PARTFUN2:23
   for f being one-to-one PartFunc of C,D st d in rng f
  holds d = f/.(f"/.d) & d = (f*(f"))/.d;

theorem :: PARTFUN2:24
  f is one-to-one & dom f = rng t & rng f = dom t &
 (for c,d st c in dom f & d in dom t holds f/.c = d iff t/.d = c)
  implies t = f";

canceled 7;

theorem :: PARTFUN2:32
  g = f|X iff dom g = dom f /\ X & for c st c in dom g holds g/.c = f/.c;

canceled;

theorem :: PARTFUN2:34
c in dom f /\ X implies f|X/.c = f/.c;

theorem :: PARTFUN2:35
  c in dom f & c in X implies f|X/.c = f/.c;

theorem :: PARTFUN2:36
  c in dom f & c in X implies f/.c in rng (f|X);

definition let C,D; let X,f;
 redefine func X|f -> PartFunc of C,D;
end;

theorem :: PARTFUN2:37
g = X|f iff (for c holds c in dom g iff c in dom f & f/.c in X) &
            (for c st c in dom g holds g/.c = f/.c);

theorem :: PARTFUN2:38
  c in dom (X|f) iff c in dom f & f/.c in X;

theorem :: PARTFUN2:39
  c in dom (X|f) implies X|f/.c = f/.c;



theorem :: PARTFUN2:40
 SD = f.:
X iff for d holds d in SD iff ex c st c in dom f & c in X & d = f/.c;

theorem :: PARTFUN2:41
  d in (f qua Relation of C,D).:X iff ex c st c in dom f & c in X & d = f/.c;

theorem :: PARTFUN2:42
  c in dom f implies f.:{c} = {f/.c};

theorem :: PARTFUN2:43
  c1 in dom f & c2 in dom f implies f.:{c1,c2} = {f/.c1,f/.c2};



theorem :: PARTFUN2:44
SC = f"X iff for c holds c in SC iff c in dom f & f/.c in X;

canceled;

theorem :: PARTFUN2:46
  for f ex g being Function of C,D st for c st c in dom f holds g.c = f/.c;

theorem :: PARTFUN2:47
  f tolerates g iff for c st c in dom f /\ dom g holds f/.c = g/.c;

scheme PartFuncExD{D,C()->non empty set, P[set,set]}:
 ex f being PartFunc of D(),C() st
  (for d be Element of D() holds
      d in dom f iff (ex c be Element of C() st P[d,c])) &
  (for d be Element of D() st d in dom f holds P[d,f/.d]);

scheme LambdaPFD{D,C()->non empty set, F(set)->Element of C(), P[set]}:
  ex f being PartFunc of D(),C() st
   (for d be Element of D() holds d in dom f iff P[d]) &
   (for d be Element of D() st d in dom f holds f/.d = F(d));

scheme UnPartFuncD{C,D()->non empty set, X()->set, F(set)->Element of D()}:
  for f,g being PartFunc of C(),D() st
   (dom f=X() & for c be Element of C() st c in dom f holds f/.c = F(c)) &
   (dom g=X() & for c be Element of C() st c in dom g holds g/.c = F(c))
  holds f = g;

definition let C,D; let SC,d;
redefine func SC --> d -> PartFunc of C,D;
end;

theorem :: PARTFUN2:48
c in SC implies (SC --> d)/.c = d;

theorem :: PARTFUN2:49
  (for c st c in dom f holds f/.c = d) implies f = dom f --> d;

theorem :: PARTFUN2:50
  c in dom f implies f*(SE --> c) = SE --> f/.c;

theorem :: PARTFUN2:51
  (id SC) is total iff SC = C;

theorem :: PARTFUN2:52
  (SC --> d) is total implies SC <> {};

theorem :: PARTFUN2:53
  (SC --> d) is total iff SC = C;

::
:: PARTIAL FUNCTION CONSTANT ON SET
::

definition let C,D; let f,X;
 canceled 2;

pred f is_constant_on X means
:: PARTFUN2:def 3
 ex d st for c st c in X /\ dom f holds f/.c = d;
end;

canceled;

theorem :: PARTFUN2:55
  f is_constant_on X iff
 for c1,c2 st c1 in X /\ dom f & c2 in X /\ dom f holds f/.c1=f/.c2;

theorem :: PARTFUN2:56
  X meets dom f implies (f is_constant_on X iff ex d st rng (f|X) = {d});

theorem :: PARTFUN2:57
  f is_constant_on X & Y c= X implies f is_constant_on Y;

theorem :: PARTFUN2:58
X misses dom f implies f is_constant_on X;

theorem :: PARTFUN2:59
  f|SC = dom (f|SC) --> d implies f is_constant_on SC;

theorem :: PARTFUN2:60
  f is_constant_on {x};

theorem :: PARTFUN2:61
  f is_constant_on X & f is_constant_on Y & X /\ Y meets dom f implies
f is_constant_on X \/ Y;

theorem :: PARTFUN2:62
  f is_constant_on Y implies f|X is_constant_on Y;

theorem :: PARTFUN2:63
  SC --> d is_constant_on SC;

::
::  OF PARTIAL FUNCTION FROM A DOMAIN TO A DOMAIN
::

theorem :: PARTFUN2:64
   f c= g iff dom f c= dom g & (for c st c in dom f holds f/.c = g/.c);

theorem :: PARTFUN2:65
c in dom f & d = f/.c iff [c,d] in f;

theorem :: PARTFUN2:66
  [c,e] in (s*f) implies [c,f/.c] in f & [f/.c,e] in s;

theorem :: PARTFUN2:67
   f = {[c,d]} implies f/.c = d;

theorem :: PARTFUN2:68
  dom f = {c} implies f = {[c,f/.c]};

theorem :: PARTFUN2:69
   f1 = f /\ g & c in dom f1 implies f1/.c = f/.c & f1/.c = g/.c;

theorem :: PARTFUN2:70
  c in dom f & f1 = f \/ g implies f1/.c = f/.c;

theorem :: PARTFUN2:71
  c in dom g & f1 = f \/ g implies f1/.c = g/.c;

theorem :: PARTFUN2:72
  c in dom f1 & f1 = f \/ g implies f1/.c = f/.c or f1/.c = g/.c;

theorem :: PARTFUN2:73
  c in dom f & c in SC iff [c,f/.c] in (f|SC);

theorem :: PARTFUN2:74
  c in dom f & f/.c in SD iff [c,f/.c] in (SD|f);

theorem :: PARTFUN2:75
  c in f"SD iff [c,f/.c] in f & f/.c in SD;

theorem :: PARTFUN2:76
 f is_constant_on X iff
  ex d st for c st c in X /\ dom f holds f.c = d;

theorem :: PARTFUN2:77
  f is_constant_on X iff
 for c1,c2 st c1 in X /\ dom f & c2 in X /\ dom f holds f.c1=f.c2;

theorem :: PARTFUN2:78
    d in f.:X implies ex c st c in dom f & c in X & d = f.c;

theorem :: PARTFUN2:79
  f is one-to-one implies (d in rng f & c = (f").d iff c in dom f & d = f.c);