:: Partial Functions from a Domain to a Domain
:: by Jaros{\l}aw Kotowicz
::
:: Received May 31, 1990
:: Copyright (c) 1990-2017 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 XBOOLE_0, SUBSET_1, PARTFUN1, RELAT_1, FUNCT_1, TARSKI, FUNCOP_1;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1,
FUNCT_2, FUNCOP_1;
constructors PARTFUN1, FUNCOP_1, RELSET_1;
registrations FUNCT_1, RELSET_1;
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;
theorem :: PARTFUN2:1
dom f = dom g & (for c st c in dom f holds f/.c = g/.c) implies f = g;
theorem :: PARTFUN2:2
y in rng f iff ex c st c in dom f & y = f/.c;
theorem :: PARTFUN2:3
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);
theorem :: PARTFUN2:4
c in dom f & f/.c in dom s implies (s*f)/.c = s/.(f/.c);
theorem :: PARTFUN2:5
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;
theorem :: PARTFUN2:6
F = id SD iff dom F = SD & for d st d in SD holds F/.d = d;
theorem :: PARTFUN2:7
d in dom F /\ SD implies F/.d = (F*id SD)/.d;
theorem :: PARTFUN2:8
d in dom((id SD)*F) iff d in dom F & F/.d in SD;
theorem :: PARTFUN2:9
(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:10
f is one-to-one & x in dom f & y in dom f & f/.x = f/.y implies x = y;
definition
let X,Y;
let f be one-to-one PartFunc of X,Y;
redefine func f" -> PartFunc of Y,X;
end;
theorem :: PARTFUN2:11
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;
theorem :: PARTFUN2:12
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:13
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:14
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";
theorem :: PARTFUN2:15
g = f|X iff dom g = dom f /\ X & for c st c in dom g holds g/.c = f/.c;
theorem :: PARTFUN2:16
c in dom f /\ X implies f|X/.c = f/.c;
theorem :: PARTFUN2:17
c in dom f & c in X implies f|X/.c = f/.c;
theorem :: PARTFUN2:18
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:19
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:20
c in dom (X|`f) iff c in dom f & f/.c in X;
theorem :: PARTFUN2:21
c in dom (X|`f) implies X|`f/.c = f/.c;
theorem :: PARTFUN2:22
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:23
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:24
c in dom f implies Im(f,c) = {f/.c};
theorem :: PARTFUN2:25
c1 in dom f & c2 in dom f implies f.:{c1,c2} = {f/.c1,f/.c2};
theorem :: PARTFUN2:26
SC = f"X iff for c holds c in SC iff c in dom f & f/.c in X;
theorem :: PARTFUN2:27
for f ex g being Function of C,D st for c st c in dom f holds g.c = f /.c;
theorem :: PARTFUN2:28
f tolerates g iff for c st c in dom f /\ dom g holds f/.c = g/.c;
scheme :: PARTFUN2:sch 1
PartFuncExD{D,C()->non empty set, P[object,object]}:
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 :: PARTFUN2:sch 2
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 :: PARTFUN2:sch 3
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:29
c in SC implies (SC --> d)/.c = d;
theorem :: PARTFUN2:30
(for c st c in dom f holds f/.c = d) implies f = dom f --> d;
theorem :: PARTFUN2:31
c in dom f implies f*(SE --> c) = SE --> f/.c;
theorem :: PARTFUN2:32
(id SC) is total iff SC = C;
theorem :: PARTFUN2:33
(SC --> d) is total implies SC <> {};
theorem :: PARTFUN2:34
(SC --> d) is total iff SC = C;
::
:: PARTIAL FUNCTION CONSTANT ON SET
::
definition
let C,D,f;
redefine attr f is constant means
:: PARTFUN2:def 1
ex d st for c st c in dom f holds f.c = d;
end;
theorem :: PARTFUN2:35
f|X is constant iff ex d st for c st c in X /\ dom f holds f/.c = d;
theorem :: PARTFUN2:36
f|X is constant iff for c1,c2 st c1 in X /\ dom f & c2 in X /\ dom f
holds f/.c1=f/.c2;
theorem :: PARTFUN2:37
X meets dom f implies (f|X is constant iff ex d st rng (f|X) = {d});
theorem :: PARTFUN2:38
f|X is constant & Y c= X implies f|Y is constant;
theorem :: PARTFUN2:39
X misses dom f implies f|X is constant;
theorem :: PARTFUN2:40
f|SC = dom (f|SC) --> d implies f|SC is constant;
theorem :: PARTFUN2:41
f|{x} is constant;
theorem :: PARTFUN2:42
f|X is constant & f|Y is constant & X /\ Y meets dom f implies f|(X \/
Y) is constant;
theorem :: PARTFUN2:43
f|Y is constant implies f|X|Y is constant;
theorem :: PARTFUN2:44
(SC --> d)|SC is constant;
::
:: OF PARTIAL FUNCTION FROM A DOMAIN TO A DOMAIN
::
theorem :: PARTFUN2:45
dom f c= dom g & (for c st c in dom f holds f/.c = g/.c) implies f c= g;
theorem :: PARTFUN2:46
c in dom f & d = f/.c iff [c,d] in f;
theorem :: PARTFUN2:47
[c,e] in (s*f) implies [c,f/.c] in f & [f/.c,e] in s;
theorem :: PARTFUN2:48
f = {[c,d]} implies f/.c = d;
theorem :: PARTFUN2:49
dom f = {c} implies f = {[c,f/.c]};
theorem :: PARTFUN2:50
f1 = f /\ g & c in dom f1 implies f1/.c = f/.c & f1/.c = g/.c;
theorem :: PARTFUN2:51
c in dom f & f1 = f \/ g implies f1/.c = f/.c;
theorem :: PARTFUN2:52
c in dom g & f1 = f \/ g implies f1/.c = g/.c;
theorem :: PARTFUN2:53
c in dom f1 & f1 = f \/ g implies f1/.c = f/.c or f1/.c = g/.c;
theorem :: PARTFUN2:54
c in dom f & c in SC iff [c,f/.c] in (f|SC);
theorem :: PARTFUN2:55
c in dom f & f/.c in SD iff [c,f/.c] in (SD|`f);
theorem :: PARTFUN2:56
c in f"SD iff [c,f/.c] in f & f/.c in SD;
theorem :: PARTFUN2:57
f|X is constant iff ex d st for c st c in X /\ dom f holds f.c = d;
theorem :: PARTFUN2:58
f|X is constant iff for c1,c2 st c1 in X /\ dom f & c2 in X /\ dom f
holds f.c1=f.c2;
theorem :: PARTFUN2:59
d in f.:X implies ex c st c in dom f & c in X & d = f.c;
theorem :: PARTFUN2:60
f is one-to-one implies (d in rng f & c = (f").d iff c in dom f & d = f.c);
theorem :: PARTFUN2:61
for Y for f,g be Y-valued Function st f c= g
for x st x in dom f holds f/.x = g/.x;