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;
:: for x1,x2 being Element of X st x1 <> x2 holds f.x1 = f.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;
::5.30
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;
::5.31
for X,Y,Z being non empty set
for f being Function of X,Y
for g being Function of Y,Z
for fg being Function of X,Y st fg=f*g & fg is one-to-one & f is onto
holds g 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;
let fg be Function of X,Y such that
fg: fg=f*g and o: fg is one-to-one and f: f is onto;
thus g is one-to-one
proof
let a,b be Element of Y;
now
assume ab: a <> b;
a in Y by Def4;
then a in rng f by f;
then consider c being set such that
c: [c,a] in f by RELAT_AB:def 2;
c in dom f by c,RELAT_AB:def 1;
then c in X by Def3;
then reconsider c as Element of X by Def4;
b in Y by Def4;
then b in rng f by f;
then consider d being set such that
d: [d,b] in f by RELAT_AB:def 2;
d in dom f by d,RELAT_AB:def 1;
then d in X by Def3;
then reconsider d as Element of X by Def4;
c <> d by ab,c,d,Def1;
then
r: fg.c <> fg.d by o;
[a,g.a] in g by Def5;
then cg: [c,g.a] in fg & [c,fg.c] in fg by c,fg,RELATION:def 7,Def5;
then cc: g.a=fg.c by Def1;
[b,g.b] in g by Def5;
then dg: [d,g.b] in fg & [d,fg.d] in fg by d,fg,RELATION:def 7,Def5;
then dd: g.b=fg.d by Def1;
thus g.a <> g.b by cc,dd,r;
end;
hence thesis;
end;
end;
:: 5.25
for X being non empty set
for f,g being Function of X,X st f is one-to-one & g*f=f holds
g = id X
proof
let X be non empty set;
let f,g be Function of X,X;
assume that f: f is one-to-one and g: g*f=f;
thus g = id X
proof
thus g c= id X
proof
let a,b;
assume ab: [a,b] in g;
then br: b in rng g by RELAT_AB:def 2;
rng g c= X by RELAT_AB:def 5;
then bx: b in X by br,ENUMSET:def 10;
then b in dom f by Def3;
then consider c such that
c: [b,c] in f by RELAT_AB:def 1;
[a,c] in g*f by ab,c,RELATION:def 7;
then af: [a,c] in f by g;
then a in dom f by RELAT_AB:def 1;
then ax: a in X by Def3;
reconsider B=b as Element of X by bx,Def4;
reconsider A=a as Element of X by ax,Def4;
[A,f.A] in f & [B,f.B] in f by Def5;
then c = f.A & c = f.B by c,af,Def1;
then a=b by f;
hence [a,b] in id X by ax,RELAT_AB:def 6;
end;
thus id X c= g
proof
let a,b;
assume [a,b] in id X;
then ab: a in X & a=b by RELAT_AB:def 6;
then reconsider A=a as Element of X by Def4;
[A,g.A] in g & [g.A,f.(g.A)] in f by Def5;
then [A,f.(g.A)] in g*f by RELATION:def 7;
then [A,f.(g.A)] in f & [A,f.A] in f by g,Def5;
then f.(g.A)=f.A by Def1;
then A=g.A by f;
hence [a,b] in g by Def5,ab;
end;
end;
end;
:: 5.26
for X being non empty set
for f,g being Function of X,X st f is onto & f*g=f holds
g = id X
proof
let X be non empty set;
let f,g be Function of X,X such that
f: f is onto and g: f*g=f;
thus g = id X
proof
thus g c= id X
proof
let a,b be set;
assume ab: [a,b] in g;
then a in dom g & dom g c= X by RELAT_AB:def 1,def 5;
then ax: a in X by ENUMSET:def 10;
then a in rng f by f;
then consider c being set such that
c: [c,a] in f by RELAT_AB:def 2;
[c,b] in f by ab,c,g,RELATION:def 7;
then a=b by c,Def1;
hence [a,b] in id X by ax,RELAT_AB:def 6;
end;
thus id X c= g
proof
let a,b be set;
assume [a,b] in id X;
then ab: a=b & a in X by RELAT_AB:def 6;
then a in rng f by f;
then consider c being set such that
c: [c,a] in f by RELAT_AB:def 2;
a in dom g by ab,Def3;
then consider d being set such that
d: [a,d] in g by RELAT_AB:def 1;
[c,d] in f by g,c,d,RELATION:def 7;
then a=d by c,Def1;
hence [a,b] in g by ab,d;
end;
end;
end;
:: 5.27
for X being non empty set
for f,g being Function of X,X st f*g=id X holds
f is one-to-one & g is onto
proof
let X be non empty set;
let f,g be Function of X,X such that f: f*g=id X;
thus f is one-to-one
proof
let a,b be Element of X;
now
assume ab: a<>b;
[a,f.a] in f & [f.a,g.(f.a)] in g &
[b,f.b] in f & [f.b,g.(f.b)] in g by Def5;
then [a,g.(f.a)] in id X & [b,g.(f.b)] in id X by f,RELATION:def 7;
then a=g.(f.a) & b=g.(f.b) by RELAT_AB:def 6;
hence f.a <> f.b by ab;
end;
hence thesis;
end;
thus g is onto
proof
thus rng g = X
proof
thus rng g c= X by RELAT_AB:def 5;
thus X c= rng g
proof
let a be set;
assume a in X;
then [a,a] in f*g by f,RELAT_AB:def 6;
then consider b being set such that
b: [a,b] in f & [b,a] in g by RELATION:def 7;
thus a in rng g by b,RELAT_AB:def 2;
end;
end;
end;
end;
:: 5.70
R.:(X\/Y) = (R.:X) \/ (R.:Y)
proof
thus R.:(X\/Y) c= (R.:X) \/ (R.:Y)
proof
let a be set;
assume a in R.:(X\/Y);
then consider b being set such that
b: [b,a] in R & b in X \/ Y by RELAT_AB:def 3;
b in X or b in Y by ENUMSET:def 6,b;
then a in (R.:X) or a in (R.:Y) by b,RELAT_AB:def 3;
hence a in (R.:X) \/ (R.:Y) by ENUMSET:def 6;
end;
thus (R.:X) \/ (R.:Y) c= R.:(X\/Y)
proof
let a be set;
assume a in (R.:X) \/ (R.:Y);
then per cases by ENUMSET:def 6;
suppose a in (R.:X);
then consider b being set such that
b: [b,a] in R & b in X by RELAT_AB:def 3;
b in X\/Y by b,ENUMSET:def 6;
hence a in R.:(X\/Y) by b,RELAT_AB:def 3;
end;
suppose a in (R.:Y);
then consider b being set such that
b: [b,a] in R & b in Y by RELAT_AB:def 3;
b in X\/Y by b,ENUMSET:def 6;
hence a in R.:(X\/Y) by b,RELAT_AB:def 3;
end;
end;
end;
:: 5.71
l571:
R.:(X/\Y) c= (R.:X) /\ (R.:Y)
proof
let a be set;
assume a in R.:(X/\Y);
then consider b being set such that
b: [b,a] in R & b in X/\Y by RELAT_AB:def 3;
b in X & b in Y by b,ENUMSET:def 7;
then a in (R.:X) & a in (R.:Y) by b,RELAT_AB:def 3;
hence a in (R.:X) /\ (R.:Y) by ENUMSET:def 7;
end;
for A,B being non empty set
for f being Function of A,B st f is one-to-one holds
f.:(X/\Y) = (f.:X) /\ (f.:Y)
proof
let A,B be non empty set;
let f be Function of A,B;
assume f: f is one-to-one;
thus f.:(X/\Y) = (f.:X) /\ (f.:Y)
proof
thus f.:(X/\Y) c= (f.:X) /\ (f.:Y) by l571;
thus (f.:X) /\ (f.:Y) c= f.:(X/\Y)
proof
let a;
assume a in (f.:X) /\ (f.:Y);
then a: a in (f.:X) & a in (f.:Y) by ENUMSET:def 7;
consider b1 being set such that
b1: [b1,a] in f & b1 in X by a,RELAT_AB:def 3;
consider b2 being set such that
b2: [b2,a] in f & b2 in Y by a,RELAT_AB:def 3;
b1d: b1 in dom f by b1,RELAT_AB:def 1;
dom f c= A by RELAT_AB:def 5;
then b1 in A by b1d,ENUMSET:def 10;
then reconsider B1=b1 as Element of A by Def4;
b2d: b2 in dom f by b2,RELAT_AB:def 1;
dom f c= A by RELAT_AB:def 5;
then b2 in A by b2d,ENUMSET:def 10;
then reconsider B2=b2 as Element of A by Def4;
[B1,f.B1] in f by Def5;
then
f.B1 = a by b1,Def1;
then f.B1 = f.B2 by b2,Def5;
then B1 = B2 by f;
then b1 in X/\Y by b1,b2,ENUMSET:def 7;
hence a in f.:(X/\Y) by b1,RELAT_AB:def 3;
end;
end;
end;
:: równoważność tego warunku i różnowartościowości funkcji
:: 5.72
l572:
(R.:X) \ (R.:Y) c= R.:(X\Y)
proof
let a be set;
assume a in (R.:X) \ (R.:Y);
then a: a in (R.:X) & not a in (R.:Y) by ENUMSET:def 8;
then consider b being set such that
b: [b,a] in R & b in X by RELAT_AB:def 3;
not b in Y by b,a,RELAT_AB:def 3;
then b in X\Y by b,ENUMSET:def 8;
hence a in R.:(X\Y) by b,RELAT_AB:def 3;
end;
for A,B being non empty set
for f being Function of A,B st f is one-to-one holds
(f.:X) \ (f.:Y) = f.:(X\Y)
proof
let A,B be non empty set;
let f be Function of A,B such that
f: f is one-to-one;
thus (f.:X) \ (f.:Y) c= f.:(X\Y) by l572;
thus f.:(X\Y) c= (f.:X) \ (f.:Y)
proof
let a be set;
assume a in f.:(X\Y);
then consider b being set such that
b: [b,a] in f & b in X\Y by RELAT_AB:def 3;
a in rng f & rng f c= B by b,RELAT_AB:def 2,RELAT_AB:def 5;
then a in B by ENUMSET:def 10;
then reconsider a1=a as Element of B by Def4;
b in dom f & dom f c= A by b,RELAT_AB:def 1,RELAT_AB:def 5;
then b in A by ENUMSET:def 10;
then reconsider b as Element of A by Def4;
bx: b in X by b,ENUMSET:def 8;
a1: a in f.:X by bx,b,RELAT_AB:def 3;
nb: not b in Y by b,ENUMSET:def 8;
now
assume a in f.:Y;
then consider c being set such that
c: [c,a] in f & c in Y by RELAT_AB:def 3;
c in dom f & dom f c= A by c,RELAT_AB:def 1,RELAT_AB:def 5;
then c in A by ENUMSET:def 10;
then reconsider c as Element of A by Def4;
f.b = a1 & a1 = f.c by b,c,Def5;
hence contradiction by c,f,nb;
end;
hence a in (f.:X) \ (f.:Y) by a1,ENUMSET:def 8;
end;
end;
:: rownoważność tego warunku i różnowartościowości funkcji
::5.73
X c= Y implies R.:X c= R.:Y
proof
assume z: X c= Y;
let a;
assume a in R.:X;
then consider b such that
b: [b,a] in R & b in X by RELAT_AB:def 3;
b in Y by b,z,ENUMSET:def 10;
hence a in R.:Y by b,RELAT_AB:def 3;
end;
::5.74
for A being set st A c= dom R holds
A c= R"(R.:A)
proof
let A be set;
assume a: A c= dom R;
let x;
assume xa: x in A;
then x in dom R by a,ENUMSET:def 10;
then consider y such that
y: [x,y] in R by RELAT_AB:def 1;
y in R.:A by y,xa,RELAT_AB:def 3;
hence x in R"(R.:A) by y,RELAT_AB:def 4;
end;
:: 5.75
R"(X\/Y) = (R"X) \/ (R"Y)
proof
thus R"(X\/Y) c= (R"X) \/ (R"Y)
proof
let a;
assume a in R"(X\/Y);
then consider b such that
b: [a,b] in R & b in X \/ Y by RELAT_AB:def 4;
b in X or b in Y by ENUMSET:def 6,b;
then a in R"X or a in R"Y by b,RELAT_AB:def 4;
hence a in (R"X) \/ (R"Y) by ENUMSET:def 6;
end;
thus (R"X) \/ (R"Y) c= R"(X\/Y)
proof
let a;
assume a in (R"X) \/ (R"Y);
then a in R"X or a in R"Y by ENUMSET:def 6;
then per cases;
suppose a in R"X;
then consider b such that
b: [a,b] in R & b in X by RELAT_AB:def 4;
b in X \/ Y by b,ENUMSET:def 6;
hence a in R"(X\/Y) by b,RELAT_AB:def 4;
end;
suppose a in R"Y;
then consider b such that
b: [a,b] in R & b in Y by RELAT_AB:def 4;
b in X \/ Y by b,ENUMSET:def 6;
hence a in R"(X\/Y) by b,RELAT_AB:def 4;
end;
end;
end;
:: 5.76
l576:
R"(X/\Y) c= (R"X) /\ (R"Y)
proof
let a be set;
assume a in R"(X/\Y);
then consider b being set such that
b: [a,b] in R & b in X/\Y by RELAT_AB:def 4;
b in X & b in Y by b,ENUMSET:def 7;
then a in (R"X) & a in (R"Y) by b,RELAT_AB:def 4;
hence a in (R"X) /\ (R"Y) by ENUMSET:def 7;
end;
for f being Relation st f is Function-like holds
f"(X/\Y) = (f"X) /\ (f"Y)
proof
let f be Relation such that
f: f is Function-like;
thus f"(X/\Y) c= (f"X) /\ (f"Y) by l576;
thus (f"X) /\ (f"Y) c= f"(X/\Y)
proof
let a be set;
assume a in (f"X) /\ (f"Y);
then aa: a in f"X & a in f"Y by ENUMSET:def 7;
consider b being set such that
b: [a,b] in f & b in X by aa,RELAT_AB:def 4;
consider c being set such that
c: [a,c] in f & c in Y by aa,RELAT_AB:def 4;
b=c by f,b,c;
then b in X /\ Y by b,c,ENUMSET:def 7;
hence a in f"(X/\Y) by b,RELAT_AB:def 4;
end;
end;
:: 5:77
l577:
(R"X) \ (R"Y) c= R"(X\Y)
proof
let a be set;
assume a in (R"X) \ (R"Y);
then aa: a in R"X & not a in R"Y by ENUMSET:def 8;
then consider b being set such that
b: [a,b] in R & b in X by RELAT_AB:def 4;
not b in Y by aa,b,RELAT_AB:def 4;
then b in X\Y by b,ENUMSET:def 8;
hence a in R"(X\Y) by b,RELAT_AB:def 4;
end;
for f being Relation st f is Function-like holds
(f"X) \ (f"Y) = f"(X\Y)
proof
let f be Relation such that
f: f is Function-like;
thus (f"X) \ (f"Y) c= f"(X\Y) by l577;
thus f"(X\Y) c= (f"X) \ (f"Y)
proof
let a be set;
assume a in f"(X\Y);
then consider b being set such that
b: [a,b] in f & b in X\Y by RELAT_AB:def 4;
b in X by b,ENUMSET:def 8;
then a1: a in f"X by b,RELAT_AB:def 4;
now
assume a in f"Y;
then consider c being set such that
c: [a,c] in f & c in Y by RELAT_AB:def 4;
b=c by b,c,f;
hence contradiction by b,c,ENUMSET:def 8;
end;
hence a in (f"X) \ (f"Y) by a1,ENUMSET:def 8;
end;
end;
::5:78
X c= Y implies R"X c= R"Y
proof
assume z: X c= Y;
let a;
assume a in R"X;
then consider b such that
b: [a,b] in R & b in X by RELAT_AB:def 4;
b in Y by b,z,ENUMSET:def 10;
hence a in R"Y by b,RELAT_AB:def 4;
end;