:: PARTFUN1 semantic presentation
begin
theorem Th1: :: PARTFUN1:1
for f, g being Function st ( for x being set st x in (dom f) /\ (dom g) holds
f . x = g . x ) holds
ex h being Function st f \/ g = h
proof
let f, g be Function; ::_thesis: ( ( for x being set st x in (dom f) /\ (dom g) holds
f . x = g . x ) implies ex h being Function st f \/ g = h )
assume A1: for x being set st x in (dom f) /\ (dom g) holds
f . x = g . x ; ::_thesis: ex h being Function st f \/ g = h
defpred S1[ set , set ] means [$1,$2] in f \/ g;
A2: for x, y1, y2 being set st S1[x,y1] & S1[x,y2] holds
y1 = y2
proof
let x, y1, y2 be set ; ::_thesis: ( S1[x,y1] & S1[x,y2] implies y1 = y2 )
assume that
A3: [x,y1] in f \/ g and
A4: [x,y2] in f \/ g ; ::_thesis: y1 = y2
now__::_thesis:_y1_=_y2
( [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;
percases ( ( x in dom f & x in dom g ) or ( x in dom f & not x in dom g ) or ( not x in dom f & x in dom g ) ) by A6, XTUPLE_0:def_12;
suppose ( x in dom f & x in dom g ) ; ::_thesis: y1 = y2
then x in (dom f) /\ (dom g) by XBOOLE_0:def_4;
hence y1 = y2 by A1, A5, A7; ::_thesis: verum
end;
suppose ( x in dom f & not x in dom g ) ; ::_thesis: y1 = y2
hence y1 = y2 by A6, A5, FUNCT_1:1; ::_thesis: verum
end;
suppose ( not x in dom f & x in dom g ) ; ::_thesis: y1 = y2
hence y1 = y2 by A6, A5, FUNCT_1:1; ::_thesis: verum
end;
end;
end;
hence y1 = y2 ; ::_thesis: verum
end;
consider h being Function such that
A8: for x, y being set holds
( [x,y] in h iff ( x in (dom f) \/ (dom g) & S1[x,y] ) ) from FUNCT_1:sch_1(A2);
take h ; ::_thesis: f \/ g = h
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b1 being set holds
( ( not [x,b1] in f \/ g or [x,b1] in h ) & ( not [x,b1] in h or [x,b1] in f \/ g ) )
let y be set ; ::_thesis: ( ( not [x,y] in f \/ g or [x,y] in h ) & ( not [x,y] in h or [x,y] in f \/ g ) )
thus ( [x,y] in f \/ g implies [x,y] in h ) ::_thesis: ( not [x,y] in h or [x,y] in f \/ g )
proof
assume A9: [x,y] in f \/ g ; ::_thesis: [x,y] in h
then ( [x,y] in f or [x,y] in g ) by 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 [x,y] in h by A8, A9; ::_thesis: verum
end;
thus ( not [x,y] in h or [x,y] in f \/ g ) by A8; ::_thesis: verum
end;
theorem Th2: :: PARTFUN1:2
for f, g, h being Function st f \/ g = h holds
for x being set st x in (dom f) /\ (dom g) holds
f . x = g . x
proof
let f, g, h be Function; ::_thesis: ( f \/ g = h implies for x being set st x in (dom f) /\ (dom g) holds
f . x = g . x )
assume A1: f \/ g = h ; ::_thesis: for x being set st x in (dom f) /\ (dom g) holds
f . x = g . x
let x be set ; ::_thesis: ( x in (dom f) /\ (dom g) implies f . x = g . x )
assume A2: x in (dom f) /\ (dom g) ; ::_thesis: f . x = g . x
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 f . x = g . x by A1, A3, GRFUNC_1:15; ::_thesis: verum
end;
scheme :: PARTFUN1:sch 1
LambdaC{ F1() -> set , P1[ set ], F2( set ) -> set , F3( set ) -> set } :
ex f being Function st
( dom f = F1() & ( for x being set st x in F1() holds
( ( P1[x] implies f . x = F2(x) ) & ( P1[x] implies f . x = F3(x) ) ) ) )
proof
defpred S1[ set , set ] means ( ( P1[$1] implies $2 = F2($1) ) & ( P1[$1] implies $2 = F3($1) ) );
A1: for x being set st x in F1() holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in F1() implies ex y being set st S1[x,y] )
( P1[x] implies ( ( P1[x] implies F3(x) = F2(x) ) & ( P1[x] implies F3(x) = F3(x) ) ) ) ;
hence ( x in F1() implies ex y being set st S1[x,y] ) ; ::_thesis: verum
end;
A2: for x, y1, y2 being set st x in F1() & S1[x,y1] & S1[x,y2] holds
y1 = y2 ;
thus ex f being Function st
( dom f = F1() & ( for x being set st x in F1() holds
S1[x,f . x] ) ) from FUNCT_1:sch_2(A2, A1); ::_thesis: verum
end;
Lm1: now__::_thesis:_for_X,_Y_being_set_ex_E_being_set_st_
(_dom_E_c=_X_&_rng_E_c=_Y_)
let X, Y be set ; ::_thesis: ex E being set st
( dom E c= X & rng E c= Y )
take E = {} ; ::_thesis: ( dom E c= X & rng E c= Y )
thus ( dom E c= X & rng E c= Y ) by XBOOLE_1:2; ::_thesis: verum
end;
registration
let X, Y be set ;
cluster Relation-like X -defined Y -valued Function-like for Element of bool [:X,Y:];
existence
ex b1 being Relation of X,Y st b1 is Function-like
proof
consider E being Function such that
A1: ( dom E c= X & rng E c= Y ) by Lm1;
reconsider E = E as Relation of X,Y by A1, RELSET_1:4;
take E ; ::_thesis: E is Function-like
thus E is Function-like ; ::_thesis: verum
end;
end;
definition
let X, Y be set ;
mode PartFunc of X,Y is Function-like Relation of X,Y;
end;
theorem :: PARTFUN1:3
for X, Y, y being set
for f being PartFunc of X,Y st y in rng f holds
ex x being Element of X st
( x in dom f & y = f . x )
proof
let X, Y, y be set ; ::_thesis: for f being PartFunc of X,Y st y in rng f holds
ex x being Element of X st
( x in dom f & y = f . x )
let f be PartFunc of X,Y; ::_thesis: ( y in rng f implies ex x being Element of X st
( x in dom f & y = f . x ) )
assume y in rng f ; ::_thesis: ex x being Element of X st
( x in dom f & y = f . x )
then ex x being set st
( x in dom f & y = f . x ) by FUNCT_1:def_3;
hence ex x being Element of X st
( x in dom f & y = f . x ) ; ::_thesis: verum
end;
theorem Th4: :: PARTFUN1:4
for Y, x being set
for f being b1 -valued Function st x in dom f holds
f . x in Y
proof
let Y, x be set ; ::_thesis: for f being Y -valued Function st x in dom f holds
f . x in Y
let f be Y -valued Function; ::_thesis: ( x in dom f implies f . x in Y )
assume x in dom f ; ::_thesis: f . x in Y
then A1: f . x in rng f by FUNCT_1:def_3;
rng f c= Y by RELAT_1:def_19;
hence f . x in Y by A1; ::_thesis: verum
end;
theorem :: PARTFUN1:5
for X, Y being set
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
proof
let X, Y be set ; ::_thesis: 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
let f1, f2 be PartFunc of X,Y; ::_thesis: ( dom f1 = dom f2 & ( for x being Element of X st x in dom f1 holds
f1 . x = f2 . x ) implies f1 = f2 )
assume that
A1: dom f1 = dom f2 and
A2: for x being Element of X st x in dom f1 holds
f1 . x = f2 . x ; ::_thesis: f1 = f2
for x being set st x in dom f1 holds
f1 . x = f2 . x by A2;
hence f1 = f2 by A1, FUNCT_1:2; ::_thesis: verum
end;
scheme :: PARTFUN1:sch 2
PartFuncEx{ F1() -> set , F2() -> set , P1[ set , set ] } :
ex f being PartFunc of F1(),F2() st
( ( for x being set holds
( x in dom f iff ( x in F1() & ex y being set st P1[x,y] ) ) ) & ( for x being set st x in dom f holds
P1[x,f . x] ) )
provided
A1: for x, y being set st x in F1() & P1[x,y] holds
y in F2() and
A2: for x, y1, y2 being set st x in F1() & P1[x,y1] & P1[x,y2] holds
y1 = y2
proof
A3: now__::_thesis:_(_F2()_<>_{}_implies_ex_f_being_PartFunc_of_F1(),F2()_st_
(_(_for_x_being_set_holds_
(_x_in_dom_f_iff_(_x_in_F1()_&_ex_y_being_set_st_P1[x,y]_)_)_)_&_(_for_x_being_set_st_x_in_dom_f_holds_
P1[x,f_._x]_)_)_)
defpred S1[ set ] means ex y being set st P1[$1,y];
set y1 = the set ;
assume F2() <> {} ; ::_thesis: ex f being PartFunc of F1(),F2() st
( ( for x being set holds
( x in dom f iff ( x in F1() & ex y being set st P1[x,y] ) ) ) & ( for x being set st x in dom f holds
P1[x,f . x] ) )
defpred S2[ set , set ] means ( ( ex y being set st P1[$1,y] implies P1[$1,$2] ) & ( ( for y being set holds P1[$1,y] ) implies $2 = the set ) );
A4: for x being set st x in F1() holds
ex z being set st S2[x,z]
proof
let x be set ; ::_thesis: ( x in F1() implies ex z being set st S2[x,z] )
assume x in F1() ; ::_thesis: ex z being set st S2[x,z]
( ( for y being set holds P1[x,y] ) implies ( ( ex y being set st P1[x,y] implies P1[x, the set ] ) & ( ( for y being set holds P1[x,y] ) implies the set = the set ) ) ) ;
hence ex z being set st S2[x,z] ; ::_thesis: verum
end;
A5: for x, z1, z2 being set st x in F1() & S2[x,z1] & S2[x,z2] holds
z1 = z2 by A2;
consider g being Function such that
A6: dom g = F1() and
A7: for x being set st x in F1() holds
S2[x,g . x] from FUNCT_1:sch_2(A5, A4);
consider X being set such that
A8: for x being set holds
( x in X iff ( x in F1() & S1[x] ) ) from XBOOLE_0:sch_1();
set f = g | X;
A9: dom (g | X) c= F1() by A6, RELAT_1:60;
rng (g | X) c= F2()
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (g | X) or y in F2() )
assume y in rng (g | X) ; ::_thesis: y in F2()
then consider x being set such that
A10: x in dom (g | X) and
A11: y = (g | X) . x by FUNCT_1:def_3;
A12: dom (g | X) c= X by RELAT_1:58;
then ( x in F1() & ex y being set st P1[x,y] ) by A8, A10;
then P1[x,g . x] by A7;
then A13: P1[x,y] by A10, A11, FUNCT_1:47;
x in F1() by A8, A10, A12;
hence y in F2() by A1, A13; ::_thesis: verum
end;
then reconsider f = g | X as PartFunc of F1(),F2() by A9, RELSET_1:4;
take f = f; ::_thesis: ( ( for x being set holds
( x in dom f iff ( x in F1() & ex y being set st P1[x,y] ) ) ) & ( for x being set st x in dom f holds
P1[x,f . x] ) )
thus for x being set holds
( x in dom f iff ( x in F1() & ex y being set st P1[x,y] ) ) ::_thesis: for x being set st x in dom f holds
P1[x,f . x]
proof
let x be set ; ::_thesis: ( x in dom f iff ( x in F1() & ex y being set st P1[x,y] ) )
dom f c= X by RELAT_1:58;
hence ( x in dom f implies ( x in F1() & ex y being set st P1[x,y] ) ) by A8; ::_thesis: ( x in F1() & ex y being set st P1[x,y] implies x in dom f )
assume that
A14: x in F1() and
A15: ex y being set st P1[x,y] ; ::_thesis: x in dom f
x in X by A8, A14, A15;
then x in (dom g) /\ X by A6, A14, XBOOLE_0:def_4;
hence x in dom f by RELAT_1:61; ::_thesis: verum
end;
let x be set ; ::_thesis: ( x in dom f implies P1[x,f . x] )
assume A16: x in dom f ; ::_thesis: P1[x,f . x]
dom f c= X by RELAT_1:58;
then ex y being set st P1[x,y] by A8, A16;
then P1[x,g . x] by A7, A16;
hence P1[x,f . x] by A16, FUNCT_1:47; ::_thesis: verum
end;
now__::_thesis:_(_F2()_=_{}_implies_ex_f_being_PartFunc_of_F1(),F2()_st_
(_(_for_x_being_set_holds_
(_x_in_dom_f_iff_(_x_in_F1()_&_ex_y_being_set_st_P1[x,y]_)_)_)_&_(_for_x_being_set_st_x_in_dom_f_holds_
P1[x,f_._x]_)_)_)
consider f being Function such that
A17: ( dom f c= F1() & rng f c= F2() ) by Lm1;
reconsider f = f as PartFunc of F1(),F2() by A17, RELSET_1:4;
assume A18: F2() = {} ; ::_thesis: ex f being PartFunc of F1(),F2() st
( ( for x being set holds
( x in dom f iff ( x in F1() & ex y being set st P1[x,y] ) ) ) & ( for x being set st x in dom f holds
P1[x,f . x] ) )
take f = f; ::_thesis: ( ( for x being set holds
( x in dom f iff ( x in F1() & ex y being set st P1[x,y] ) ) ) & ( for x being set st x in dom f holds
P1[x,f . x] ) )
thus for x being set holds
( x in dom f iff ( x in F1() & ex y being set st P1[x,y] ) ) by A1, A18; ::_thesis: for x being set st x in dom f holds
P1[x,f . x]
thus for x being set st x in dom f holds
P1[x,f . x] by A18; ::_thesis: verum
end;
hence ex f being PartFunc of F1(),F2() st
( ( for x being set holds
( x in dom f iff ( x in F1() & ex y being set st P1[x,y] ) ) ) & ( for x being set st x in dom f holds
P1[x,f . x] ) ) by A3; ::_thesis: verum
end;
scheme :: PARTFUN1:sch 3
LambdaR{ F1() -> set , F2() -> set , F3( set ) -> set , P1[ set ] } :
ex f being PartFunc of F1(),F2() st
( ( for x being set holds
( x in dom f iff ( x in F1() & P1[x] ) ) ) & ( for x being set st x in dom f holds
f . x = F3(x) ) )
provided
A1: for x being set st P1[x] holds
F3(x) in F2()
proof
defpred S1[ set , set ] means ( P1[$1] & $2 = F3($1) );
A2: for x, y1, y2 being set st x in F1() & S1[x,y1] & S1[x,y2] holds
y1 = y2 ;
A3: for x, y being set st x in F1() & S1[x,y] holds
y in F2() by A1;
consider f being PartFunc of F1(),F2() such that
A4: for x being set holds
( x in dom f iff ( x in F1() & ex y being set st S1[x,y] ) ) and
A5: for x being set st x in dom f holds
S1[x,f . x] from PARTFUN1:sch_2(A3, A2);
take f ; ::_thesis: ( ( for x being set holds
( x in dom f iff ( x in F1() & P1[x] ) ) ) & ( for x being set st x in dom f holds
f . x = F3(x) ) )
thus for x being set holds
( x in dom f iff ( x in F1() & P1[x] ) ) ::_thesis: for x being set st x in dom f holds
f . x = F3(x)
proof
let x be set ; ::_thesis: ( x in dom f iff ( x in F1() & P1[x] ) )
thus ( x in dom f implies ( x in F1() & P1[x] ) ) ::_thesis: ( x in F1() & P1[x] implies x in dom f )
proof
assume A6: x in dom f ; ::_thesis: ( x in F1() & P1[x] )
then ex y being set st
( P1[x] & y = F3(x) ) by A4;
hence ( x in F1() & P1[x] ) by A6; ::_thesis: verum
end;
assume that
A7: x in F1() and
A8: P1[x] ; ::_thesis: x in dom f
ex y being set st
( P1[x] & y = F3(x) ) by A8;
hence x in dom f by A4, A7; ::_thesis: verum
end;
thus for x being set st x in dom f holds
f . x = F3(x) by A5; ::_thesis: verum
end;
definition
let X, Y, V, Z be set ;
let f be PartFunc of X,Y;
let g be PartFunc of V,Z;
:: original: *
redefine funcg * f -> PartFunc of X,Z;
coherence
f * g is PartFunc of X,Z
proof
A1: dom (g * f) c= X ;
rng (g * f) c= Z by RELAT_1:def_19;
hence f * g is PartFunc of X,Z by A1, RELSET_1:4; ::_thesis: verum
end;
end;
theorem :: PARTFUN1:6
for X, Y being set
for f being Relation of X,Y holds (id X) * f = f
proof
let X, Y be set ; ::_thesis: for f being Relation of X,Y holds (id X) * f = f
let f be Relation of X,Y; ::_thesis: (id X) * f = f
dom f c= X ;
hence (id X) * f = f by RELAT_1:51; ::_thesis: verum
end;
theorem :: PARTFUN1:7
for X, Y being set
for f being Relation of X,Y holds f * (id Y) = f
proof
let X, Y be set ; ::_thesis: for f being Relation of X,Y holds f * (id Y) = f
let f be Relation of X,Y; ::_thesis: f * (id Y) = f
rng f c= Y ;
hence f * (id Y) = f by RELAT_1:53; ::_thesis: verum
end;
theorem :: PARTFUN1:8
for X, Y being set
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
proof
let X, Y be set ; ::_thesis: 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
let f be PartFunc of X,Y; ::_thesis: ( ( for x1, x2 being Element of X st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2 ) implies f is one-to-one )
assume for x1, x2 being Element of X st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2 ; ::_thesis: f is one-to-one
then for x1, x2 being set st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2 ;
hence f is one-to-one by FUNCT_1:def_4; ::_thesis: verum
end;
theorem :: PARTFUN1:9
for X, Y being set
for f being PartFunc of X,Y st f is one-to-one holds
f " is PartFunc of Y,X
proof
let X, Y be set ; ::_thesis: for f being PartFunc of X,Y st f is one-to-one holds
f " is PartFunc of Y,X
let f be PartFunc of X,Y; ::_thesis: ( f is one-to-one implies f " is PartFunc of Y,X )
assume A1: f is one-to-one ; ::_thesis: f " is PartFunc of Y,X
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 f " is PartFunc of Y,X by A2, RELSET_1:4; ::_thesis: verum
end;
theorem :: PARTFUN1:10
for X, Y, Z being set
for f being PartFunc of X,Y holds f | Z is PartFunc of Z,Y
proof
let X, Y, Z be set ; ::_thesis: for f being PartFunc of X,Y holds f | Z is PartFunc of Z,Y
let f be PartFunc of X,Y; ::_thesis: f | Z is PartFunc of Z,Y
( dom (f | Z) c= Z & rng (f | Z) c= Y ) by RELAT_1:58, RELAT_1:def_19;
hence f | Z is PartFunc of Z,Y by RELSET_1:4; ::_thesis: verum
end;
theorem Th11: :: PARTFUN1:11
for X, Y, Z being set
for f being PartFunc of X,Y holds f | Z is PartFunc of X,Y ;
definition
let X, Y be set ;
let f be PartFunc of X,Y;
let Z be set ;
:: original: |
redefine funcf | Z -> PartFunc of X,Y;
coherence
f | Z is PartFunc of X,Y by Th11;
end;
theorem :: PARTFUN1:12
for X, Y, Z being set
for f being PartFunc of X,Y holds Z |` f is PartFunc of X,Z
proof
let X, Y, Z be set ; ::_thesis: for f being PartFunc of X,Y holds Z |` f is PartFunc of X,Z
let f be PartFunc of X,Y; ::_thesis: Z |` f is PartFunc of X,Z
( dom (Z |` f) c= X & rng (Z |` f) c= Z ) by RELAT_1:85;
hence Z |` f is PartFunc of X,Z by RELSET_1:4; ::_thesis: verum
end;
theorem :: PARTFUN1:13
for X, Y, Z being set
for f being PartFunc of X,Y holds Z |` f is PartFunc of X,Y ;
theorem Th14: :: PARTFUN1:14
for Y, X being set
for f being Function holds (Y |` f) | X is PartFunc of X,Y
proof
let Y, X be set ; ::_thesis: for f being Function holds (Y |` f) | X is PartFunc of X,Y
let f be Function; ::_thesis: (Y |` f) | X is PartFunc of X,Y
(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, RELAT_1:85;
hence (Y |` f) | X is PartFunc of X,Y by RELSET_1:4; ::_thesis: verum
end;
theorem :: PARTFUN1:15
for X, Y, y being set
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 )
proof
let X, Y, y be set ; ::_thesis: 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 )
let f be PartFunc of X,Y; ::_thesis: ( y in f .: X implies ex x being Element of X st
( x in dom f & y = f . x ) )
assume y in f .: X ; ::_thesis: ex x being Element of X st
( x in dom f & y = f . x )
then ex x being set st
( x in dom f & x in X & y = f . x ) by FUNCT_1:def_6;
hence ex x being Element of X st
( x in dom f & y = f . x ) ; ::_thesis: verum
end;
theorem Th16: :: PARTFUN1:16
for x, Y being set
for f being PartFunc of {x},Y holds rng f c= {(f . x)}
proof
let x, Y be set ; ::_thesis: for f being PartFunc of {x},Y holds rng f c= {(f . x)}
let f be PartFunc of {x},Y; ::_thesis: rng f c= {(f . x)}
( dom f = {} or dom f = {x} ) by ZFMISC_1:33;
then ( rng f = {} or rng f = {(f . x)} ) by FUNCT_1:4, RELAT_1:42;
hence rng f c= {(f . x)} by ZFMISC_1:33; ::_thesis: verum
end;
theorem :: PARTFUN1:17
for x, Y being set
for f being PartFunc of {x},Y holds f is one-to-one
proof
let x, Y be set ; ::_thesis: for f being PartFunc of {x},Y holds f is one-to-one
let f be PartFunc of {x},Y; ::_thesis: f is one-to-one
let x1 be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x1 in dom f or not b1 in dom f or not f . x1 = f . b1 or x1 = b1 )
let x2 be set ; ::_thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume that
A1: x1 in dom f and
A2: x2 in dom f ; ::_thesis: ( not f . x1 = f . x2 or x1 = x2 )
( dom f <> {} implies ( x1 = x & x2 = x ) ) by A1, A2, TARSKI:def_1;
hence ( not f . x1 = f . x2 or x1 = x2 ) by A1; ::_thesis: verum
end;
theorem :: PARTFUN1:18
for x, Y, P being set
for f being PartFunc of {x},Y holds f .: P c= {(f . x)}
proof
let x, Y, P be set ; ::_thesis: for f being PartFunc of {x},Y holds f .: P c= {(f . x)}
let f be PartFunc of {x},Y; ::_thesis: f .: P c= {(f . x)}
( f .: P c= rng f & rng f c= {(f . x)} ) by Th16, RELAT_1:111;
hence f .: P c= {(f . x)} by XBOOLE_1:1; ::_thesis: verum
end;
theorem :: PARTFUN1:19
for x, X, Y being set
for f being Function st dom f = {x} & x in X & f . x in Y holds
f is PartFunc of X,Y
proof
let x, X, Y be set ; ::_thesis: for f being Function st dom f = {x} & x in X & f . x in Y holds
f is PartFunc of X,Y
let f be Function; ::_thesis: ( dom f = {x} & x in X & f . x in Y implies f is PartFunc of X,Y )
assume that
A1: dom f = {x} and
A2: x in X and
A3: f . x in Y ; ::_thesis: f is PartFunc of X,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 f is PartFunc of X,Y by A4, RELSET_1:4; ::_thesis: verum
end;
theorem Th20: :: PARTFUN1:20
for X, y, x being set
for f being PartFunc of X,{y} st x in dom f holds
f . x = y
proof
let X, y, x be set ; ::_thesis: for f being PartFunc of X,{y} st x in dom f holds
f . x = y
let f be PartFunc of X,{y}; ::_thesis: ( x in dom f implies f . x = y )
( x in dom f implies f . x in {y} ) by Th4;
hence ( x in dom f implies f . x = y ) by TARSKI:def_1; ::_thesis: verum
end;
theorem :: PARTFUN1:21
for X, y being set
for f1, f2 being PartFunc of X,{y} st dom f1 = dom f2 holds
f1 = f2
proof
let X, y be set ; ::_thesis: for f1, f2 being PartFunc of X,{y} st dom f1 = dom f2 holds
f1 = f2
let f1, f2 be PartFunc of X,{y}; ::_thesis: ( dom f1 = dom f2 implies f1 = f2 )
assume A1: dom f1 = dom f2 ; ::_thesis: f1 = f2
for x being set st x in dom f1 holds
f1 . x = f2 . x
proof
let x be set ; ::_thesis: ( x in dom f1 implies f1 . x = f2 . x )
assume A2: x in dom f1 ; ::_thesis: f1 . x = f2 . x
then f1 . x = y by Th20;
hence f1 . x = f2 . x by A1, A2, Th20; ::_thesis: verum
end;
hence f1 = f2 by A1, FUNCT_1:2; ::_thesis: verum
end;
definition
let f be Function;
let X, Y be set ;
func<:f,X,Y:> -> PartFunc of X,Y equals :: PARTFUN1:def 1
(Y |` f) | X;
coherence
(Y |` f) | X is PartFunc of X,Y by Th14;
end;
:: deftheorem defines <: PARTFUN1:def_1_:_
for f being Function
for X, Y being set holds <:f,X,Y:> = (Y |` f) | X;
theorem Th22: :: PARTFUN1:22
for X, Y being set
for f being Function holds <:f,X,Y:> c= f
proof
let X, Y be set ; ::_thesis: for f being Function holds <:f,X,Y:> c= f
let f be Function; ::_thesis: <:f,X,Y:> c= f
( (Y |` f) | X c= Y |` f & Y |` f c= f ) by RELAT_1:59, RELAT_1:86;
hence <:f,X,Y:> c= f by XBOOLE_1:1; ::_thesis: verum
end;
theorem Th23: :: PARTFUN1:23
for X, Y being set
for f being Function holds
( dom <:f,X,Y:> c= dom f & rng <:f,X,Y:> c= rng f )
proof
let X, Y be set ; ::_thesis: for f being Function holds
( dom <:f,X,Y:> c= dom f & rng <:f,X,Y:> c= rng f )
let f be Function; ::_thesis: ( dom <:f,X,Y:> c= dom f & rng <:f,X,Y:> c= rng f )
<:f,X,Y:> c= f by Th22;
hence ( dom <:f,X,Y:> c= dom f & rng <:f,X,Y:> c= rng f ) by RELAT_1:11; ::_thesis: verum
end;
theorem Th24: :: PARTFUN1:24
for x, X, Y being set
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 x, X, Y be set ; ::_thesis: for f being Function holds
( x in dom <:f,X,Y:> iff ( x in dom f & x in X & f . x in Y ) )
let f be Function; ::_thesis: ( x in dom <:f,X,Y:> iff ( x in dom f & x in X & f . x in Y ) )
thus ( x in dom <:f,X,Y:> implies ( x in dom f & x in X & f . x in Y ) ) ::_thesis: ( x in dom f & x in X & f . x in Y implies x in dom <:f,X,Y:> )
proof
assume A1: x in dom <:f,X,Y:> ; ::_thesis: ( x in dom f & x in X & f . x in Y )
then x in (dom (Y |` f)) /\ X by RELAT_1:61;
then x in dom (Y |` f) by XBOOLE_0:def_4;
hence ( x in dom f & x in X & f . x in Y ) by A1, FUNCT_1:54; ::_thesis: verum
end;
assume that
A2: x in dom f and
A3: x in X and
A4: f . x in Y ; ::_thesis: x in dom <:f,X,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 x in dom <:f,X,Y:> by RELAT_1:61; ::_thesis: verum
end;
theorem Th25: :: PARTFUN1:25
for x, X, Y being set
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 x, X, Y be set ; ::_thesis: for f being Function st x in dom f & x in X & f . x in Y holds
<:f,X,Y:> . x = f . x
let f be Function; ::_thesis: ( x in dom f & x in X & f . x in Y implies <:f,X,Y:> . x = f . x )
assume that
A1: x in dom f and
A2: x in X and
A3: f . x in Y ; ::_thesis: <:f,X,Y:> . x = f . x
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 <:f,X,Y:> . x = f . x ; ::_thesis: verum
end;
theorem Th26: :: PARTFUN1:26
for x, X, Y being set
for f being Function st x in dom <:f,X,Y:> holds
<:f,X,Y:> . x = f . x
proof
let x, X, Y be set ; ::_thesis: for f being Function st x in dom <:f,X,Y:> holds
<:f,X,Y:> . x = f . x
let f be Function; ::_thesis: ( x in dom <:f,X,Y:> implies <:f,X,Y:> . x = f . x )
assume A1: x in dom <:f,X,Y:> ; ::_thesis: <:f,X,Y:> . x = f . x
then ( x in dom f & f . x in Y ) by Th24;
hence <:f,X,Y:> . x = f . x by A1, Th25; ::_thesis: verum
end;
theorem :: PARTFUN1:27
for X, Y being set
for f, g being Function st f c= g holds
<:f,X,Y:> c= <:g,X,Y:>
proof
let X, Y be set ; ::_thesis: for f, g being Function st f c= g holds
<:f,X,Y:> c= <:g,X,Y:>
let f, g be Function; ::_thesis: ( f c= g implies <:f,X,Y:> c= <:g,X,Y:> )
assume A1: f c= g ; ::_thesis: <:f,X,Y:> c= <:g,X,Y:>
A2: dom <:f,X,Y:> c= dom f by Th23;
now__::_thesis:_(_dom_<:f,X,Y:>_c=_dom_<:g,X,Y:>_&_(_for_x_being_set_st_x_in_dom_<:f,X,Y:>_holds_
<:f,X,Y:>_._x_=_<:g,X,Y:>_._x_)_)
thus A3: dom <:f,X,Y:> c= dom <:g,X,Y:> ::_thesis: for x being set st x in dom <:f,X,Y:> holds
<:f,X,Y:> . x = <:g,X,Y:> . x
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom <:f,X,Y:> or x in dom <:g,X,Y:> )
A4: dom f c= dom g by A1, RELAT_1:11;
assume A5: x in dom <:f,X,Y:> ; ::_thesis: x in dom <:g,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 x in dom <:g,X,Y:> by A5, A4, A6, Th24; ::_thesis: verum
end;
let x be set ; ::_thesis: ( x in dom <:f,X,Y:> implies <:f,X,Y:> . x = <:g,X,Y:> . x )
assume A7: x in dom <:f,X,Y:> ; ::_thesis: <:f,X,Y:> . x = <:g,X,Y:> . x
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; ::_thesis: verum
end;
hence <:f,X,Y:> c= <:g,X,Y:> by GRFUNC_1:2; ::_thesis: verum
end;
theorem Th28: :: PARTFUN1:28
for Z, X, Y being set
for f being Function st Z c= X holds
<:f,Z,Y:> c= <:f,X,Y:>
proof
let Z, X, Y be set ; ::_thesis: for f being Function st Z c= X holds
<:f,Z,Y:> c= <:f,X,Y:>
let f be Function; ::_thesis: ( Z c= X implies <:f,Z,Y:> c= <:f,X,Y:> )
assume A1: Z c= X ; ::_thesis: <:f,Z,Y:> c= <:f,X,Y:>
A2: dom <:f,Z,Y:> c= dom <:f,X,Y:>
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom <:f,Z,Y:> or x in dom <:f,X,Y:> )
assume A3: x in dom <:f,Z,Y:> ; ::_thesis: x in dom <:f,X,Y:>
then A4: f . x in Y by Th24;
( x in Z & x in dom f ) by A3, Th24;
hence x in dom <:f,X,Y:> by A1, A4, Th24; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_dom_<:f,Z,Y:>_holds_
<:f,Z,Y:>_._x_=_<:f,X,Y:>_._x
let x be set ; ::_thesis: ( x in dom <:f,Z,Y:> implies <:f,Z,Y:> . x = <:f,X,Y:> . x )
assume A5: x in dom <:f,Z,Y:> ; ::_thesis: <:f,Z,Y:> . x = <:f,X,Y:> . x
then <:f,Z,Y:> . x = f . x by Th26;
hence <:f,Z,Y:> . x = <:f,X,Y:> . x by A2, A5, Th26; ::_thesis: verum
end;
hence <:f,Z,Y:> c= <:f,X,Y:> by A2, GRFUNC_1:2; ::_thesis: verum
end;
theorem Th29: :: PARTFUN1:29
for Z, Y, X being set
for f being Function st Z c= Y holds
<:f,X,Z:> c= <:f,X,Y:>
proof
let Z, Y, X be set ; ::_thesis: for f being Function st Z c= Y holds
<:f,X,Z:> c= <:f,X,Y:>
let f be Function; ::_thesis: ( Z c= Y implies <:f,X,Z:> c= <:f,X,Y:> )
assume A1: Z c= Y ; ::_thesis: <:f,X,Z:> c= <:f,X,Y:>
A2: dom <:f,X,Z:> c= dom <:f,X,Y:>
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom <:f,X,Z:> or x in dom <:f,X,Y:> )
assume A3: x in dom <:f,X,Z:> ; ::_thesis: x in dom <:f,X,Y:>
then ( f . x in Z & x in dom f ) by Th24;
hence x in dom <:f,X,Y:> by A1, A3, Th24; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_dom_<:f,X,Z:>_holds_
<:f,X,Z:>_._x_=_<:f,X,Y:>_._x
let x be set ; ::_thesis: ( x in dom <:f,X,Z:> implies <:f,X,Z:> . x = <:f,X,Y:> . x )
assume A4: x in dom <:f,X,Z:> ; ::_thesis: <:f,X,Z:> . x = <:f,X,Y:> . x
then <:f,X,Z:> . x = f . x by Th26;
hence <:f,X,Z:> . x = <:f,X,Y:> . x by A2, A4, Th26; ::_thesis: verum
end;
hence <:f,X,Z:> c= <:f,X,Y:> by A2, GRFUNC_1:2; ::_thesis: verum
end;
theorem :: PARTFUN1:30
for X1, X2, Y1, Y2 being set
for f being Function st X1 c= X2 & Y1 c= Y2 holds
<:f,X1,Y1:> c= <:f,X2,Y2:>
proof
let X1, X2, Y1, Y2 be set ; ::_thesis: for f being Function st X1 c= X2 & Y1 c= Y2 holds
<:f,X1,Y1:> c= <:f,X2,Y2:>
let f be Function; ::_thesis: ( X1 c= X2 & Y1 c= Y2 implies <:f,X1,Y1:> c= <:f,X2,Y2:> )
assume ( X1 c= X2 & Y1 c= Y2 ) ; ::_thesis: <:f,X1,Y1:> c= <:f,X2,Y2:>
then ( <:f,X1,Y1:> c= <:f,X2,Y1:> & <:f,X2,Y1:> c= <:f,X2,Y2:> ) by Th28, Th29;
hence <:f,X1,Y1:> c= <:f,X2,Y2:> by XBOOLE_1:1; ::_thesis: verum
end;
theorem Th31: :: PARTFUN1:31
for X, Y being set
for f being Function st dom f c= X & rng f c= Y holds
f = <:f,X,Y:>
proof
let X, Y be set ; ::_thesis: for f being Function st dom f c= X & rng f c= Y holds
f = <:f,X,Y:>
let f be Function; ::_thesis: ( dom f c= X & rng f c= Y implies f = <:f,X,Y:> )
assume A1: ( dom f c= X & rng f c= Y ) ; ::_thesis: f = <:f,X,Y:>
A2: dom f c= dom <:f,X,Y:>
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom f or x in dom <:f,X,Y:> )
assume A3: x in dom f ; ::_thesis: x in dom <:f,X,Y:>
then f . x in rng f by FUNCT_1:def_3;
hence x in dom <:f,X,Y:> by A1, A3, Th24; ::_thesis: verum
end;
dom <:f,X,Y:> c= dom f by Th23;
then A4: dom f = dom <:f,X,Y:> by A2, XBOOLE_0:def_10;
for x being set st x in dom f holds
f . x = <:f,X,Y:> . x by A2, Th26;
hence f = <:f,X,Y:> by A4, FUNCT_1:2; ::_thesis: verum
end;
theorem :: PARTFUN1:32
for f being Function holds f = <:f,(dom f),(rng f):> ;
theorem :: PARTFUN1:33
for X, Y being set
for f being PartFunc of X,Y holds <:f,X,Y:> = f
proof
let X, Y be set ; ::_thesis: for f being PartFunc of X,Y holds <:f,X,Y:> = f
let f be PartFunc of X,Y; ::_thesis: <:f,X,Y:> = f
thus <:f,X,Y:> = f ; ::_thesis: verum
end;
theorem Th34: :: PARTFUN1:34
for X, Y being set holds <:{},X,Y:> = {}
proof
let X, Y be set ; ::_thesis: <:{},X,Y:> = {}
( dom {} c= X & rng {} c= Y ) by XBOOLE_1:2;
hence <:{},X,Y:> = {} by Th31; ::_thesis: verum
end;
theorem Th35: :: PARTFUN1:35
for Y, Z, X being set
for f, g being Function holds <:g,Y,Z:> * <:f,X,Y:> c= <:(g * f),X,Z:>
proof
let Y, Z, X be set ; ::_thesis: for f, g being Function holds <:g,Y,Z:> * <:f,X,Y:> c= <:(g * f),X,Z:>
let f, g be Function; ::_thesis: <:g,Y,Z:> * <:f,X,Y:> c= <:(g * f),X,Z:>
A1: for x being set 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 set ; ::_thesis: ( x in dom (<:g,Y,Z:> * <:f,X,Y:>) implies (<:g,Y,Z:> * <:f,X,Y:>) . x = <:(g * f),X,Z:> . x )
assume A2: x in dom (<:g,Y,Z:> * <:f,X,Y:>) ; ::_thesis: (<:g,Y,Z:> * <:f,X,Y:>) . x = <:(g * f),X,Z:> . x
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 ; ::_thesis: verum
end;
dom (<:g,Y,Z:> * <:f,X,Y:>) c= dom <:(g * f),X,Z:>
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (<:g,Y,Z:> * <:f,X,Y:>) or x in dom <:(g * f),X,Z:> )
assume A8: x in dom (<:g,Y,Z:> * <:f,X,Y:>) ; ::_thesis: x in dom <:(g * f),X,Z:>
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 x in dom <:(g * f),X,Z:> by A8, A12, Th24; ::_thesis: verum
end;
hence <:g,Y,Z:> * <:f,X,Y:> c= <:(g * f),X,Z:> by A1, GRFUNC_1:2; ::_thesis: verum
end;
theorem :: PARTFUN1:36
for Y, Z, X being set
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 Y, Z, X be set ; ::_thesis: for f, g being Function st (rng f) /\ (dom g) c= Y holds
<:g,Y,Z:> * <:f,X,Y:> = <:(g * f),X,Z:>
let f, g be Function; ::_thesis: ( (rng f) /\ (dom g) c= Y implies <:g,Y,Z:> * <:f,X,Y:> = <:(g * f),X,Z:> )
assume A1: (rng f) /\ (dom g) c= Y ; ::_thesis: <:g,Y,Z:> * <:f,X,Y:> = <:(g * f),X,Z:>
A2: dom <:(g * f),X,Z:> c= dom (<:g,Y,Z:> * <:f,X,Y:>)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom <:(g * f),X,Z:> or x in dom (<:g,Y,Z:> * <:f,X,Y:>) )
assume A3: x in dom <:(g * f),X,Z:> ; ::_thesis: x in dom (<:g,Y,Z:> * <:f,X,Y:>)
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 x in dom (<:g,Y,Z:> * <:f,X,Y:>) by A8, FUNCT_1:11; ::_thesis: verum
end;
for x being set 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 set ; ::_thesis: ( x in dom <:(g * f),X,Z:> implies <:(g * f),X,Z:> . x = (<:g,Y,Z:> * <:f,X,Y:>) . x )
assume A9: x in dom <:(g * f),X,Z:> ; ::_thesis: <:(g * f),X,Z:> . x = (<:g,Y,Z:> * <:f,X,Y:>) . x
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 ; ::_thesis: verum
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 <:g,Y,Z:> * <:f,X,Y:> = <:(g * f),X,Z:> by A15, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th37: :: PARTFUN1:37
for X, Y being set
for f being Function st f is one-to-one holds
<:f,X,Y:> is one-to-one
proof
let X, Y be set ; ::_thesis: for f being Function st f is one-to-one holds
<:f,X,Y:> is one-to-one
let f be Function; ::_thesis: ( f is one-to-one implies <:f,X,Y:> is one-to-one )
assume f is one-to-one ; ::_thesis: <:f,X,Y:> is one-to-one
then Y |` f is one-to-one by FUNCT_1:58;
hence <:f,X,Y:> is one-to-one by FUNCT_1:52; ::_thesis: verum
end;
theorem :: PARTFUN1:38
for X, Y being set
for f being Function st f is one-to-one holds
<:f,X,Y:> " = <:(f "),Y,X:>
proof
let X, Y be set ; ::_thesis: for f being Function st f is one-to-one holds
<:f,X,Y:> " = <:(f "),Y,X:>
let f be Function; ::_thesis: ( f is one-to-one implies <:f,X,Y:> " = <:(f "),Y,X:> )
assume A1: f is one-to-one ; ::_thesis: <:f,X,Y:> " = <:(f "),Y,X:>
then A2: <:f,X,Y:> is one-to-one by Th37;
for y being set holds
( y in dom (<:f,X,Y:> ") iff y in dom <:(f "),Y,X:> )
proof
let y be set ; ::_thesis: ( y in dom (<:f,X,Y:> ") iff y in dom <:(f "),Y,X:> )
thus ( y in dom (<:f,X,Y:> ") implies y in dom <:(f "),Y,X:> ) ::_thesis: ( y in dom <:(f "),Y,X:> implies y in dom (<:f,X,Y:> ") )
proof
assume y in dom (<:f,X,Y:> ") ; ::_thesis: y in dom <:(f "),Y,X:>
then A3: y in rng <:f,X,Y:> by A2, FUNCT_1:33;
then consider x being set 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 y in dom <:(f "),Y,X:> by A4, A8, A7, Th24; ::_thesis: verum
end;
assume A9: y in dom <:(f "),Y,X:> ; ::_thesis: y in dom (<:f,X,Y:> ")
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 set 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 y in dom (<:f,X,Y:> ") by A2, A11, FUNCT_1:33; ::_thesis: verum
end;
then A12: dom (<:f,X,Y:> ") = dom <:(f "),Y,X:> by TARSKI:1;
for y being set st y in dom <:(f "),Y,X:> holds
<:(f "),Y,X:> . y = (<:f,X,Y:> ") . y
proof
let y be set ; ::_thesis: ( y in dom <:(f "),Y,X:> implies <:(f "),Y,X:> . y = (<:f,X,Y:> ") . y )
A13: rng <:f,X,Y:> c= rng f by Th23;
assume A14: y in dom <:(f "),Y,X:> ; ::_thesis: <:(f "),Y,X:> . y = (<:f,X,Y:> ") . y
then y in rng <:f,X,Y:> by A2, A12, FUNCT_1:33;
then consider x being set 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 <:(f "),Y,X:> . y = (<:f,X,Y:> ") . y by A14, A16, A17, Th26; ::_thesis: verum
end;
hence <:f,X,Y:> " = <:(f "),Y,X:> by A12, FUNCT_1:2; ::_thesis: verum
end;
theorem :: PARTFUN1:39
for Z, X, Y being set
for f being Function holds Z |` <:f,X,Y:> = <:f,X,(Z /\ Y):>
proof
let Z, X, Y be set ; ::_thesis: for f being Function holds Z |` <:f,X,Y:> = <:f,X,(Z /\ Y):>
let f be Function; ::_thesis: Z |` <:f,X,Y:> = <:f,X,(Z /\ Y):>
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 ; ::_thesis: verum
end;
definition
let X be set ;
let f be X -defined Relation;
attrf is total means :Def2: :: PARTFUN1:def 2
dom f = X;
end;
:: deftheorem Def2 defines total PARTFUN1:def_2_:_
for X being set
for f being b1 -defined Relation holds
( f is total iff dom f = X );
registration
let X be empty set ;
let Y be set ;
cluster -> total for Element of bool [:X,Y:];
coherence
for b1 being Relation of X,Y holds b1 is total
proof
let R be Relation of X,Y; ::_thesis: R is total
thus dom R = X ; :: according to PARTFUN1:def_2 ::_thesis: verum
end;
end;
registration
let X be non empty set ;
let Y be empty set ;
cluster -> non total for Element of bool [:X,Y:];
coherence
for b1 being Relation of X,Y holds not b1 is total
proof
let f be Relation of X,Y; ::_thesis: not f is total
assume f is total ; ::_thesis: contradiction
then dom f = X by Def2;
hence contradiction ; ::_thesis: verum
end;
end;
theorem Th40: :: PARTFUN1:40
for X, Y being set
for f being Function st <:f,X,Y:> is total holds
X c= dom f
proof
let X, Y be set ; ::_thesis: for f being Function st <:f,X,Y:> is total holds
X c= dom f
let f be Function; ::_thesis: ( <:f,X,Y:> is total implies X c= dom f )
assume A1: dom <:f,X,Y:> = X ; :: according to PARTFUN1:def_2 ::_thesis: X c= dom f
A2: dom <:f,X,Y:> c= dom f by Th23;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in dom f )
assume x in X ; ::_thesis: x in dom f
hence x in dom f by A1, A2; ::_thesis: verum
end;
theorem :: PARTFUN1:41
for X, Y being set st <:{},X,Y:> is total holds
X = {}
proof
let X, Y be set ; ::_thesis: ( <:{},X,Y:> is total implies X = {} )
dom {} = {} ;
hence ( <:{},X,Y:> is total implies X = {} ) by Th40, XBOOLE_1:3; ::_thesis: verum
end;
theorem :: PARTFUN1:42
for X, Y being set
for f being Function st X c= dom f & rng f c= Y holds
<:f,X,Y:> is total
proof
let X, Y be set ; ::_thesis: for f being Function st X c= dom f & rng f c= Y holds
<:f,X,Y:> is total
let f be Function; ::_thesis: ( X c= dom f & rng f c= Y implies <:f,X,Y:> is total )
assume that
A1: X c= dom f and
A2: rng f c= Y ; ::_thesis: <:f,X,Y:> is total
X c= dom <:f,X,Y:>
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in dom <:f,X,Y:> )
assume A3: x in X ; ::_thesis: x in dom <:f,X,Y:>
then f . x in rng f by A1, FUNCT_1:def_3;
hence x in dom <:f,X,Y:> by A1, A2, A3, Th24; ::_thesis: verum
end;
hence dom <:f,X,Y:> = X by XBOOLE_0:def_10; :: according to PARTFUN1:def_2 ::_thesis: verum
end;
theorem :: PARTFUN1:43
for X, Y being set
for f being Function st <:f,X,Y:> is total holds
f .: X c= Y
proof
let X, Y be set ; ::_thesis: for f being Function st <:f,X,Y:> is total holds
f .: X c= Y
let f be Function; ::_thesis: ( <:f,X,Y:> is total implies f .: X c= Y )
assume A1: dom <:f,X,Y:> = X ; :: according to PARTFUN1:def_2 ::_thesis: f .: X c= Y
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f .: X or y in Y )
A2: rng <:f,X,Y:> c= Y by RELAT_1:def_19;
assume y in f .: X ; ::_thesis: y in Y
then consider x being set 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 y in Y by A2; ::_thesis: verum
end;
theorem :: PARTFUN1:44
for X, Y being set
for f being Function st X c= dom f & f .: X c= Y holds
<:f,X,Y:> is total
proof
let X, Y be set ; ::_thesis: for f being Function st X c= dom f & f .: X c= Y holds
<:f,X,Y:> is total
let f be Function; ::_thesis: ( X c= dom f & f .: X c= Y implies <:f,X,Y:> is total )
assume that
A1: X c= dom f and
A2: f .: X c= Y ; ::_thesis: <:f,X,Y:> is total
X c= dom <:f,X,Y:>
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in dom <:f,X,Y:> )
assume A3: x in X ; ::_thesis: x in dom <:f,X,Y:>
then f . x in f .: X by A1, FUNCT_1:def_6;
hence x in dom <:f,X,Y:> by A1, A2, A3, Th24; ::_thesis: verum
end;
hence dom <:f,X,Y:> = X by XBOOLE_0:def_10; :: according to PARTFUN1:def_2 ::_thesis: verum
end;
definition
let X, Y be set ;
func PFuncs (X,Y) -> set means :Def3: :: PARTFUN1:def 3
for x being set holds
( x in it iff ex f being Function st
( x = f & dom f c= X & rng f c= Y ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ex f being Function st
( x = f & dom f c= X & rng f c= Y ) )
proof
defpred S1[ set ] means ex f being Function st
( $1 = f & dom f c= X & rng f c= Y );
consider F being set such that
A1: for z being set holds
( z in F iff ( z in bool [:X,Y:] & S1[z] ) ) from XBOOLE_0:sch_1();
take F ; ::_thesis: for x being set holds
( x in F iff ex f being Function st
( x = f & dom f c= X & rng f c= Y ) )
let z be set ; ::_thesis: ( z in F iff ex f being Function st
( z = f & dom f c= X & rng f c= Y ) )
thus ( z in F implies ex f being Function st
( z = f & dom f c= X & rng f c= Y ) ) by A1; ::_thesis: ( ex f being Function st
( z = f & dom f c= X & rng f c= Y ) implies z in F )
given f being Function such that A2: z = f and
A3: ( dom f c= X & rng f c= Y ) ; ::_thesis: z in F
f c= [:X,Y:]
proof
let x be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [x,b1] in f or [x,b1] in [:X,Y:] )
let y be set ; ::_thesis: ( not [x,y] in f or [x,y] in [:X,Y:] )
assume A4: [x,y] in f ; ::_thesis: [x,y] in [:X,Y:]
then A5: x in dom f by XTUPLE_0:def_12;
then y = f . x by A4, FUNCT_1:def_2;
then y in rng f by A5, FUNCT_1:def_3;
hence [x,y] in [:X,Y:] by A3, A5, ZFMISC_1:def_2; ::_thesis: verum
end;
hence z in F by A1, A2, A3; ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ex f being Function st
( x = f & dom f c= X & rng f c= Y ) ) ) & ( for x being set holds
( x in b2 iff ex f being Function st
( x = f & dom f c= X & rng f c= Y ) ) ) holds
b1 = b2
proof
let F1, F2 be set ; ::_thesis: ( ( for x being set holds
( x in F1 iff ex f being Function st
( x = f & dom f c= X & rng f c= Y ) ) ) & ( for x being set holds
( x in F2 iff ex f being Function st
( x = f & dom f c= X & rng f c= Y ) ) ) implies F1 = F2 )
assume that
A6: for x being set holds
( x in F1 iff ex f being Function st
( x = f & dom f c= X & rng f c= Y ) ) and
A7: for x being set holds
( x in F2 iff ex f being Function st
( x = f & dom f c= X & rng f c= Y ) ) ; ::_thesis: F1 = F2
for x being set holds
( x in F1 iff x in F2 )
proof
let x be set ; ::_thesis: ( x in F1 iff x in F2 )
( x in F1 iff ex f being Function st
( x = f & dom f c= X & rng f c= Y ) ) by A6;
hence ( x in F1 iff x in F2 ) by A7; ::_thesis: verum
end;
hence F1 = F2 by TARSKI:1; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines PFuncs PARTFUN1:def_3_:_
for X, Y, b3 being set holds
( b3 = PFuncs (X,Y) iff for x being set holds
( x in b3 iff ex f being Function st
( x = f & dom f c= X & rng f c= Y ) ) );
registration
let X, Y be set ;
cluster PFuncs (X,Y) -> non empty ;
coherence
not PFuncs (X,Y) is empty
proof
ex f being Function st
( dom f c= X & rng f c= Y ) by Lm1;
hence not PFuncs (X,Y) is empty by Def3; ::_thesis: verum
end;
end;
theorem Th45: :: PARTFUN1:45
for X, Y being set
for f being PartFunc of X,Y holds f in PFuncs (X,Y)
proof
let X, Y be set ; ::_thesis: for f being PartFunc of X,Y holds f in PFuncs (X,Y)
let f be PartFunc of X,Y; ::_thesis: f in PFuncs (X,Y)
( dom f c= X & rng f c= Y ) by RELAT_1:def_19;
hence f in PFuncs (X,Y) by Def3; ::_thesis: verum
end;
theorem Th46: :: PARTFUN1:46
for X, Y, f being set st f in PFuncs (X,Y) holds
f is PartFunc of X,Y
proof
let X, Y, f be set ; ::_thesis: ( f in PFuncs (X,Y) implies f is PartFunc of X,Y )
assume f in PFuncs (X,Y) ; ::_thesis: f is PartFunc of X,Y
then ex F being Function st
( f = F & dom F c= X & rng F c= Y ) by Def3;
hence f is PartFunc of X,Y by RELSET_1:4; ::_thesis: verum
end;
theorem :: PARTFUN1:47
for X, Y being set
for f being Element of PFuncs (X,Y) holds f is PartFunc of X,Y by Th46;
theorem :: PARTFUN1:48
for Y being set holds PFuncs ({},Y) = {{}}
proof
let Y be set ; ::_thesis: PFuncs ({},Y) = {{}}
for x being set holds
( x in PFuncs ({},Y) iff x = {} )
proof
let x be set ; ::_thesis: ( x in PFuncs ({},Y) iff x = {} )
thus ( x in PFuncs ({},Y) implies x = {} ) ::_thesis: ( x = {} implies x in PFuncs ({},Y) )
proof
assume x in PFuncs ({},Y) ; ::_thesis: x = {}
then x is PartFunc of {},Y by Th46;
hence x = {} ; ::_thesis: verum
end;
{} is PartFunc of {},Y by RELSET_1:12;
hence ( x = {} implies x in PFuncs ({},Y) ) by Th45; ::_thesis: verum
end;
hence PFuncs ({},Y) = {{}} by TARSKI:def_1; ::_thesis: verum
end;
theorem :: PARTFUN1:49
for X being set holds PFuncs (X,{}) = {{}}
proof
let X be set ; ::_thesis: PFuncs (X,{}) = {{}}
for x being set holds
( x in PFuncs (X,{}) iff x = {} )
proof
let x be set ; ::_thesis: ( x in PFuncs (X,{}) iff x = {} )
thus ( x in PFuncs (X,{}) implies x = {} ) ::_thesis: ( x = {} implies x in PFuncs (X,{}) )
proof
assume x in PFuncs (X,{}) ; ::_thesis: x = {}
then x is PartFunc of X,{} by Th46;
hence x = {} ; ::_thesis: verum
end;
{} is PartFunc of X,{} by RELSET_1:12;
hence ( x = {} implies x in PFuncs (X,{}) ) by Th45; ::_thesis: verum
end;
hence PFuncs (X,{}) = {{}} by TARSKI:def_1; ::_thesis: verum
end;
theorem :: PARTFUN1:50
for X1, X2, Y1, Y2 being set st X1 c= X2 & Y1 c= Y2 holds
PFuncs (X1,Y1) c= PFuncs (X2,Y2)
proof
let X1, X2, Y1, Y2 be set ; ::_thesis: ( X1 c= X2 & Y1 c= Y2 implies PFuncs (X1,Y1) c= PFuncs (X2,Y2) )
assume A1: ( X1 c= X2 & Y1 c= Y2 ) ; ::_thesis: PFuncs (X1,Y1) c= PFuncs (X2,Y2)
let f be set ; :: according to TARSKI:def_3 ::_thesis: ( not f in PFuncs (X1,Y1) or f in PFuncs (X2,Y2) )
assume f in PFuncs (X1,Y1) ; ::_thesis: f in PFuncs (X2,Y2)
then f is PartFunc of X1,Y1 by Th46;
then f is PartFunc of X2,Y2 by A1, RELSET_1:7;
hence f in PFuncs (X2,Y2) by Th45; ::_thesis: verum
end;
definition
let f, g be Function;
predf tolerates g means :Def4: :: PARTFUN1:def 4
for x being set st x in (dom f) /\ (dom g) holds
f . x = g . x;
reflexivity
for f being Function
for x being set st x in (dom f) /\ (dom f) holds
f . x = f . x ;
symmetry
for f, g being Function st ( for x being set st x in (dom f) /\ (dom g) holds
f . x = g . x ) holds
for x being set st x in (dom g) /\ (dom f) holds
g . x = f . x ;
end;
:: deftheorem Def4 defines tolerates PARTFUN1:def_4_:_
for f, g being Function holds
( f tolerates g iff for x being set st x in (dom f) /\ (dom g) holds
f . x = g . x );
theorem Th51: :: PARTFUN1:51
for f, g being Function holds
( f tolerates g iff ex h being Function st f \/ g = h )
proof
let f, g be Function; ::_thesis: ( f tolerates g iff ex h being Function st f \/ g = h )
( ( for x being set st x in (dom f) /\ (dom g) holds
f . x = g . x ) iff ex h being Function st f \/ g = h ) by Th1, Th2;
hence ( f tolerates g iff ex h being Function st f \/ g = h ) by Def4; ::_thesis: verum
end;
theorem Th52: :: PARTFUN1:52
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; ::_thesis: ( f tolerates g iff ex h being Function st
( f c= h & g c= h ) )
now__::_thesis:_(_(_ex_h_being_Function_st_
(_f_c=_h_&_g_c=_h_)_implies_ex_h_being_Function_st_f_\/_g_=_h_)_&_(_ex_h_being_Function_st_f_\/_g_=_h_implies_ex_h_being_Function_st_
(_f_c=_h_&_g_c=_h_)_)_)
thus ( ex h being Function st
( f c= h & g c= h ) implies ex h being Function st f \/ g = h ) ::_thesis: ( ex h being Function st f \/ g = h implies ex h being Function st
( f c= h & g c= h ) )
proof
given h being Function such that A1: ( f c= h & g c= h ) ; ::_thesis: ex h being Function st f \/ g = h
f \/ g is Function by A1, GRFUNC_1:1, XBOOLE_1:8;
hence ex h being Function st f \/ g = h ; ::_thesis: verum
end;
given h being Function such that A2: f \/ g = h ; ::_thesis: ex h being Function st
( f c= h & g c= h )
( f c= h & g c= h ) by A2, XBOOLE_1:7;
hence ex h being Function st
( f c= h & g c= h ) ; ::_thesis: verum
end;
hence ( f tolerates g iff ex h being Function st
( f c= h & g c= h ) ) by Th51; ::_thesis: verum
end;
theorem Th53: :: PARTFUN1:53
for f, g being Function st dom f c= dom g holds
( f tolerates g iff for x being set st x in dom f holds
f . x = g . x )
proof
let f, g be Function; ::_thesis: ( dom f c= dom g implies ( f tolerates g iff for x being set st x in dom f holds
f . x = g . x ) )
assume dom f c= dom g ; ::_thesis: ( f tolerates g iff for x being set st x in dom f holds
f . x = g . x )
then (dom f) /\ (dom g) = dom f by XBOOLE_1:28;
hence ( f tolerates g iff for x being set st x in dom f holds
f . x = g . x ) by Def4; ::_thesis: verum
end;
theorem :: PARTFUN1:54
for f, g being Function st f c= g holds
f tolerates g by Th52;
theorem Th55: :: PARTFUN1:55
for f, g being Function st dom f = dom g & f tolerates g holds
f = g
proof
let f, g be Function; ::_thesis: ( dom f = dom g & f tolerates g implies f = g )
assume that
A1: dom f = dom g and
A2: f tolerates g ; ::_thesis: f = g
for x being set st x in dom f holds
f . x = g . x by A1, A2, Th53;
hence f = g by A1, FUNCT_1:2; ::_thesis: verum
end;
theorem :: PARTFUN1:56
for f, g being Function st dom f misses dom g holds
f tolerates g
proof
let f, g be Function; ::_thesis: ( dom f misses dom g implies f tolerates g )
assume dom f misses dom g ; ::_thesis: f tolerates g
then f \/ g is Function by GRFUNC_1:13;
hence f tolerates g by Th51; ::_thesis: verum
end;
theorem :: PARTFUN1:57
for f, g, h being Function st f c= h & g c= h holds
f tolerates g by Th52;
theorem :: PARTFUN1:58
for X, Y being set
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 X, Y be set ; ::_thesis: for f, g being PartFunc of X,Y
for h being Function st f tolerates h & g c= f holds
g tolerates h
let f, g be PartFunc of X,Y; ::_thesis: for h being Function st f tolerates h & g c= f holds
g tolerates h
let h be Function; ::_thesis: ( f tolerates h & g c= f implies g tolerates h )
assume that
A1: f tolerates h and
A2: g c= f ; ::_thesis: g tolerates h
A3: dom g c= dom f by A2, RELAT_1:11;
let x be set ; :: according to PARTFUN1:def_4 ::_thesis: ( x in (dom g) /\ (dom h) implies g . x = h . x )
assume A4: x in (dom g) /\ (dom h) ; ::_thesis: g . x = h . x
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 g . x = h . x by A1, A6, Def4; ::_thesis: verum
end;
theorem Th59: :: PARTFUN1:59
for f being Function holds {} tolerates f
proof
let f be Function; ::_thesis: {} tolerates f
{} \/ f = f ;
hence {} tolerates f by Th51; ::_thesis: verum
end;
theorem :: PARTFUN1:60
for X, Y being set
for f being Function holds <:{},X,Y:> tolerates f
proof
let X, Y be set ; ::_thesis: for f being Function holds <:{},X,Y:> tolerates f
let f be Function; ::_thesis: <:{},X,Y:> tolerates f
<:{},X,Y:> = {} by Th34;
hence <:{},X,Y:> tolerates f by Th59; ::_thesis: verum
end;
theorem :: PARTFUN1:61
for X, y being set
for f, g being PartFunc of X,{y} holds f tolerates g
proof
let X, y be set ; ::_thesis: for f, g being PartFunc of X,{y} holds f tolerates g
let f, g be PartFunc of X,{y}; ::_thesis: f tolerates g
let x be set ; :: according to PARTFUN1:def_4 ::_thesis: ( x in (dom f) /\ (dom g) implies f . x = g . x )
assume A1: x in (dom f) /\ (dom g) ; ::_thesis: f . x = g . x
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 f . x = g . x by A2, Th20; ::_thesis: verum
end;
theorem :: PARTFUN1:62
for X being set
for f being Function holds f | X tolerates f
proof
let X be set ; ::_thesis: for f being Function holds f | X tolerates f
let f be Function; ::_thesis: f | X tolerates f
f | X c= f by RELAT_1:59;
hence f | X tolerates f by Th52; ::_thesis: verum
end;
theorem :: PARTFUN1:63
for Y being set
for f being Function holds Y |` f tolerates f
proof
let Y be set ; ::_thesis: for f being Function holds Y |` f tolerates f
let f be Function; ::_thesis: Y |` f tolerates f
Y |` f c= f by RELAT_1:86;
hence Y |` f tolerates f by Th52; ::_thesis: verum
end;
theorem Th64: :: PARTFUN1:64
for Y, X being set
for f being Function holds (Y |` f) | X tolerates f
proof
let Y, X be set ; ::_thesis: for f being Function holds (Y |` f) | X tolerates f
let f be Function; ::_thesis: (Y |` f) | X tolerates f
( (Y |` f) | X c= Y |` f & Y |` f c= f ) by RELAT_1:59, RELAT_1:86;
then (Y |` f) | X c= f by XBOOLE_1:1;
hence (Y |` f) | X tolerates f by Th52; ::_thesis: verum
end;
theorem :: PARTFUN1:65
for X, Y being set
for f being Function holds <:f,X,Y:> tolerates f by Th64;
theorem Th66: :: PARTFUN1:66
for X, Y being set
for f, g being PartFunc of X,Y st f is total & g is total & f tolerates g holds
f = g
proof
let X, Y be set ; ::_thesis: for f, g being PartFunc of X,Y st f is total & g is total & f tolerates g holds
f = g
let f, g be PartFunc of X,Y; ::_thesis: ( f is total & g is total & f tolerates g implies f = g )
assume ( dom f = X & dom g = X ) ; :: according to PARTFUN1:def_2 ::_thesis: ( not f tolerates g or f = g )
hence ( not f tolerates g or f = g ) by Th55; ::_thesis: verum
end;
theorem Th67: :: PARTFUN1:67
for X, Y being set
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 X, Y be set ; ::_thesis: for f, g, h being PartFunc of X,Y st f tolerates h & g tolerates h & h is total holds
f tolerates g
let f, g, h be PartFunc of X,Y; ::_thesis: ( f tolerates h & g tolerates h & h is total implies f tolerates g )
assume that
A1: f tolerates h and
A2: g tolerates h and
A3: dom h = X ; :: according to PARTFUN1:def_2 ::_thesis: f tolerates g
let x be set ; :: according to PARTFUN1:def_4 ::_thesis: ( x in (dom f) /\ (dom g) implies f . x = g . x )
assume A4: x in (dom f) /\ (dom g) ; ::_thesis: f . x = g . x
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, Def4;
x in dom g by A4, XBOOLE_0:def_4;
then x in (dom g) /\ (dom h) by A3, XBOOLE_0:def_4;
hence f . x = g . x by A2, A5, Def4; ::_thesis: verum
end;
theorem Th68: :: PARTFUN1:68
for X, Y being set
for f, g being PartFunc of X,Y st ( Y = {} implies X = {} ) & f tolerates g holds
ex h being PartFunc of X,Y st
( h is total & f tolerates h & g tolerates h )
proof
let X, Y be set ; ::_thesis: for f, g being PartFunc of X,Y st ( Y = {} implies X = {} ) & f tolerates g holds
ex h being PartFunc of X,Y st
( h is total & f tolerates h & g tolerates h )
let f, g be PartFunc of X,Y; ::_thesis: ( ( Y = {} implies X = {} ) & f tolerates g implies ex h being PartFunc of X,Y st
( h is total & f tolerates h & g tolerates h ) )
assume that
A1: ( Y = {} implies X = {} ) and
A2: f tolerates g ; ::_thesis: ex h being PartFunc of X,Y st
( h is total & f tolerates h & g tolerates h )
now__::_thesis:_ex_h_being_PartFunc_of_X,Y_st_
(_h_is_total_&_f_tolerates_h_&_g_tolerates_h_)
percases ( Y = {} or Y <> {} ) ;
supposeA3: Y = {} ; ::_thesis: ex h being PartFunc of X,Y st
( h is total & f tolerates h & g tolerates h )
then ( f tolerates <:{},X,Y:> & g tolerates <:{},X,Y:> ) ;
hence ex h being PartFunc of X,Y st
( h is total & f tolerates h & g tolerates h ) by A1, A3; ::_thesis: verum
end;
supposeA4: Y <> {} ; ::_thesis: ex h being PartFunc of X,Y st
( h is total & f tolerates h & g tolerates h )
set y = the Element of Y;
defpred S1[ set , set ] 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 = the Element of Y ) );
A5: for x being set st x in X holds
ex y9 being set st S1[x,y9]
proof
let x be set ; ::_thesis: ( x in X implies ex y9 being set st S1[x,y9] )
assume x in X ; ::_thesis: ex y9 being set st S1[x,y9]
now__::_thesis:_ex_y9_being_set_st_
(_(_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_=_the_Element_of_Y_)_)
percases ( ( x in dom f & x in dom g ) or ( x in dom f & not x in dom g ) or ( not x in dom f & x in dom g ) or ( not x in dom f & not x in dom g ) ) ;
supposeA6: ( x in dom f & x in dom g ) ; ::_thesis: ex y9 being set st
( ( 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 = the Element of Y ) )
take y9 = f . x; ::_thesis: ( ( 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 = the Element of Y ) )
thus ( x in dom f implies y9 = f . x ) ; ::_thesis: ( ( x in dom g implies y9 = g . x ) & ( not x in dom f & not x in dom g implies y9 = the Element of Y ) )
x in (dom f) /\ (dom g) by A6, XBOOLE_0:def_4;
hence ( x in dom g implies y9 = g . x ) by A2, Def4; ::_thesis: ( not x in dom f & not x in dom g implies y9 = the Element of Y )
thus ( not x in dom f & not x in dom g implies y9 = the Element of Y ) by A6; ::_thesis: verum
end;
supposeA7: ( x in dom f & not x in dom g ) ; ::_thesis: ex y9 being set st
( ( 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 = the Element of Y ) )
take y9 = f . x; ::_thesis: ( ( 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 = the Element of Y ) )
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 = the Element of Y ) ) by A7; ::_thesis: verum
end;
supposeA8: ( not x in dom f & x in dom g ) ; ::_thesis: ex y9 being set st
( ( 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 = the Element of Y ) )
take y9 = g . x; ::_thesis: ( ( 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 = the Element of Y ) )
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 = the Element of Y ) ) by A8; ::_thesis: verum
end;
suppose ( not x in dom f & not x in dom g ) ; ::_thesis: ex y9 being set st S1[x,y9]
hence ex y9 being set st S1[x,y9] ; ::_thesis: verum
end;
end;
end;
hence ex y9 being set st S1[x,y9] ; ::_thesis: verum
end;
A9: for x, y1, y2 being set st x in X & S1[x,y1] & S1[x,y2] holds
y1 = y2 ;
consider h being Function such that
A10: dom h = X and
A11: for x being set st x in X holds
S1[x,h . x] from FUNCT_1:sch_2(A9, A5);
rng h c= Y
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng h or z in Y )
assume z in rng h ; ::_thesis: z in Y
then consider x being set such that
A12: x in dom h and
A13: z = h . x by FUNCT_1:def_3;
percases ( ( x in dom f & x in dom g ) or ( x in dom f & not x in dom g ) or ( not x in dom f & x in dom g ) or ( not x in dom f & not x in dom g ) ) ;
supposeA14: ( x in dom f & x in dom g ) ; ::_thesis: z in Y
then z = f . x by A11, A13;
hence z in Y by A14, Th4; ::_thesis: verum
end;
supposeA15: ( x in dom f & not x in dom g ) ; ::_thesis: z in Y
then z = f . x by A11, A13;
hence z in Y by A15, Th4; ::_thesis: verum
end;
supposeA16: ( not x in dom f & x in dom g ) ; ::_thesis: z in Y
then z = g . x by A11, A13;
hence z in Y by A16, Th4; ::_thesis: verum
end;
suppose ( not x in dom f & not x in dom g ) ; ::_thesis: z in Y
then z = the Element of Y by A10, A11, A12, A13;
hence z in Y by A4; ::_thesis: verum
end;
end;
end;
then reconsider h9 = h as PartFunc of X,Y by A10, RELSET_1:4;
A17: f tolerates h
proof
let x be set ; :: according to PARTFUN1:def_4 ::_thesis: ( x in (dom f) /\ (dom h) implies f . x = h . x )
assume x in (dom f) /\ (dom h) ; ::_thesis: f . x = h . x
then x in dom f by XBOOLE_0:def_4;
hence f . x = h . x by A11; ::_thesis: verum
end;
A18: g tolerates h
proof
let x be set ; :: according to PARTFUN1:def_4 ::_thesis: ( x in (dom g) /\ (dom h) implies g . x = h . x )
assume x in (dom g) /\ (dom h) ; ::_thesis: g . x = h . x
then x in dom g by XBOOLE_0:def_4;
hence g . x = h . x by A11; ::_thesis: verum
end;
h9 is total by A10, Def2;
hence ex h being PartFunc of X,Y st
( h is total & f tolerates h & g tolerates h ) by A17, A18; ::_thesis: verum
end;
end;
end;
hence ex h being PartFunc of X,Y st
( h is total & f tolerates h & g tolerates h ) ; ::_thesis: verum
end;
definition
let X, Y be set ;
let f be PartFunc of X,Y;
func TotFuncs f -> set means :Def5: :: PARTFUN1:def 5
for x being set holds
( x in it iff ex g being PartFunc of X,Y st
( g = x & g is total & f tolerates g ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ex g being PartFunc of X,Y st
( g = x & g is total & f tolerates g ) )
proof
defpred S1[ set ] means ex g being PartFunc of X,Y st
( g = $1 & g is total & f tolerates g );
now__::_thesis:_ex_F_being_set_st_
for_x_being_set_holds_
(_(_x_in_F_implies_ex_g_being_PartFunc_of_X,Y_st_
(_g_=_x_&_g_is_total_&_f_tolerates_g_)_)_&_(_ex_g_being_PartFunc_of_X,Y_st_
(_g_=_x_&_g_is_total_&_f_tolerates_g_)_implies_x_in_F_)_)
consider F being set such that
A1: for x being set holds
( x in F iff ( x in PFuncs (X,Y) & S1[x] ) ) from XBOOLE_0:sch_1();
take F = F; ::_thesis: for x being set holds
( ( x in F implies ex g being PartFunc of X,Y st
( g = x & g is total & f tolerates g ) ) & ( ex g being PartFunc of X,Y st
( g = x & g is total & f tolerates g ) implies x in F ) )
let x be set ; ::_thesis: ( ( x in F implies ex g being PartFunc of X,Y st
( g = x & g is total & f tolerates g ) ) & ( ex g being PartFunc of X,Y st
( g = x & g is total & f tolerates g ) implies x in F ) )
thus ( x in F implies ex g being PartFunc of X,Y st
( g = x & g is total & f tolerates g ) ) by A1; ::_thesis: ( ex g being PartFunc of X,Y st
( g = x & g is total & f tolerates g ) implies x in F )
given g being PartFunc of X,Y such that A2: ( g = x & g is total & f tolerates g ) ; ::_thesis: x in F
g in PFuncs (X,Y) by Th45;
hence x in F by A1, A2; ::_thesis: verum
end;
hence ex b1 being set st
for x being set holds
( x in b1 iff ex g being PartFunc of X,Y st
( g = x & g is total & f tolerates g ) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ex g being PartFunc of X,Y st
( g = x & g is total & f tolerates g ) ) ) & ( for x being set holds
( x in b2 iff ex g being PartFunc of X,Y st
( g = x & g is total & f tolerates g ) ) ) holds
b1 = b2
proof
defpred S1[ set ] means ex g being PartFunc of X,Y st
( g = $1 & g is total & f tolerates g );
let F1, F2 be set ; ::_thesis: ( ( for x being set holds
( x in F1 iff ex g being PartFunc of X,Y st
( g = x & g is total & f tolerates g ) ) ) & ( for x being set holds
( x in F2 iff ex g being PartFunc of X,Y st
( g = x & g is total & f tolerates g ) ) ) implies F1 = F2 )
assume that
A3: for x being set holds
( x in F1 iff S1[x] ) and
A4: for x being set holds
( x in F2 iff S1[x] ) ; ::_thesis: F1 = F2
thus F1 = F2 from XBOOLE_0:sch_2(A3, A4); ::_thesis: verum
end;
end;
:: deftheorem Def5 defines TotFuncs PARTFUN1:def_5_:_
for X, Y being set
for f being PartFunc of X,Y
for b4 being set holds
( b4 = TotFuncs f iff for x being set holds
( x in b4 iff ex g being PartFunc of X,Y st
( g = x & g is total & f tolerates g ) ) );
theorem Th69: :: PARTFUN1:69
for X, Y being set
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 X, Y be set ; ::_thesis: for f being PartFunc of X,Y
for g being set st g in TotFuncs f holds
g is PartFunc of X,Y
let f be PartFunc of X,Y; ::_thesis: for g being set st g in TotFuncs f holds
g is PartFunc of X,Y
let g be set ; ::_thesis: ( g in TotFuncs f implies g is PartFunc of X,Y )
assume g in TotFuncs f ; ::_thesis: g is PartFunc of X,Y
then ex g9 being PartFunc of X,Y st
( g9 = g & g9 is total & f tolerates g9 ) by Def5;
hence g is PartFunc of X,Y ; ::_thesis: verum
end;
theorem Th70: :: PARTFUN1:70
for X, Y being set
for f, g being PartFunc of X,Y st g in TotFuncs f holds
g is total
proof
let X, Y be set ; ::_thesis: for f, g being PartFunc of X,Y st g in TotFuncs f holds
g is total
let f, g be PartFunc of X,Y; ::_thesis: ( g in TotFuncs f implies g is total )
assume g in TotFuncs f ; ::_thesis: g is total
then ex g9 being PartFunc of X,Y st
( g9 = g & g9 is total & f tolerates g9 ) by Def5;
hence g is total ; ::_thesis: verum
end;
theorem Th71: :: PARTFUN1:71
for X, Y being set
for f being PartFunc of X,Y
for g being Function st g in TotFuncs f holds
f tolerates g
proof
let X, Y be set ; ::_thesis: for f being PartFunc of X,Y
for g being Function st g in TotFuncs f holds
f tolerates g
let f be PartFunc of X,Y; ::_thesis: for g being Function st g in TotFuncs f holds
f tolerates g
let g be Function; ::_thesis: ( g in TotFuncs f implies f tolerates g )
assume g in TotFuncs f ; ::_thesis: f tolerates g
then ex g9 being PartFunc of X,Y st
( g9 = g & g9 is total & f tolerates g9 ) by Def5;
hence f tolerates g ; ::_thesis: verum
end;
registration
let X be non empty set ;
let Y be empty set ;
let f be PartFunc of X,Y;
cluster TotFuncs f -> empty ;
coherence
TotFuncs f is empty
proof
set g = the Element of TotFuncs f;
assume not TotFuncs f is empty ; ::_thesis: contradiction
then ex g9 being PartFunc of X,{} st
( g9 = the Element of TotFuncs f & g9 is total & f tolerates g9 ) by Def5;
hence contradiction ; ::_thesis: verum
end;
end;
theorem Th72: :: PARTFUN1:72
for X, Y being set
for f being PartFunc of X,Y holds
( f is total iff TotFuncs f = {f} )
proof
let X, Y be set ; ::_thesis: for f being PartFunc of X,Y holds
( f is total iff TotFuncs f = {f} )
let f be PartFunc of X,Y; ::_thesis: ( f is total iff TotFuncs f = {f} )
thus ( f is total implies TotFuncs f = {f} ) ::_thesis: ( TotFuncs f = {f} implies f is total )
proof
assume A1: f is total ; ::_thesis: TotFuncs f = {f}
for g being set holds
( g in TotFuncs f iff f = g )
proof
let g be set ; ::_thesis: ( g in TotFuncs f iff f = g )
thus ( g in TotFuncs f implies f = g ) ::_thesis: ( f = g implies g in TotFuncs f )
proof
assume g in TotFuncs f ; ::_thesis: f = g
then ex g9 being PartFunc of X,Y st
( g9 = g & g9 is total & f tolerates g9 ) by Def5;
hence f = g by A1, Th66; ::_thesis: verum
end;
thus ( f = g implies g in TotFuncs f ) by A1, Def5; ::_thesis: verum
end;
hence TotFuncs f = {f} by TARSKI:def_1; ::_thesis: verum
end;
assume TotFuncs f = {f} ; ::_thesis: f is total
then f in TotFuncs f by TARSKI:def_1;
hence f is total by Th70; ::_thesis: verum
end;
theorem :: PARTFUN1:73
for Y being set
for f being PartFunc of {},Y holds TotFuncs f = {f} by Th72;
theorem :: PARTFUN1:74
for Y being set
for f being PartFunc of {},Y holds TotFuncs f = {{}} by Th72;
theorem :: PARTFUN1:75
for X, Y being set
for f, g being PartFunc of X,Y st TotFuncs f meets TotFuncs g holds
f tolerates g
proof
let X, Y be set ; ::_thesis: for f, g being PartFunc of X,Y st TotFuncs f meets TotFuncs g holds
f tolerates g
let f, g be PartFunc of X,Y; ::_thesis: ( TotFuncs f meets TotFuncs g implies f tolerates g )
set h = the Element of (TotFuncs f) /\ (TotFuncs g);
assume A1: (TotFuncs f) /\ (TotFuncs g) <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: f tolerates g
then A2: the Element of (TotFuncs f) /\ (TotFuncs g) in TotFuncs f by XBOOLE_0:def_4;
A3: the Element of (TotFuncs f) /\ (TotFuncs g) in TotFuncs g by A1, XBOOLE_0:def_4;
reconsider h = the Element of (TotFuncs f) /\ (TotFuncs g) as PartFunc of X,Y by A2, Th69;
A4: g tolerates h by A3, Th71;
f tolerates h by A2, Th71;
hence f tolerates g by A2, A4, Th67, Th70; ::_thesis: verum
end;
theorem :: PARTFUN1:76
for X, Y being set
for f, g being PartFunc of X,Y st ( Y = {} implies X = {} ) & f tolerates g holds
TotFuncs f meets TotFuncs g
proof
let X, Y be set ; ::_thesis: for f, g being PartFunc of X,Y st ( Y = {} implies X = {} ) & f tolerates g holds
TotFuncs f meets TotFuncs g
let f, g be PartFunc of X,Y; ::_thesis: ( ( Y = {} implies X = {} ) & f tolerates g implies TotFuncs f meets TotFuncs g )
assume ( ( Y = {} implies X = {} ) & f tolerates g ) ; ::_thesis: TotFuncs f meets TotFuncs 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; :: according to XBOOLE_0:def_7 ::_thesis: verum
end;
begin
Lm2: for X being set
for R being Relation of X st R = id X holds
R is total
proof
let X be set ; ::_thesis: for R being Relation of X st R = id X holds
R is total
let R be Relation of X; ::_thesis: ( R = id X implies R is total )
assume R = id X ; ::_thesis: R is total
hence dom R = X by RELAT_1:45; :: according to PARTFUN1:def_2 ::_thesis: verum
end;
Lm3: for X being set
for R being Relation st R = id X holds
( R is reflexive & R is symmetric & R is antisymmetric & R is transitive )
proof
let X be set ; ::_thesis: for R being Relation st R = id X holds
( R is reflexive & R is symmetric & R is antisymmetric & R is transitive )
let R be Relation; ::_thesis: ( R = id X implies ( R is reflexive & R is symmetric & R is antisymmetric & R is transitive ) )
assume A1: R = id X ; ::_thesis: ( R is reflexive & R is symmetric & R is antisymmetric & R is transitive )
then A2: ( dom R = X & rng R = X ) by RELAT_1:45;
thus R is_reflexive_in field R :: according to RELAT_2:def_9 ::_thesis: ( R is symmetric & R is antisymmetric & R is transitive )
proof
let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in field R or [x,x] in R )
thus ( not x in field R or [x,x] in R ) by A1, A2, RELAT_1:def_10; ::_thesis: verum
end;
thus R is_symmetric_in field R :: according to RELAT_2:def_11 ::_thesis: ( R is antisymmetric & R is transitive )
proof
let x be set ; :: according to RELAT_2:def_3 ::_thesis: for b1 being set holds
( not x in field R or not b1 in field R or not [x,b1] in R or [b1,x] in R )
let y be set ; ::_thesis: ( not x in field R or not y in field R or not [x,y] in R or [y,x] in R )
assume that
x in field R and
y in field R ; ::_thesis: ( not [x,y] in R or [y,x] in R )
assume [x,y] in R ; ::_thesis: [y,x] in R
hence [y,x] in R by A1, RELAT_1:def_10; ::_thesis: verum
end;
thus R is_antisymmetric_in field R :: according to RELAT_2:def_12 ::_thesis: R is transitive
proof
let x be set ; :: according to RELAT_2:def_4 ::_thesis: for b1 being set holds
( not x in field R or not b1 in field R or not [x,b1] in R or not [b1,x] in R or x = b1 )
thus for b1 being set holds
( not x in field R or not b1 in field R or not [x,b1] in R or not [b1,x] in R or x = b1 ) by A1, RELAT_1:def_10; ::_thesis: verum
end;
thus R is_transitive_in field R :: according to RELAT_2:def_16 ::_thesis: verum
proof
let x be set ; :: according to RELAT_2:def_8 ::_thesis: for b1, b2 being set holds
( not x in field R or not b1 in field R or not b2 in field R or not [x,b1] in R or not [b1,b2] in R or [x,b2] in R )
thus for b1, b2 being set holds
( not x in field R or not b1 in field R or not b2 in field R or not [x,b1] in R or not [b1,b2] in R or [x,b2] in R ) by A1, RELAT_1:def_10; ::_thesis: verum
end;
end;
Lm4: for X being set holds id X is Relation of X
proof
let X be set ; ::_thesis: id X is Relation of X
( dom (id X) c= X & rng (id X) c= X ) ;
hence id X is Relation of X by RELSET_1:4; ::_thesis: verum
end;
registration
let X be set ;
cluster Relation-like X -defined X -valued reflexive symmetric antisymmetric transitive total for Element of bool [:X,X:];
existence
ex b1 being Relation of X st
( b1 is total & b1 is reflexive & b1 is symmetric & b1 is antisymmetric & b1 is transitive )
proof
reconsider R = id X as Relation of X by Lm4;
take R ; ::_thesis: ( R is total & R is reflexive & R is symmetric & R is antisymmetric & R is transitive )
thus ( R is total & R is reflexive & R is symmetric & R is antisymmetric & R is transitive ) by Lm2, Lm3; ::_thesis: verum
end;
end;
registration
cluster Relation-like symmetric transitive -> reflexive for set ;
coherence
for b1 being Relation st b1 is symmetric & b1 is transitive holds
b1 is reflexive
proof
let R be Relation; ::_thesis: ( R is symmetric & R is transitive implies R is reflexive )
assume that
A1: R is_symmetric_in field R and
A2: R is_transitive_in field R ; :: according to RELAT_2:def_11,RELAT_2:def_16 ::_thesis: R is reflexive
let x be set ; :: according to RELAT_2:def_1,RELAT_2:def_9 ::_thesis: ( not x in field R or [x,x] in R )
assume A3: x in field R ; ::_thesis: [x,x] in R
then ( x in dom R or x in rng R ) by XBOOLE_0:def_3;
then consider y being set such that
A4: ( [x,y] in R or [y,x] in R ) by XTUPLE_0:def_12, XTUPLE_0:def_13;
( y in rng R or y in dom R ) by A4, XTUPLE_0:def_12, XTUPLE_0: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, RELAT_2:def_3;
hence [x,x] in R by A2, A3, A5, RELAT_2:def_8; ::_thesis: verum
end;
end;
registration
let X be set ;
cluster id X -> symmetric antisymmetric transitive ;
coherence
( id X is symmetric & id X is antisymmetric & id X is transitive ) by Lm3;
end;
definition
let X be set ;
:: original: id
redefine func id X -> total Relation of X;
coherence
id X is total Relation of X by Lm2, Lm4;
end;
scheme :: PARTFUN1:sch 4
LambdaC9{ F1() -> non empty set , P1[ set ], F2( set ) -> set , F3( set ) -> set } :
ex f being Function st
( dom f = F1() & ( for x being Element of F1() holds
( ( P1[x] implies f . x = F2(x) ) & ( P1[x] implies f . x = F3(x) ) ) ) )
proof
consider f being Function such that
A1: ( dom f = F1() & ( for x being set st x in F1() holds
( ( P1[x] implies f . x = F2(x) ) & ( P1[x] implies f . x = F3(x) ) ) ) ) from PARTFUN1:sch_1();
take f ; ::_thesis: ( dom f = F1() & ( for x being Element of F1() holds
( ( P1[x] implies f . x = F2(x) ) & ( P1[x] implies f . x = F3(x) ) ) ) )
thus ( dom f = F1() & ( for x being Element of F1() holds
( ( P1[x] implies f . x = F2(x) ) & ( P1[x] implies f . x = F3(x) ) ) ) ) by A1; ::_thesis: verum
end;
begin
theorem Th77: :: PARTFUN1:77
for x, y, z being set
for f, g being Function st f tolerates g & [x,y] in f & [x,z] in g holds
y = z
proof
let x, y, z be set ; ::_thesis: for f, g being Function st f tolerates g & [x,y] in f & [x,z] in g holds
y = z
let f, g be Function; ::_thesis: ( f tolerates g & [x,y] in f & [x,z] in g implies y = z )
assume f tolerates g ; ::_thesis: ( not [x,y] in f or not [x,z] in g or y = z )
then consider h being Function such that
A1: h = f \/ g by Th51;
assume ( [x,y] in f & [x,z] in g ) ; ::_thesis: y = z
then ( [x,y] in h & [x,z] in h ) by A1, XBOOLE_0:def_3;
hence y = z by FUNCT_1:def_1; ::_thesis: verum
end;
theorem :: PARTFUN1:78
for A being set st A is functional & ( for f, g being Function st f in A & g in A holds
f tolerates g ) holds
union A is Function
proof
let A be set ; ::_thesis: ( A is functional & ( for f, g being Function st f in A & g in A holds
f tolerates g ) implies union A is Function )
assume that
A1: for x being set 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 ; :: according to FUNCT_1:def_13 ::_thesis: union A is Function
A3: now__::_thesis:_for_x,_y,_z_being_set_st_[x,y]_in_union_A_&_[x,z]_in_union_A_holds_
y_=_z
let x, y, z be set ; ::_thesis: ( [x,y] in union A & [x,z] in union A implies y = z )
assume that
A4: [x,y] in union A and
A5: [x,z] in union A ; ::_thesis: y = z
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 = p, q = q as Function by A1, A7, A9;
p tolerates q by A2, A7, A9;
hence y = z by A6, A8, Th77; ::_thesis: verum
end;
now__::_thesis:_for_z_being_set_st_z_in_union_A_holds_
ex_x,_y_being_set_st_[x,y]_=_z
let z be set ; ::_thesis: ( z in union A implies ex x, y being set st [x,y] = z )
assume z in union A ; ::_thesis: ex x, y being set st [x,y] = z
then consider p being set such that
A10: z in p and
A11: p in A by TARSKI:def_4;
reconsider p = p as Function by A1, A11;
p = p ;
hence ex x, y being set st [x,y] = z by A10, RELAT_1:def_1; ::_thesis: verum
end;
hence union A is Function by A3, FUNCT_1:def_1, RELAT_1:def_1; ::_thesis: verum
end;
definition
let D be set ;
let p be D -valued Function;
let i be set ;
assume A1: i in dom p ;
funcp /. i -> Element of D equals :Def6: :: PARTFUN1:def 6
p . i;
coherence
p . i is Element of D by A1, Th4;
end;
:: deftheorem Def6 defines /. PARTFUN1:def_6_:_
for D being set
for p being b1 -valued Function
for i being set st i in dom p holds
p /. i = p . i;
registration
let X, Y be non empty set ;
cluster Relation-like X -defined Y -valued Function-like non empty for Element of bool [:X,Y:];
existence
not for b1 being PartFunc of X,Y holds b1 is empty
proof
reconsider p = {[(choose X),(choose Y)]} as PartFunc of X,Y by RELSET_1:3;
take p ; ::_thesis: not p is empty
thus not p is empty ; ::_thesis: verum
end;
end;
registration
let A, B be set ;
cluster PFuncs (A,B) -> functional ;
coherence
PFuncs (A,B) is functional
proof
let x be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not x in PFuncs (A,B) or x is set )
assume x in PFuncs (A,B) ; ::_thesis: x is set
then ex f being Function st
( x = f & dom f c= A & rng f c= B ) by Def3;
hence x is set ; ::_thesis: verum
end;
end;
theorem :: PARTFUN1:79
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; ::_thesis: ( rng g c= dom f1 & rng g c= dom f2 & f1 tolerates f2 implies f1 * g = f2 * g )
assume that
A1: rng g c= dom f1 and
A2: rng g c= dom f2 and
A3: f1 tolerates f2 ; ::_thesis: f1 * g = f2 * g
A4: dom (f2 * g) = dom g by A2, RELAT_1:27;
A5: dom (f1 * g) = dom g by A1, RELAT_1:27;
now__::_thesis:_for_x_being_set_st_x_in_dom_g_holds_
(f1_*_g)_._x_=_(f2_*_g)_._x
let x be set ; ::_thesis: ( x in dom g implies (f1 * g) . x = (f2 * g) . x )
assume A6: x in dom g ; ::_thesis: (f1 * g) . x = (f2 * g) . x
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, Def4; ::_thesis: verum
end;
hence f1 * g = f2 * g by A5, A4, FUNCT_1:2; ::_thesis: verum
end;
theorem :: PARTFUN1:80
for Y, x, X being set
for f being b1 -valued Function st x in dom (f | X) holds
(f | X) /. x = f /. x
proof
let Y, x, X be set ; ::_thesis: for f being Y -valued Function st x in dom (f | X) holds
(f | X) /. x = f /. x
let f be Y -valued Function; ::_thesis: ( x in dom (f | X) implies (f | X) /. x = f /. x )
assume A1: x in dom (f | X) ; ::_thesis: (f | X) /. x = 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 ; ::_thesis: verum
end;