:: Partial Functions
:: by Czes{\l}aw Byli\'nski
::
:: Received September 18, 1989
:: Copyright (c) 1990-2026 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;
definitions TARSKI, FUNCT_1, XBOOLE_0, RELAT_1, RELAT_2;
equalities TARSKI, RELAT_1;
expansions TARSKI, FUNCT_1, XBOOLE_0, RELAT_2;
theorems TARSKI, FUNCT_1, GRFUNC_1, ZFMISC_1, RELAT_1, RELSET_1, XBOOLE_0,
XBOOLE_1, XTUPLE_0;
schemes FUNCT_1, XBOOLE_0;
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 Th1:
for f,g being Function st
for x being object st x in dom f /\ dom g holds f.x = g.x
holds f \/ g is Function
proof
let f,g be Function such that
A1: for x being object st x in dom f /\ dom g holds f.x = g.x;
defpred P[object,object] means [$1,$2] in f \/ g;
A2: for x,y1,y2 being object st P[x,y1] & P[x,y2] holds y1 = y2
proof
let x,y1,y2 be object such that
A3: [x,y1] in f \/ g and
A4: [x,y2] in f \/ g;
now
[x,y1] in f or [x,y1] in g by A3,XBOOLE_0:def 3;
then
A5: x in dom f & f.x = y1 or x in dom g & g.x = y1 by FUNCT_1:1;
A6: [x,y2] in f or [x,y2] in g by A4,XBOOLE_0:def 3;
then
A7: x in dom f & f.x = y2 or x in dom g & g.x = y2 by FUNCT_1:1;
per cases by A6,XTUPLE_0:def 12;
suppose
x in dom f & x in dom g;
then x in dom f /\ dom g by XBOOLE_0:def 4;
hence thesis by A1,A5,A7;
end;
suppose
x in dom f & not x in dom g;
hence thesis by A6,A5,FUNCT_1:1;
end;
suppose
not x in dom f & x in dom g;
hence thesis by A6,A5,FUNCT_1:1;
end;
end;
hence thesis;
end;
consider h being Function such that
A8: for x,y being object holds [x,y] in h iff x in dom f \/ dom g & P[x,y]
from FUNCT_1:sch 1(A2);
h = f \/ g
proof
let x,y be object;
thus [x,y] in h implies [x,y] in f\/g by A8;
assume
A9: [x,y] in f\/g;
[x,y] in f or [x,y] in g by A9,XBOOLE_0:def 3;
then x in dom f or x in dom g by XTUPLE_0:def 12;
then x in dom f \/ dom g by XBOOLE_0:def 3;
hence thesis by A8,A9;
end;
hence thesis;
end;
theorem Th2:
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
proof
let f,g,h be Function such that
A1: f \/ g = h;
let x be object;
assume
A2: x in dom f /\ dom g;
then x in dom f by XBOOLE_0:def 4;
then
A3: h.x = f.x by A1,GRFUNC_1:15;
x in dom g by A2,XBOOLE_0:def 4;
hence thesis by A1,A3,GRFUNC_1:15;
end;
scheme
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));
defpred P[object,object] means
(C[$1] implies $2 = F($1)) & (not C[$1] implies $2
= G($1));
A1: for x being object st x in A() ex y being object st P[x,y]
proof
let x be object;
not C[x] implies (C[x] implies G(x) = F(x)) & (not C[x] implies G(x) =
G(x));
hence thesis;
end;
A2: for x,y1,y2 being object st x in A() & P[x,y1] & P[x,y2] holds y1 = y2;
thus ex f being Function st dom f = A() &
for x being object st x in A() holds P[x,f.x]
from FUNCT_1:sch 2(A2,A1);
end;
Lm1: now
let X,Y;
take E = {};
thus dom E c= X & rng E c= Y;
end;
registration
let X,Y;
cluster Function-like for Relation of X,Y;
existence
proof
consider E being Function such that
A1: dom E c= X & rng E c= Y by Lm1;
reconsider E as Relation of X,Y by A1,RELSET_1:4;
take E;
thus thesis;
end;
end;
definition
let X,Y;
mode PartFunc of X,Y is Function-like Relation of X,Y;
end;
theorem
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
proof
let f be PartFunc of X,Y;
assume y in rng f;
then ex x being object st x in dom f & y = f.x by FUNCT_1:def 3;
hence thesis;
end;
theorem Th4:
for f being Y-valued Function st x in dom f holds f.x in Y
proof
let f be Y-valued Function;
assume x in dom f;
then
A1: f.x in rng f by FUNCT_1:def 3;
rng f c= Y by RELAT_1:def 19;
hence thesis by A1;
end;
theorem
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
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
A1: for x,y being object st x in X() & P[x,y] holds y in Y() and
A2: for x,y1,y2 being object st x in X() & P[x,y1] & P[x,y2] holds y1 = y2
proof
A3: now
defpred R[object] means ex y being object st P[$1,y];
set y1 = the set;
assume Y() <> {};
defpred Q[object,object] means
((ex y being object st P[$1,y]) implies P[$1,$2]) &
((for y being object
holds not P[$1,y]) implies $2=y1);
A4: for x being object st x in X() ex z being object st Q[x,z]
proof
let x being object such that
x in X();
(for y being object holds not P[x,y]) implies
((ex y being object st P[x,y]) implies P[x,y1])
& ((for y being object holds not P[x,y]) implies y1=y1);
hence thesis;
end;
A5: for x,z1,z2 being object st x in X() & Q[x,z1] & Q[x,z2] holds z1 = z2
by A2;
consider g being Function such that
A6: dom g = X() and
A7: for x being object st x in X() holds Q[x,g.x] from FUNCT_1:sch 2(A5,A4);
consider X being set such that
A8: for x being object holds x in X iff x in X() & R[x] from XBOOLE_0:sch 1;
set f=g|X;
A9: dom f c= X() by A6,RELAT_1:60;
rng f c= Y()
proof
let y be object;
assume y in rng f;
then consider x being object such that
A10: x in dom f and
A11: y = f.x by FUNCT_1:def 3;
A12: dom f c= X by RELAT_1:58;
then x in X() & ex y being object st P[x,y] by A8,A10;
then P[x,g.x] by A7;
then
A13: P[x,y] by A10,A11,FUNCT_1:47;
x in X() by A8,A10,A12;
hence thesis by A1,A13;
end;
then reconsider f as PartFunc of X(),Y() by A9,RELSET_1:4;
take f;
thus for x being object holds x in dom f iff x in X() &
ex y being object st P[x,y]
proof
let x be object;
dom f c= X by RELAT_1:58;
hence x in dom f implies x in X() & ex y being object st P[x,y] by A8;
assume that
A14: x in X() and
A15: ex y being object st P[x,y];
x in X by A8,A14,A15;
then x in dom g /\ X by A6,A14,XBOOLE_0:def 4;
hence thesis by RELAT_1:61;
end;
let x be object;
assume
A16: x in dom f;
dom f c= X by RELAT_1:58;
then ex y being object st P[x,y] by A8,A16;
then P[x,g.x] by A7,A16;
hence P[x,f.x] by A16,FUNCT_1:47;
end;
now
consider f being Function such that
A17: dom f c= X() & rng f c= Y() by Lm1;
reconsider f as PartFunc of X(),Y() by A17,RELSET_1:4;
assume
A18: Y() = {};
take f;
thus for x being object holds x in dom f
iff x in X() & ex y being object st P[x,y] by A1,A18;
thus for x being object st x in dom f holds P[x,f.x] by A18;
end;
hence thesis by A3;
end;
scheme
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
A1: for x being object st P[x] holds F(x) in Y()
proof
defpred Q[object,object] means P[$1] & $2 = F($1);
A2: for x,y1,y2 being object st x in X() & Q[x,y1] & Q[x,y2] holds y1 = y2;
A3: for x,y being object st x in X() & Q[x,y] holds y in Y() by A1;
consider f being PartFunc of X(),Y() such that
A4: for x being object holds x in dom f iff x in X() &
ex y being object st Q[x,y] and
A5: for x being object st x in dom f holds Q[x,f.x] from PartFuncEx(A3,A2);
take f;
thus for x being object holds x in dom f iff x in X() & P[x]
proof
let x be object;
thus x in dom f implies x in X() & P[x]
proof
assume
A6: x in dom f;
then ex y being object st P[x] & y = F(x) by A4;
hence thesis by A6;
end;
assume that
A7: x in X() and
A8: P[x];
ex y st P[x] & y = F(x) by A8;
hence thesis by A4,A7;
end;
thus thesis by A5;
end;
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; :: redefines * (FUNCT_1, synonym) → * (RELAT_1, synonym) → (#) (RELAT_1, definition)
coherence
proof
A1: dom(g*f) c= X;
rng(g*f) c= Z by RELAT_1:def 19;
hence thesis by A1,RELSET_1:4;
end;
end;
theorem
for f being Relation of X,Y holds (id X)*f = f
proof
let f be Relation of X,Y;
dom f c= X;
hence thesis by RELAT_1:51;
end;
theorem
for f being Relation of X,Y holds f*(id Y) = f
proof
let f be Relation of X,Y;
rng f c= Y;
hence thesis by RELAT_1:53;
end;
theorem
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
for f being PartFunc of X,Y st f is one-to-one holds f" is PartFunc of Y,X
proof
let f be PartFunc of X,Y such that
A1: f is one-to-one;
rng f c= Y by RELAT_1:def 19;
then
A2: dom(f") c= Y by A1,FUNCT_1:33;
dom f c= X;
then rng(f") c= X by A1,FUNCT_1:33;
hence thesis by A2,RELSET_1:4;
end;
theorem
for f being PartFunc of X,Y holds f|Z is PartFunc of Z,Y
proof
let f be PartFunc of X,Y;
dom(f|Z) c= Z & rng(f|Z) c= Y by RELAT_1:58,def 19;
hence thesis by RELSET_1:4;
end;
theorem Th11:
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; :: redefines | (RELAT_1, definition)
coherence by Th11;
end;
theorem
for f being PartFunc of X,Y holds Z|`f is PartFunc of X,Z
proof
let f be PartFunc of X,Y;
dom(Z|`f) c= X & rng(Z|`f) c= Z by RELAT_1:85;
hence thesis by RELSET_1:4;
end;
theorem
for f being PartFunc of X,Y holds Z|`f is PartFunc of X,Y;
theorem Th14:
for f being Function holds Y|`f|X is PartFunc of X,Y
proof
let f be Function;
Y|`f|X = Y|`(f|X) by RELAT_1:109;
then dom(Y|`f|X) c= X & rng(Y|`f|X) c= Y by RELAT_1:58,85;
hence thesis by RELSET_1:4;
end;
theorem
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
proof
let f be PartFunc of X,Y;
assume y in f.:X;
then ex x being object st x in dom f & x in X & y = f.x by FUNCT_1:def 6;
hence thesis;
end;
:: Partial function from a singelton into set
theorem Th16:
for f being PartFunc of {x},Y holds rng f c= {f.x}
proof
let f be PartFunc of {x},Y;
dom f = {} or dom f = {x} by ZFMISC_1:33;
hence thesis by FUNCT_1:4,RELAT_1:42;
end;
theorem
for f being PartFunc of {x},Y holds f is one-to-one
proof
let f be PartFunc of {x},Y;
let x1,x2 be object;
assume that
A1: x1 in dom f and
A2: x2 in dom f;
dom f<>{} implies x1 = x & x2 = x by A1,A2,TARSKI:def 1;
hence thesis by A1;
end;
theorem
for f being PartFunc of {x},Y holds f.:P c= {f.x}
proof
let f be PartFunc of {x},Y;
f.:P c= rng f & rng f c= {f.x} by Th16,RELAT_1:111;
hence thesis;
end;
theorem
for f being Function st dom f = {x} & x in X & f.x in Y holds f is
PartFunc of X,Y
proof
let f be Function;
assume that
A1: dom f = {x} and
A2: x in X and
A3: f.x in Y;
rng f = {f.x} by A1,FUNCT_1:4;
then
A4: rng f c= Y by A3,ZFMISC_1:31;
dom f c= X by A1,A2,ZFMISC_1:31;
hence thesis by A4,RELSET_1:4;
end;
:: Partial function from a set into a singelton
theorem Th20:
for f being PartFunc of X,{y} st x in dom f holds f.x = y
proof
let f be PartFunc of X,{y};
x in dom f implies f.x in {y} by Th4;
hence thesis by TARSKI:def 1;
end;
theorem
for f1,f2 being PartFunc of X,{y} st dom f1 = dom f2 holds f1 = f2
proof
let f1,f2 be PartFunc of X,{y} such that
A1: dom f1 = dom f2;
for x being object holds x in dom f1 implies f1.x = f2.x
proof let x be object;
assume
A2: x in dom f1;
then f1.x = y by Th20;
hence thesis by A1,A2,Th20;
end;
hence thesis by A1;
end;
:: 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
Y|`f|X;
coherence by Th14;
end;
theorem Th22:
for f being Function holds <:f,X,Y:> c= f
proof
let f be Function;
(Y|`f|X) c= (Y|`f) & (Y|`f) c= f by RELAT_1:59,86;
hence thesis;
end;
theorem Th23:
for f being Function holds dom <:f,X,Y:> c= dom f & rng <:f,X,Y :> c= rng f
proof
let f be Function;
<:f,X,Y:> c= f by Th22;
hence thesis by RELAT_1:11;
end;
theorem Th24:
for f being Function holds x in dom <:f,X,Y:> iff x in dom f & x
in X & f.x in Y
proof
let f be Function;
thus x in dom <:f,X,Y:> implies x in dom f & x in X & f.x in Y
proof
assume
A1: x in dom <:f,X,Y:>;
then x in dom(Y|`f) /\ X by RELAT_1:61;
then x in dom(Y|`f) by XBOOLE_0:def 4;
hence thesis by A1,FUNCT_1:54;
end;
assume that
A2: x in dom f and
A3: x in X and
A4: f.x in Y;
x in dom(Y|`f) by A2,A4,FUNCT_1:54;
then x in dom(Y|`f) /\ X by A3,XBOOLE_0:def 4;
hence thesis by RELAT_1:61;
end;
theorem Th25:
for f being Function st x in dom f & x in X & f.x in Y holds <:f
,X,Y:>.x = f.x
proof
let f be Function such that
A1: x in dom f and
A2: x in X and
A3: f.x in Y;
x in dom(Y|`f) by A1,A3,FUNCT_1:54;
then f.x = (Y|`f).x by FUNCT_1:55
.= (Y|`f|X).x by A2,FUNCT_1:49;
hence thesis;
end;
theorem Th26:
for f being Function st x in dom <:f,X,Y:> holds <:f,X,Y:>.x = f .x
proof
let f be Function;
assume
A1: x in dom <:f,X,Y:>;
then x in dom f & f.x in Y by Th24;
hence thesis by A1,Th25;
end;
theorem
for f,g being Function st f c= g holds <:f,X,Y:> c= <:g,X,Y:>
proof
let f,g be Function such that
A1: f c= g;
A2: dom <:f,X,Y:> c= dom f by Th23;
now
thus
A3: dom <:f,X,Y:> c= dom <:g,X,Y:>
proof
let x be object;
A4: dom f c= dom g by A1,RELAT_1:11;
assume
A5: x in dom <:f,X,Y:>;
then
A6: f.x = g.x by A1,A2,GRFUNC_1:2;
x in dom f & f.x in Y by A5,Th24;
hence thesis by A5,A4,A6,Th24;
end;
let x be object;
assume
A7: x in dom <:f,X,Y:>;
then
A8: <:f,X,Y:>.x = f.x by Th26;
<:g,X,Y:>.x = g.x by A3,A7,Th26;
hence <:f,X,Y:>.x = <:g,X,Y:>.x by A1,A2,A7,A8,GRFUNC_1:2;
end;
hence thesis by GRFUNC_1:2;
end;
theorem Th28:
for f being Function st Z c= X holds <:f,Z,Y:> c= <:f,X,Y:>
proof
let f be Function such that
A1: Z c= X;
A2: dom <:f,Z,Y:> c= dom <:f,X,Y:>
proof
let x be object;
assume
A3: x in dom <:f,Z,Y:>;
then
A4: f.x in Y by Th24;
x in Z & x in dom f by A3,Th24;
hence thesis by A1,A4,Th24;
end;
now
let x be object;
assume
A5: x in dom <:f,Z,Y:>;
then <:f,Z,Y:>.x = f.x by Th26;
hence <:f,Z,Y:>.x = <:f,X,Y:>.x by A2,A5,Th26;
end;
hence thesis by A2,GRFUNC_1:2;
end;
theorem Th29:
for f being Function st Z c= Y holds <:f,X,Z:> c= <:f,X,Y:>
proof
let f be Function such that
A1: Z c= Y;
A2: dom <:f,X,Z:> c= dom <:f,X,Y:>
proof
let x be object;
assume
A3: x in dom <:f,X,Z:>;
then f.x in Z & x in dom f by Th24;
hence thesis by A1,A3,Th24;
end;
now
let x be object;
assume
A4: x in dom <:f,X,Z:>;
then <:f,X,Z:>.x = f.x by Th26;
hence <:f,X,Z:>.x = <:f,X,Y:>.x by A2,A4,Th26;
end;
hence thesis by A2,GRFUNC_1:2;
end;
theorem
for f being Function st X1 c= X2 & Y1 c= Y2 holds <:f,X1,Y1:> c= <:f, X2,Y2:>
proof
let f be Function;
assume X1 c= X2 & Y1 c= Y2;
then <:f,X1,Y1:> c= <:f,X2,Y1:> & <:f,X2,Y1:> c= <:f,X2,Y2:> by Th28,Th29;
hence thesis;
end;
theorem Th31:
for f being Function st dom f c= X & rng f c= Y holds f = <:f,X, Y:>
proof
let f be Function such that
A1: dom f c= X & rng f c= Y;
A2: dom f c= dom <:f,X,Y:>
proof
let x be object;
assume
A3: x in dom f;
then f.x in rng f by FUNCT_1:def 3;
hence thesis by A1,A3,Th24;
end;
dom <:f,X,Y:> c= dom f by Th23;
then
A4: dom f = dom <:f,X,Y:> by A2;
for x being object st x in dom f holds f.x = <:f,X,Y:>.x by A2,Th26;
hence thesis by A4;
end;
theorem
for f being Function holds f = <:f,dom f,rng f:>;
theorem
for f being PartFunc of X,Y holds <:f,X,Y:> = f;
theorem Th34:
<:{},X,Y:> = {}
proof
dom {} c= X & rng {} c= Y;
hence thesis by Th31;
end;
theorem Th35:
for f,g being Function holds (<:g,Y,Z:>*<:f,X,Y:>) c= <:g*f,X,Z :>
proof
let f,g be Function;
A1: for x being object
st x in dom (<:g,Y,Z:>*<:f,X,Y:>) holds (<:g,Y,Z:>*<:f,X,Y:>).x =
<:g*f,X,Z:>.x
proof
let x be object;
assume
A2: x in dom (<:g,Y,Z:>*<:f,X,Y:>);
then
A3: x in dom<:f,X,Y:> by FUNCT_1:11;
then
A4: x in dom f by Th24;
<:f,X,Y:>.x in dom<:g,Y,Z:> by A2,FUNCT_1:11;
then
A5: f.x in dom<:g,Y,Z:> by A3,Th26;
then g.(f.x) in Z by Th24;
then
A6: (g*f).x in Z by A4,FUNCT_1:13;
f.x in dom g by A5,Th24;
then x in dom (g*f) by A4,FUNCT_1:11;
then
A7: x in dom <:g*f,X,Z:> by A2,A6,Th24;
thus (<:g,Y,Z:>*<:f,X,Y:>).x = <:g,Y,Z:>.(<:f,X,Y:>.x) by A2,FUNCT_1:12
.= <:g,Y,Z:>.(f.x) by A3,Th26
.= g.(f.x) by A5,Th26
.= (g*f).x by A4,FUNCT_1:13
.= <:g*f,X,Z:>.x by A7,Th26;
end;
dom (<:g,Y,Z:>*<:f,X,Y:>) c= dom <:g*f,X,Z:>
proof
let x be object;
assume
A8: x in dom (<:g,Y,Z:>*<:f,X,Y:>);
then
A9: x in dom<:f,X,Y:> by FUNCT_1:11;
then
A10: x in dom f by Th24;
<:f,X,Y:>.x in dom<:g,Y,Z:> by A8,FUNCT_1:11;
then
A11: f.x in dom<:g,Y,Z:> by A9,Th26;
then g.(f.x) in Z by Th24;
then
A12: (g*f).x in Z by A10,FUNCT_1:13;
f.x in dom g by A11,Th24;
then x in dom (g*f) by A10,FUNCT_1:11;
hence thesis by A8,A12,Th24;
end;
hence thesis by A1,GRFUNC_1:2;
end;
theorem
for f,g being Function st rng f /\ dom g c= Y holds <:g,Y,Z:>*<:f,X,Y
:> = <:g*f,X,Z:>
proof
let f,g be Function such that
A1: rng f /\ dom g c= Y;
A2: dom <:g*f,X,Z:> c= dom (<:g,Y,Z:>*<:f,X,Y:>)
proof
let x be object;
assume
A3: x in dom <:g*f,X,Z:>;
then
A4: x in dom (g*f) by Th24;
then
A5: f.x in dom g by FUNCT_1:11;
A6: x in dom f by A4,FUNCT_1:11;
then f.x in rng f by FUNCT_1:def 3;
then
A7: f.x in rng f /\ dom g by A5,XBOOLE_0:def 4;
(g*f).x in Z by A3,Th24;
then g.(f.x) in Z by A4,FUNCT_1:12;
then
A8: f.x in dom <:g,Y,Z:> by A1,A5,A7,Th24;
x in dom <:f,X,Y:> & <:f,X,Y:>.x = f.x by A1,A3,A6,A7,Th24,Th25;
hence thesis by A8,FUNCT_1:11;
end;
for x being object st x in dom <:g*f,X,Z:>
holds <:g*f,X,Z:>.x = (<:g,Y,Z:>*<:f,X,Y :>).x
proof
let x be object;
assume
A9: x in dom <:g*f,X,Z:>;
then
A10: x in dom (g*f) by Th24;
then
A11: f.x in dom g by FUNCT_1:11;
x in dom f by A10,FUNCT_1:11;
then f.x in rng f by FUNCT_1:def 3;
then
A12: f.x in rng f /\ dom g by A11,XBOOLE_0:def 4;
(g*f).x in Z by A9,Th24;
then g.(f.x) in Z by A10,FUNCT_1:12;
then
A13: f.x in dom <:g,Y,Z:> by A1,A11,A12,Th24;
x in dom f by A10,FUNCT_1:11;
then
A14: x in dom <:f,X,Y:> by A1,A9,A12,Th24;
thus <:g*f,X,Z:>.x = (g*f).x by A9,Th26
.= g.(f.x) by A10,FUNCT_1:12
.= <:g,Y,Z:>.(f.x) by A13,Th26
.= <:g,Y,Z:>.(<:f,X,Y:>.x) by A14,Th26
.= (<:g,Y,Z:>*<:f,X,Y:>).x by A2,A9,FUNCT_1:12;
end;
then
A15: <:g*f,X,Z:> c= (<:g,Y,Z:>*<:f,X,Y:>) by A2,GRFUNC_1:2;
(<:g,Y,Z:>*<:f,X,Y:>) c= <:g*f,X,Z:> by Th35;
hence thesis by A15;
end;
theorem Th37:
for f being Function st f is one-to-one holds <:f,X,Y:> is one-to-one
proof
let f be Function;
assume f is one-to-one;
then Y|`f is one-to-one by FUNCT_1:58;
hence thesis by FUNCT_1:52;
end;
theorem
for f being Function st f is one-to-one holds <:f,X,Y:>" = <:f",Y,X:>
proof
let f be Function;
assume
A1: f is one-to-one;
then
A2: <:f,X,Y:> is one-to-one by Th37;
for y being object holds y in dom (<:f,X,Y:>") iff y in dom <:f",Y,X:>
proof let y be object;
thus y in dom (<:f,X,Y:>") implies y in dom <:f",Y,X:>
proof
assume y in dom (<:f,X,Y:>");
then
A3: y in rng <:f,X,Y:> by A2,FUNCT_1:33;
then consider x being object such that
A4: x in dom <:f,X,Y:> and
A5: y = <:f,X,Y:>.x by FUNCT_1:def 3;
A6: f.x = y by A4,A5,Th26;
then
A7: y in Y by A4,Th24;
rng <:f,X,Y:> c= rng f by Th23;
then y in rng f by A3;
then
A8: y in dom(f") by A1,FUNCT_1:32;
dom <:f,X,Y:> c= dom f by Th23;
then (f").y = x by A1,A4,A6,FUNCT_1:32;
hence thesis by A4,A8,A7,Th24;
end;
assume
A9: y in dom <:f",Y,X:>;
dom <:f",Y,X:> c= dom (f") by Th23;
then y in dom(f") by A9;
then y in rng f by A1,FUNCT_1:33;
then consider x being object such that
A10: x in dom f and
A11: y = f.x by FUNCT_1:def 3;
x =(f").(f.x) by A1,A10,FUNCT_1:34;
then x in X by A9,A11,Th24;
then x in dom <:f,X,Y:> by A9,A10,A11,Th24;
then <:f,X,Y:>.x in rng <:f,X,Y:> & <:f,X,Y:>.x = f.x by Th26,FUNCT_1:def 3
;
hence thesis by A2,A11,FUNCT_1:33;
end;
then
A12: dom (<:f,X,Y:>") = dom <:f",Y,X:> by TARSKI:2;
for y being object st y in dom <:f",Y,X:>
holds <:f",Y,X:>.y = (<:f,X,Y:>").y
proof
let y be object;
A13: rng <:f,X,Y:> c= rng f by Th23;
assume
A14: y in dom <:f",Y,X:>;
then y in rng <:f,X,Y:> by A2,A12,FUNCT_1:33;
then consider x being object such that
A15: x in dom f and
A16: y = f.x by A13,FUNCT_1:def 3;
A17: x =(f").(f.x) by A1,A15,FUNCT_1:34;
then x in X by A14,A16,Th24;
then x in dom<:f,X,Y:> by A14,A15,A16,Th24;
then (<:f,X,Y:>").(<:f,X,Y:>.x) = x & <:f,X,Y:>.x = f.x by A2,Th26,
FUNCT_1:34;
hence thesis by A14,A16,A17,Th26;
end;
hence thesis by A12;
end;
theorem
for f being Function holds Z|`<:f,X,Y:> = <:f,X,Z /\ Y:>
proof
let f be Function;
thus Z|`<:f,X,Y:> = Z|`(Y|`(f|X)) by RELAT_1:109
.= (Z /\ Y)|`(f|X) by RELAT_1:96
.= <:f,X,Z /\ Y:> by RELAT_1:109;
end;
:: Total Function
definition
let X;
let f be X-defined Relation;
attr f is total means
dom f = X;
end;
registration
let X be empty set, Y be set;
cluster -> total for Relation of X,Y;
coherence;
end;
registration
let X be non empty set, Y be empty set;
cluster -> non total for Relation of X,Y;
coherence;
end;
theorem Th40:
for f being Function st <:f,X,Y:> is total holds X c= dom f
by Th23;
theorem
<:{},X,Y:> is total implies X = {}
proof
dom {} = {};
hence thesis by Th40,XBOOLE_1:3;
end;
theorem
for f being Function st X c= dom f & rng f c= Y holds <:f,X,Y:> is total
proof
let f be Function such that
A1: X c= dom f and
A2: rng f c= Y;
X c= dom <:f,X,Y:>
proof
let x be object;
assume
A3: x in X;
then f.x in rng f by A1,FUNCT_1:def 3;
hence thesis by A1,A2,A3,Th24;
end;
hence dom <:f,X,Y:> = X;
end;
theorem
for f being Function st <:f,X,Y:> is total holds f.:X c= Y
proof
let f be Function such that
A1: dom <:f,X,Y:> = X;
let y be object;
A2: rng <:f,X,Y:> c= Y by RELAT_1:def 19;
assume y in f.:X;
then consider x being object such that
x in dom f and
A3: x in X & y = f.x by FUNCT_1:def 6;
<:f,X,Y:>.x = y & <:f,X,Y:>.x in rng <:f,X,Y:> by A1,A3,Th26,FUNCT_1:def 3;
hence thesis by A2;
end;
theorem
for f being Function st X c= dom f & f.:X c= Y holds <:f,X,Y:> is total
proof
let f be Function such that
A1: X c= dom f and
A2: f.:X c= Y;
X c= dom <:f,X,Y:>
proof
let x be object;
assume
A3: x in X;
then f.x in f.:X by A1,FUNCT_1:def 6;
hence thesis by A1,A2,A3,Th24;
end;
hence dom <:f,X,Y:> = X;
end;
:: set of partial functions from a set into a set
definition
let X,Y;
func PFuncs(X,Y) -> set means
:Def3:
x in it iff ex f being Function st x = f & dom f c= X & rng f c= Y;
existence
proof
defpred P[object] means
ex f be Function st $1 = f & dom f c= X & rng f c= Y;
consider F being set such that
A1: for z being object holds z in F iff z in bool [:X,Y:] & P[z]
from XBOOLE_0:sch 1;
take F;
let z;
thus z in F implies ex f being Function st z = f & dom f c= X & rng f c= Y
by A1;
given f being Function such that
A2: z = f and
A3: dom f c= X & rng f c= Y;
f c= [:X,Y:]
proof
let x,y be object;
assume
A4: [x,y] in f;
reconsider y as set by TARSKI:1;
A5: x in dom f by XTUPLE_0:def 12,A4;
then y = f.x by A4,FUNCT_1:def 2;
then y in rng f by A5,FUNCT_1:def 3;
hence thesis by A3,A5,ZFMISC_1:def 2;
end;
hence thesis by A1,A2,A3;
end;
uniqueness
proof
let F1,F2 be set such that
A6: x in F1 iff ex f being Function st x = f & dom f c= X & rng f c= Y and
A7: x in F2 iff ex f being Function st x = f & dom f c= X & rng f c= Y;
for x being object holds x in F1 iff x in F2
proof let x be object;
x in F1 iff ex f being Function st x = f & dom f c= X & rng f c= Y by A6;
hence thesis by A7;
end;
hence thesis by TARSKI:2;
end;
end;
registration
let X,Y;
cluster PFuncs(X,Y) -> non empty;
coherence
proof
ex f being Function st dom f c= X & rng f c= Y by Lm1;
hence thesis by Def3;
end;
end;
theorem Th45:
for f being PartFunc of X,Y holds f in PFuncs(X,Y)
proof
let f be PartFunc of X,Y;
dom f c= X & rng f c= Y by RELAT_1:def 19;
hence thesis by Def3;
end;
theorem Th46:
for f being set st f in PFuncs(X,Y) holds f is PartFunc of X,Y
proof
let f be set;
assume f in PFuncs(X,Y);
then ex F being Function st f = F & dom F c= X & rng F c= Y by Def3;
hence thesis by RELSET_1:4;
end;
theorem
for f being Element of PFuncs(X,Y) holds f is PartFunc of X,Y by Th46;
theorem
PFuncs({},Y) = { {} }
proof
for x be object holds x in PFuncs({},Y) iff x = {}
proof
let x be object;
thus x in PFuncs({},Y) implies x = {}
proof
assume x in PFuncs({},Y);
then x is PartFunc of {},Y by Th46;
hence thesis;
end;
{} is PartFunc of {},Y by RELSET_1:12;
hence thesis by Th45;
end;
hence thesis by TARSKI:def 1;
end;
theorem
PFuncs(X,{}) = { {} }
proof
for x be object holds x in PFuncs(X,{}) iff x = {}
proof
let x be object;
thus x in PFuncs(X,{}) implies x = {}
proof
assume x in PFuncs(X,{});
then x is PartFunc of X,{} by Th46;
hence thesis;
end;
{} is PartFunc of X,{} by RELSET_1:12;
hence thesis by Th45;
end;
hence thesis by TARSKI:def 1;
end;
theorem
X1 c= X2 & Y1 c= Y2 implies PFuncs(X1,Y1) c= PFuncs(X2,Y2)
proof
assume
A1: X1 c= X2 & Y1 c= Y2;
let f be object;
assume f in PFuncs(X1,Y1);
then f is PartFunc of X1,Y1 by Th46;
then f is PartFunc of X2,Y2 by A1,RELSET_1:7;
hence thesis by Th45;
end;
:: Relation of Tolerance on Functions
definition
let f,g be Function;
pred f tolerates g means
for x being object st x in dom f /\ dom g holds f.x = g.x;
reflexivity;
symmetry;
end;
theorem Th51:
for f,g being Function holds
f tolerates g iff f \/ g is Function by Th1,Th2;
theorem Th52:
for f,g being Function holds
f tolerates g iff ex h being Function st f c= h & g c= h
proof
let f,g be Function;
thus f tolerates g implies ex h being Function st f c= h & g c= h
proof
assume f tolerates g;
then reconsider h = f \/ g as Function by Th1;
take h;
thus thesis by XBOOLE_1:7;
end;
given h being Function such that
A1: f c= h & g c= h;
f \/ g is Function by A1,GRFUNC_1:1,XBOOLE_1:8;
hence thesis by Th51;
end;
theorem
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
proof
let f,g be Function;
assume dom f c= dom g;
then dom f /\ dom g = dom f by XBOOLE_1:28;
hence thesis;
end;
theorem
for f,g being Function st f c= g holds f tolerates g by Th52;
theorem
for f,g being Function st dom f = dom g & f tolerates g holds f = g;
theorem
for f,g being Function st dom f misses dom g holds f tolerates g;
theorem
for f,g,h being Function st f c= h & g c= h holds f tolerates g by Th52;
theorem
for f,g being PartFunc of X,Y for h being Function st f tolerates h &
g c= f holds g tolerates h
proof
let f,g be (PartFunc of X,Y),h be Function such that
A1: f tolerates h and
A2: g c= f;
A3: dom g c= dom f by A2,RELAT_1:11;
let x be object;
assume
A4: x in dom g /\ dom h;
then
A5: x in dom g by XBOOLE_0:def 4;
then
A6: f.x = g.x by A2,GRFUNC_1:2;
x in dom h by A4,XBOOLE_0:def 4;
then x in dom f /\ dom h by A5,A3,XBOOLE_0:def 4;
hence thesis by A1,A6;
end;
theorem
for f being Function holds {} tolerates f;
theorem
for f being Function holds <:{},X,Y:> tolerates f
proof
let f be Function;
<:{},X,Y:> = {} by Th34;
hence thesis;
end;
theorem
for f,g being PartFunc of X,{y} holds f tolerates g
proof
let f,g be PartFunc of X,{y};
let x be object;
assume
A1: x in dom f /\ dom g;
then x in dom f by XBOOLE_0:def 4;
then
A2: f.x = y by Th20;
x in dom g by A1,XBOOLE_0:def 4;
hence thesis by A2,Th20;
end;
theorem
for f being Function holds f|X tolerates f
proof
let f be Function;
(f|X) c= f by RELAT_1:59;
hence thesis by Th52;
end;
theorem
for f being Function holds Y|`f tolerates f
proof
let f be Function;
(Y|`f) c= f by RELAT_1:86;
hence thesis by Th52;
end;
theorem Th64:
for f being Function holds Y|`f|X tolerates f
proof
let f be Function;
(Y|`f|X) c= (Y|`f) & (Y|`f) c= f by RELAT_1:59,86;
then (Y|`f|X) c= f;
hence thesis by Th52;
end;
theorem
for f being Function holds <:f,X,Y:> tolerates f by Th64;
theorem Th66:
for f,g being PartFunc of X,Y st f is total & g is total & f
tolerates g holds f = g;
theorem Th67:
for f,g,h being PartFunc of X,Y st f tolerates h & g tolerates
h & h is total holds f tolerates g
proof
let f,g,h be PartFunc of X,Y such that
A1: f tolerates h and
A2: g tolerates h and
A3: dom h = X;
let x be object;
assume
A4: x in dom f /\ dom g;
then x in dom f by XBOOLE_0:def 4;
then x in dom f /\ dom h by A3,XBOOLE_0:def 4;
then
A5: f.x = h.x by A1;
x in dom g by A4,XBOOLE_0:def 4;
then x in dom g /\ dom h by A3,XBOOLE_0:def 4;
hence thesis by A2,A5;
end;
theorem Th68:
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
proof
let f,g be PartFunc of X,Y such that
A1: Y = {} implies X = {} and
A2: f tolerates g;
now
per cases;
suppose
A3: Y = {};
then f tolerates <:{},X,Y:> & g tolerates <:{},X,Y:>;
hence thesis by A1,A3;
end;
suppose
A4: Y <> {};
set y = the Element of Y;
defpred P[object,object] means
($1 in dom f implies $2 = f.$1) & ($1 in dom g
implies $2 = g.$1) & (not $1 in dom f & not $1 in dom g implies $2 = y);
A5: for x being object st x in X ex y9 being object st P[x,y9]
proof
let x be object such that
x in X;
per cases;
suppose
A6: x in dom f & x in dom g;
take y9 = f.x;
thus x in dom f implies y9 = f.x;
x in dom f /\ dom g by A6,XBOOLE_0:def 4;
hence x in dom g implies y9 = g.x by A2;
thus not x in dom f & not x in dom g implies y9 = y by A6;
end;
suppose
A7: x in dom f & not x in dom g;
take y9 = f.x;
thus (x in dom f implies y9 = f.x) & (x in dom g implies y9 = g.x)
& (not x in dom f & not x in dom g implies y9 = y) by A7;
end;
suppose
A8: not x in dom f & x in dom g;
take y9 = g.x;
thus (x in dom f implies y9 = f.x) & (x in dom g implies y9 = g.x)
& (not x in dom f & not x in dom g implies y9 = y) by A8;
end;
suppose
not x in dom f & not x in dom g;
hence thesis;
end;
end;
A9: for x,y1,y2 being object st x in X & P[x,y1] & P[x,y2] holds y1 = y2;
consider h being Function such that
A10: dom h = X and
A11: for x being object st x in X holds P[x,h.x] from FUNCT_1:sch 2(A9,A5);
rng h c= Y
proof
let z be object;
assume z in rng h;
then consider x being object such that
A12: x in dom h and
A13: z = h.x by FUNCT_1:def 3;
per cases;
suppose
A14: x in dom f & x in dom g;
then z = f.x by A11,A13;
hence thesis by A14,Th4;
end;
suppose
A15: x in dom f & not x in dom g;
then z = f.x by A11,A13;
hence thesis by A15,Th4;
end;
suppose
A16: not x in dom f & x in dom g;
then z = g.x by A11,A13;
hence thesis by A16,Th4;
end;
suppose
not x in dom f & not x in dom g;
then z = y by A10,A11,A12,A13;
hence thesis by A4;
end;
end;
then reconsider h9 = h as PartFunc of X,Y by A10,RELSET_1:4;
A17: f tolerates h
proof
let x be object;
assume x in dom f /\ dom h;
then x in dom f by XBOOLE_0:def 4;
hence thesis by A11;
end;
A18: g tolerates h
proof
let x be object;
assume x in dom g /\ dom h;
then x in dom g by XBOOLE_0:def 4;
hence thesis by A11;
end;
h9 is total by A10;
hence thesis by A17,A18;
end;
end;
hence thesis;
end;
definition
let X,Y;
let f be PartFunc of X,Y;
func TotFuncs f -> set means
:Def5: 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;
existence
proof
defpred P[object] means
ex g being PartFunc of X,Y st g = $1 & g is total & f
tolerates g;
now
consider F being set such that
A1: for x being object holds x in F iff x in PFuncs(X,Y) & P[x]
from XBOOLE_0:sch
1;
take F;
let x be object;
thus x in F implies ex g being PartFunc of X,Y st g = x & g is total & f
tolerates g by A1;
given g being PartFunc of X,Y such that
A2: g = x & g is total & f tolerates g;
g in PFuncs(X,Y) by Th45;
hence x in F by A1,A2;
end;
hence thesis;
end;
uniqueness
proof
defpred P[object] means
ex g being PartFunc of X,Y st g = $1 & g is total & f
tolerates g;
let F1,F2 be set such that
A3: for x being object holds x in F1 iff P[x] and
A4: for x being object holds x in F2 iff P[x];
thus thesis from XBOOLE_0:sch 2(A3,A4);
end;
end;
theorem Th69:
for f being PartFunc of X,Y for g being set st g in TotFuncs(f)
holds g is PartFunc of X,Y
proof
let f be PartFunc of X,Y;
let g be set;
assume g in TotFuncs(f);
then
ex g9 being PartFunc of X,Y st g9 = g & g9 is total & f tolerates g9 by Def5;
hence thesis;
end;
theorem Th70:
for f,g being PartFunc of X,Y st g in TotFuncs(f) holds g is total
proof
let f,g be PartFunc of X,Y;
assume g in TotFuncs(f);
then
ex g9 being PartFunc of X,Y st g9 = g & g9 is total & f tolerates g9 by Def5;
hence thesis;
end;
theorem Th71:
for f being PartFunc of X,Y for g being Function st g in
TotFuncs(f) holds f tolerates g
proof
let f be PartFunc of X,Y;
let g be Function;
assume g in TotFuncs(f);
then
ex g9 being PartFunc of X,Y st g9 = g & g9 is total & f tolerates g9 by Def5;
hence thesis;
end;
registration
let X be non empty set, Y be empty set;
let f be PartFunc of X,Y;
cluster TotFuncs f -> empty;
coherence
proof
set g = the Element of TotFuncs(f);
assume TotFuncs(f) is not empty;
then
ex g9 being PartFunc of X,{} st g9 = g & g9 is total & f tolerates g9
by Def5;
hence contradiction;
end;
end;
theorem Th72:
for f being PartFunc of X,Y holds f is total iff TotFuncs f = { f}
proof
let f be PartFunc of X,Y;
thus f is total implies TotFuncs f = {f}
proof
assume
A1: f is total;
for g being object holds g in TotFuncs f iff f = g
proof
let g be object;
thus g in TotFuncs f implies f = g
proof
assume g in TotFuncs f;
then
ex g9 being PartFunc of X,Y st g9 = g & g9 is total & f tolerates
g9 by Def5;
hence thesis by A1,Th66;
end;
thus thesis by A1,Def5;
end;
hence thesis by TARSKI:def 1;
end;
assume TotFuncs f = {f};
then f in TotFuncs f by TARSKI:def 1;
hence thesis by Th70;
end;
theorem
for f being PartFunc of {},Y holds TotFuncs f = {f} by Th72;
theorem
for f being PartFunc of {},Y holds TotFuncs f = {{}} by Th72;
theorem
for f,g being PartFunc of X,Y st TotFuncs f meets TotFuncs g holds f
tolerates g
proof
let f,g be PartFunc of X,Y;
set h = the Element of TotFuncs f /\ TotFuncs g;
assume
A1: TotFuncs f /\ TotFuncs g <> {};
then
A2: h in TotFuncs f by XBOOLE_0:def 4;
A3: h in TotFuncs g by A1,XBOOLE_0:def 4;
reconsider h as PartFunc of X,Y by A2,Th69;
A4: g tolerates h by A3,Th71;
f tolerates h by A2,Th71;
hence thesis by A2,A4,Th67,Th70;
end;
theorem
for f,g being PartFunc of X,Y st (Y = {} implies X = {}) & f tolerates
g holds TotFuncs f meets TotFuncs g
proof
let f,g be PartFunc of X,Y;
assume ( Y = {} implies X = {})& f tolerates g;
then consider h being PartFunc of X,Y such that
A1: h is total & f tolerates h & g tolerates h by Th68;
h in TotFuncs f & h in TotFuncs g by A1,Def5;
hence TotFuncs f /\ TotFuncs g <> {} by XBOOLE_0:def 4;
end;
begin :: id X as a relation of X
Lm2: for R being Relation of X st R = id X holds R is total;
Lm3: for R being Relation st R = id X holds R is reflexive symmetric
antisymmetric transitive
proof
let R be Relation;
assume
A1: R = id X;
thus R is_reflexive_in field R
by A1,RELAT_1:def 10;
thus R is_symmetric_in field R
by A1,RELAT_1:def 10;
thus R is_antisymmetric_in field R
by A1,RELAT_1:def 10;
thus R is_transitive_in field R
by A1,RELAT_1:def 10;
end;
Lm4: id X is Relation of X
proof
dom id X c= X & rng id X c= X;
hence thesis by RELSET_1:4;
end;
registration
let X;
cluster total reflexive symmetric antisymmetric transitive for Relation of X;
existence
proof
reconsider R = id X as Relation of X by Lm4;
take R;
thus thesis by Lm3;
end;
end;
registration
cluster symmetric transitive -> reflexive for Relation;
coherence
proof
let R be Relation;
assume that
A1: R is_symmetric_in field R and
A2: R is_transitive_in field R;
let x be object;
assume
A3: x in field R;
then x in dom R or x in rng R by XBOOLE_0:def 3;
then consider y being object such that
A4: [x,y] in R or [y,x] in R by XTUPLE_0:def 12,def 13;
y in rng R or y in dom R by A4,XTUPLE_0:def 12,def 13;
then
A5: y in field R by XBOOLE_0:def 3;
then [x,y] in R & [y,x] in R by A1,A3,A4;
hence thesis by A2,A3,A5;
end;
end;
registration
let X;
cluster id X -> symmetric antisymmetric transitive;
coherence by Lm3;
end;
definition
let X;
redefine func id X -> total Relation of X; :: redefines id (RELAT_1, definition)
coherence by Lm2,Lm4;
end;
scheme
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));
consider f being Function such that
A1: dom f = A() & for x be object st x in A() holds (C[x] implies f.x = F(x
)) & (not C[x] implies f.x = G(x)) from LambdaC;
take f;
thus thesis by A1;
end;
begin :: Addenda
:: from AMI_1, 2007,07,20, A.T.
reserve A for set,
f,g,h for Function;
theorem Th77:
for x,y,z being object holds
f tolerates g & [x,y] in f & [x,z] in g implies y = z
proof let x,y,z be object;
set h = f \/ g;
assume f tolerates g;
then
A1: h is Function by Th51;
assume [x,y] in f & [x,z] in g;
then [x,y] in h & [x,z] in h by XBOOLE_0:def 3;
hence thesis by A1,FUNCT_1:def 1;
end;
theorem
A is functional &
(for f,g being Function st f in A & g in A holds f tolerates g)
implies union A is Function
proof
assume that
A1: for x st x in A holds x is Function and
A2: for f,g being Function st f in A & g in A holds f tolerates g;
A3: now
let x,y,z be object;
assume that
A4: [x,y] in union A and
A5: [x,z] in union A;
consider p being set such that
A6: [x,y] in p and
A7: p in A by A4,TARSKI:def 4;
consider q being set such that
A8: [x,z] in q and
A9: q in A by A5,TARSKI:def 4;
reconsider p,q as Function by A1,A7,A9;
p tolerates q by A2,A7,A9;
hence y = z by A6,A8,Th77;
end;
now
let z be object;
assume z in union A;
then consider p being set such that
A10: z in p and
A11: p in A by TARSKI:def 4;
reconsider p as Function by A1,A11;
p = p;
hence ex x,y being object st [x,y] = z by A10,RELAT_1:def 1;
end;
hence thesis by A3,FUNCT_1:def 1,RELAT_1:def 1;
end;
:: Moved from FINSEQ_4 by AK on 2007.10.09
definition
let D be set, p be D-valued Function, i be object;
assume
A1: i in dom p;
func p/.i -> Element of D equals
:Def6: p.i;
coherence by A1,Th4;
end;
:: missing, 2008.09.15, A.T.
registration
let X,Y be non empty set;
cluster non empty for PartFunc of X,Y;
existence
proof
reconsider p = {[the Element of X,the Element of Y]}
as PartFunc of X,Y by RELSET_1:3;
take p;
thus thesis;
end;
end;
:: from FRAENKEL, 2009.05.06, A.K.
registration
let A, B be set;
cluster PFuncs(A,B) -> functional;
coherence
proof
let x be object;
assume x in PFuncs(A,B);
then ex f being Function st x = f & dom f c= A & rng f c= B by Def3;
hence thesis;
end;
end;
:: from CIRCCOMB, 2011.04.19, A.T.
theorem
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
proof
let f1,f2, g be Function;
assume that
A1: rng g c= dom f1 and
A2: rng g c= dom f2 and
A3: f1 tolerates f2;
A4: dom (f2*g) = dom g by A2,RELAT_1:27;
A5: dom (f1*g) = dom g by A1,RELAT_1:27;
now
let x be object;
assume
A6: x in dom g;
then
A7: (f2*g).x = f2.(g.x) by A4,FUNCT_1:12;
g.x in rng g by A6,FUNCT_1:def 3;
then
A8: g.x in (dom f1) /\ (dom f2) by A1,A2,XBOOLE_0:def 4;
(f1*g).x = f1.(g.x) by A5,A6,FUNCT_1:12;
hence (f1*g).x = (f2*g).x by A3,A7,A8;
end;
hence thesis by A5,A4;
end;
:: missing, 2011.06.06, A.T.
theorem
for f being Y-valued Function st x in dom(f|X)
holds (f|X)/.x = f/.x
proof let f be Y-valued Function;
assume
A1: x in dom(f|X);
then
A2: x in dom f by RELAT_1:57;
thus (f|X)/.x = (f|X).x by A1,Def6
.= f.x by A1,FUNCT_1:47
.= f/.x by A2,Def6;
end;
scheme
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));
consider f being Function such that
A1: dom f = A() and
A2: for x being object st x in A() holds (C[x] implies f.x = F(x)) &
(not C[x] implies f.x = G(x)) from LambdaC;
take f;
thus thesis by A1,A2;
end;
theorem
for f,g being Function st f.x = g.x holds f | {x} tolerates g | {x}
proof
let f,g be Function such that
A1: f.x = g.x;
let a be object;
set F = f|{x}, G = g|{x};
assume a in dom F /\ dom G;
then a in dom F by XBOOLE_0:def 4;
then
A2: a in {x} by RELAT_1:57;
then a = x by TARSKI:def 1;
hence G.a = f.a by A1,A2,FUNCT_1:49
.= F.a by A2,FUNCT_1:49;
end;
theorem
for f,g being Function st f.x = g.x & f.y = g.y
holds f | {x,y} tolerates g | {x,y}
proof
let f,g be Function such that
A1: f.x = g.x & f.y = g.y;
let a be object;
set F = f|{x,y}, G = g|{x,y};
assume a in dom F /\ dom G;
then a in dom F by XBOOLE_0:def 4;
then
A2: a in {x,y} by RELAT_1:57;
then a = x or a = y by TARSKI:def 2;
hence G.a = f.a by A1,A2,FUNCT_1:49
.= F.a by A2,FUNCT_1:49;
end;
definition
let A,B be set;
let F be PFuncs(A,B)-valued Function;
let i be object;
redefine func F.i -> PartFunc of A,B; :: redefines . (FUNCT_1, definition)
coherence
proof
per cases;
suppose i in dom F;
then
A1: F.i in rng F by FUNCT_1:def 3;
rng F c= PFuncs(A,B) by RELAT_1:def 19;
hence thesis by A1,Th46;
end;
suppose not i in dom F;
then F.i = {} by FUNCT_1:def 2;
hence thesis by RELSET_1:12;
end;
end;
end;