environ
vocabularies ENUMSET, RELATION, RELAT_AB, FUNCT;
notations ENUMSET, RELATION, RELAT_AB;
constructors ENUMSET, RELATION, RELAT_AB;
theorems ENUMSET, RELATION, RELAT_AB;
definitions ENUMSET, RELATION, RELAT_AB;
begin
reserve A,B,X,Y,Z,V,a,b,c,d,e,x,y,z for set, P,Q,R for Relation,
S for Relation of A,A;
definition
let R be set;
attr R is Function-like means :Def1:
for x,y,z holds [x,y] in R & [x,z] in R implies y=z;
end;
definition
let X,Y be set;
let R be Relation of X,Y;
attr R is onto means :Def2: rng R = Y;
end;
definition
let X,Y be set;
let R be Relation of X,Y;
attr R is total means :Def3: dom R = X;
end;
registration
cluster non empty for set;
existence
proof
take {1};
1 in {1} by ENUMSET:def 3;
then {1} <> {} by ENUMSET:def 1;
hence {1} is non empty by ENUMSET:def 2;
end;
end;
registration
let X be set, Y be non empty set;
cluster Function-like total for Relation of X,Y;
existence
proof
Y <> {} by ENUMSET:def 2; then
consider y such that
y: y in Y by ENUMSET:def 1;
set f=[:X,{y}:];
now
let a be set;
assume a in rng f;
then consider b such that
b: [b,a] in f by RELAT_AB:def 2;
consider b1,a1 being set such that
b1: b1 in X & a1 in {y} & [b,a]=[b1,a1] by RELAT_AB:def 7,b;
a in {y} by b1,ENUMSET:2;
then a = y by ENUMSET:def 3;
hence a in Y by y;
end; then
dom f c= X & rng f c= Y by RELAT_AB:def 5,ENUMSET:def 10; then
reconsider f as Relation of X,Y by RELAT_AB:def 5;
take f;
thus f is Function-like
proof
let a,b,c;
assume that
a: [a,b] in f and
b: [a,c] in f;
consider a1,b1 being set such that
b1: a1 in X & b1 in {y} & [a,b]=[a1,b1] by RELAT_AB:def 7,a;
consider a2,c1 being set such that
c1: a2 in X & c1 in {y} & [a,c]=[a2,c1] by RELAT_AB:def 7,b;
a=a1 & b=b1 & a=a2 & c =c1 by ENUMSET:2,b1,c1;
then b =y & c =y by b1,c1,ENUMSET:def 3;
hence b=c;
end;
thus f is total
proof
thus dom f = X
proof
thus dom f c= X by RELAT_AB:def 5;
thus X c= dom f
proof
let a be set;
assume a: a in X;
y in {y} by ENUMSET:def 3;
then [a,y] in f by y,RELAT_AB:def 7,a;
hence a in dom f by RELAT_AB:def 1;
end;
end;
end;
end;
end;
definition
let X be set, Y be non empty set;
mode Function of X,Y is Function-like total Relation of X,Y;
end;
definition
let Y be non empty set;
mode Element of Y -> set means :Def4: it in Y;
existence
proof
Y <> {} by ENUMSET:def 2; then
consider y such that
y: y in Y by ENUMSET:def 1;
take y;
thus thesis by y;
end;
end;
definition
let X,Y be non empty set;
let f be Function of X,Y;
let x be Element of X;
func f.x -> Element of Y means :Def5:
[x,it] in f;
existence
proof
x in X by Def4;then
x in dom f by Def3; then
consider y such that
y: [x,y] in f by RELAT_AB:def 1;
a: y in rng f by y,RELAT_AB:def 2;
rng f c= Y by RELAT_AB:def 5;
then y in Y by a,ENUMSET:def 10;
then reconsider y as Element of Y by Def4;
take y;
thus [x,y] in f by y;
end;
uniqueness by Def1;
end;
definition
let X,Y be non empty set;
let f be Function of X,Y;
attr f is one-to-one means :Def6:
for x1,x2 being Element of X st f.x1 = f.x2 holds x1 = x2;
end;
for f,g being Relation
st f is Function-like & g is Function-like
holds f*g is Function-like
proof
let f,g be Relation;
assume fg: f is Function-like & g is Function-like;
thus f * g is Function-like
proof
let x,y,z;
assume [x,y] in f*g;
then consider a such that
a: [x,a] in f & [a,y] in g by RELATION:def 7;
assume [x,z] in f*g;
then consider b such that
b: [x,b] in f & [b,z] in g by RELATION:def 7;
a=b by a,b,fg,Def1;
hence y=z by a,b,fg,Def1;
end;
end;
for X,Y being non empty set
for f being Function of X,Y holds
f is one-to-one implies f~ is Function-like
proof
let X,Y be non empty set;
let f be Function of X,Y;
assume f: f is one-to-one;
thus f~ is Function-like
proof
let x,y,z be set;
assume [x,y] in f~ & [x,z] in f~;
then yz: [y,x] in f & [z,x] in f by RELATION:def 3;
then dd: y in dom f & z in dom f & x in rng f by RELAT_AB:def 1, def 2;
then y in X & z in X by Def3;
then reconsider y1=y,z1=z as Element of X by Def4;
rng f c= Y by RELAT_AB:def 5;
then x in Y by dd,ENUMSET:def 10;
then reconsider x1=x as Element of Y by Def4;
x1=f.y1 & x1=f.z1 by yz,Def5;
hence y=z by f,Def6;
end;
end;
definition
let X,Y,Z be non empty set;
let g be Function of X,Y;
let f be Function of Y,Z;
redefine func g*f -> Function of X,Z;
coherence
proof
f: g*f is Function-like
proof
let a,b,c be set;
assume [a,b] in g*f;
then consider d1 being set such that
d1: [a,d1] in g & [d1,b] in f by RELATION:def 7;
assume [a,c] in g*f;
then consider d2 being set such that
d2: [a,d2] in g & [d2,c] in f by RELATION:def 7;
d1=d2 by d1,d2,Def1;
hence b=c by d1,d2,Def1;
end;
d: dom (g*f) c= X
proof
let a be set;
assume a in dom (g*f);
then consider b such that
b: [a,b] in g*f by RELAT_AB:def 1;
consider c such that
c: [a,c] in g & [c,b] in f by b,RELATION:def 7;
a in dom g & dom g c= X by c,RELAT_AB:def 1,def 5;
hence a in X by ENUMSET:def 10;
end;
rng (g*f) c= Z
proof
let a be set;
assume a in rng (g*f);
then consider b such that
b: [b,a] in g*f by RELAT_AB:def 2;
consider c such that
c: [b,c] in g & [c,a] in f by b,RELATION:def 7;
a in rng f & rng f c= Z by c,RELAT_AB:def 2,def 5;
hence a in Z by ENUMSET:def 10;
end;
then reconsider gf=g*f as Relation of X,Z by d,RELAT_AB:def 5;
dom (g*f)=X
proof
thus dom (g*f) c= X by d;
thus X c= dom(g*f)
proof
let x;
assume x in X;
then x in dom g by Def3;
then consider y such that
y: [x,y] in g by RELAT_AB:def 1;
y in rng g & rng g c= Y by y,RELAT_AB:def 2,def 5;
then y in Y by ENUMSET:def 10;
then y in dom f by Def3;
then consider z such that
z: [y,z] in f by RELAT_AB:def 1;
[x,z] in g*f by y,z,RELATION:def 7;
hence x in dom(g*f) by RELAT_AB:def 1;
end;
end;
then gf is total by Def2;
hence thesis by f;
end;
end;
for X,Y,Z being non empty set
for f being Function of X,Y
for g being Function of Y,Z
st f is one-to-one & g is one-to-one
for h being Function of X,Z st h=f*g holds h is one-to-one
proof
let X,Y,Z be non empty set;
let f be Function of X,Y;
let g be Function of Y,Z;
assume f: f is one-to-one;
assume g: g is one-to-one;
let h be Function of X,Z;
assume h: h=f*g;
thus h is one-to-one
proof
let a,b be Element of X;
assume hab: h.a = h.b;
[a,h.a] in f*g by h,Def5;
then consider x being set such that
x: [a,x] in f & [x,h.a] in g by RELATION:def 7;
[b,h.b] in f*g by h,Def5;
then consider y being set such that
y: [b,y] in f & [y,h.b] in g by RELATION:def 7;
[a,f.a] in f by Def5;
then fax: x=f.a by x,Def1;
[b,f.b] in f by Def5;
then fby: y=f.b by y,Def1;
[f.a,g.(f.a)] in g by Def5;
then
g1: g.(f.a) = h.a by fax,x,Def1;
[f.b,g.(f.b)] in g by Def5;
then
g2: g.(f.b) = h.b by fby,y,Def1;
g.(f.a)=g.(f.b) by hab,g1,g2;
then f.a=f.b by g,Def6;
hence a=b by f,Def6;
end;
end;