Copyright (c) 1992 Association of Mizar Users
environ
vocabulary BOOLE, TARSKI, CLASSES1, TOLER_1, FUNCT_2, FRAENKEL, FUNCT_1,
MCART_1, RELAT_1, CAT_1, ENS_1, PARTFUN1, COH_SP;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELSET_1, MCART_1,
FUNCT_1, PARTFUN1, CLASSES1, FUNCT_2, FRAENKEL, EQREL_1, TOLER_1, CAT_1;
constructors EQREL_1, MCART_1, CLASSES1, TOLER_1, FRAENKEL, CAT_1, PARTFUN1,
MEMBERED, FUNCT_2, XBOOLE_0, RELSET_1;
clusters FUNCT_1, RELSET_1, SUBSET_1, FRAENKEL, MEMBERED, ZFMISC_1, PARTFUN1,
FUNCT_2, XBOOLE_0, EQREL_1, TOLER_1;
requirements SUBSET, BOOLE;
definitions TARSKI, CLASSES1, XBOOLE_0;
theorems TARSKI, ZFMISC_1, TOLER_1, ENUMSET1, RELAT_1, FUNCT_2, CLASSES1,
PARTFUN1, FRAENKEL, MCART_1, FUNCT_1, DOMAIN_1, CAT_1, RELSET_1,
XBOOLE_0, XBOOLE_1, EQREL_1;
schemes TOLER_1, TARSKI, FUNCT_2, PARTFUN1, XBOOLE_0;
begin
reserve x,y,z,a,b,c,X,A for set;
:: Coherent Space and Web of Coherent Space
definition let IT be set;
canceled;
attr IT is binary_complete means :Def2:
for A st A c= IT & (for a,b st a in A & b in A holds a \/ b in IT) holds
union A in IT;
end;
definition
cluster subset-closed binary_complete non empty set;
existence
proof
take X={{}};
thus for a,b st a in X & b c= a holds b in X
proof let a,b; assume
A1: a in X & b c= a;
then a = {} by TARSKI:def 1;
hence b in X by A1,XBOOLE_1:3;
end;
thus for A st A c= X &
(for a,b st a in A & b in A holds a \/ b in X) holds union A in X
proof let A such that
A2: A c= X & for a,b st a in A & b in A holds a \/ b in X;
now per cases by A2,ZFMISC_1:39;
suppose A = {};
hence union A in X by TARSKI:def 1,ZFMISC_1:2;
suppose A = {{}}; then union A = {} by ZFMISC_1:31;
hence union A in X by TARSKI:def 1;
end;
hence thesis;
end;
thus thesis;
end;
end;
definition
mode Coherence_Space is subset-closed binary_complete non empty set;
end;
reserve C,D for Coherence_Space;
theorem
{} in C
proof A1: {} c= C by XBOOLE_1:2;
for a,b st a in {} & b in {} holds a \/ b in C;
hence thesis by A1,Def2,ZFMISC_1:2;
end;
theorem Th2:
bool X is Coherence_Space
proof
A1: for a, b st a in bool X & b c= a holds b in bool X
proof let a,b; assume a in bool X & b c= a;
then b c= X by XBOOLE_1:1; hence thesis;
end;
for A st A c= bool X &
(for a,b st a in A & b in A holds a \/ b in bool X) holds union A in bool X
proof let A; assume that
A2: A c= bool X and
for a,b st a in A & b in A holds a \/ b in bool X;
for a st a in A holds a c= X by A2;
then union A c= X by ZFMISC_1:94;
hence thesis;
end;
hence thesis by A1,Def2,CLASSES1:def 1;
end;
theorem
{{}} is Coherence_Space by Th2,ZFMISC_1:1;
theorem Th4:
x in union C implies {x} in C
proof assume x in union C; then consider X such that
A1: x in X & X in C by TARSKI:def 4;
{x} c= X by A1,ZFMISC_1:37;
hence thesis by A1,CLASSES1:def 1;
end;
definition let C be Coherence_Space;
func Web(C) -> Tolerance of union C means :Def3:
for x,y holds [x,y] in it iff ex X st X in C & x in X & y in X;
existence
proof
defpred P[set,set] means ex X st X in C & $1 in X & $2 in X;
A1: for x st x in union C holds P[x,x]
proof let x such that A2: x in union C;
take {x};
thus thesis by A2,Th4,TARSKI:def 1;
end;
A3: for x,y st x in union C & y in union C & P[x,y] holds P[y,x];
consider T be Tolerance of union C such that
A4: for x,y st x in union C & y in union C holds
[x,y] in T iff P[x,y] from ToleranceEx(A1,A3);
take T;
let x,y;
thus [x,y] in T implies ex X st X in C & x in X & y in X
proof assume A5: [x,y] in T; then x in union C & y in union C by ZFMISC_1:
106;
hence thesis by A4,A5;
end;
given X such that A6: X in C & x in X & y in X;
A7: x in union C by A6,TARSKI:def 4;
y in union C by A6,TARSKI:def 4;
hence thesis by A4,A6,A7;
end;
uniqueness by TOLER_1:52;
end;
reserve T for Tolerance of union C;
theorem Th5:
T = Web(C) iff for x,y holds [x,y] in T iff {x,y} in C
proof
thus T = Web(C) implies for x,y holds [x,y] in T iff {x,y} in C
proof assume A1: T = Web(C);
let x,y;
thus [x,y] in T implies {x,y} in C
proof assume [x,y] in T; then consider X such that
A2: X in C & x in X & y in X by A1,Def3;
{x,y} c= X by A2,ZFMISC_1:38;
hence thesis by A2,CLASSES1:def 1;
end;
assume A3: {x,y} in C;
x in {x,y} & y in {x,y} by TARSKI:def 2;
hence thesis by A1,A3,Def3;
end;
assume A4: for x,y holds [x,y] in T iff {x,y} in C;
for x,y holds
[x,y] in T iff ex X st X in C & x in X & y in X
proof let x,y;
thus [x,y] in T implies ex X st X in C & x in X & y in X
proof
assume A5: [x,y] in T;
take {x,y};
thus thesis by A4,A5,TARSKI:def 2;
end;
given X such that A6: X in C & x in X & y in X;
{x,y} c= X by A6,ZFMISC_1:38;
then {x,y} in C by A6,CLASSES1:def 1;
hence thesis by A4;
end;
hence thesis by Def3;
end;
theorem Th6:
a in C iff for x,y st x in a & y in a holds {x,y} in C
proof
thus a in C implies for x,y st x in a & y in a holds {x,y} in C
proof assume A1: a in C;
let x,y;
assume x in a & y in a;
then {x,y} c= a by ZFMISC_1:38;
hence thesis by A1,CLASSES1:def 1;
end;
assume A2: for x,y st x in a & y in a holds {x,y} in C;
defpred P[set,set] means {$1} = $2;
A3: for x,y,z st P[x,y] & P[x,z] holds y = z;
consider X such that
A4: for x holds x in X iff ex y st y in a & P[y,x] from Fraenkel(A3);
A5: X c= C
proof let x; assume x in X; then consider y such that
A6: y in a & {y} = x by A4;
{y,y} in C by A2,A6;
hence thesis by A6,ENUMSET1:69;
end;
A7: for b,c st b in X & c in X holds b \/ c in C
proof let b,c; assume A8: b in X & c in X;
then consider y such that A9: y in a & {y} = b by A4;
consider z such that A10: z in a & {z} = c by A4,A8;
{y,z} in C by A2,A9,A10;
hence thesis by A9,A10,ENUMSET1:41;
end;
union X = a
proof
thus union X c= a
proof let x; assume x in union X; then consider Z be set such that
A11: x in Z & Z in X by TARSKI:def 4;
consider y such that A12: y in a & Z = {y} by A4,A11;
thus thesis by A11,A12,TARSKI:def 1;
end;
let x; assume x in a; then A13: {x} in X by A4;
x in {x} by TARSKI:def 1;
hence thesis by A13,TARSKI:def 4;
end;
hence a in C by A5,A7,Def2;
end;
theorem Th7:
a in C iff for x,y st x in a & y in a holds [x,y] in Web(C)
proof
thus a in C implies for x,y st x in a & y in a holds [x,y] in Web(C)
proof assume A1: a in C;
let x,y; assume x in a & y in a;
then {x,y} in C by A1,Th6;
hence thesis by Th5;
end;
assume A2: for x,y st x in a & y in a holds [x,y] in Web(C);
now let x,y; assume x in a & y in a; then [x,y] in Web(C) by A2;
hence {x,y} in C by Th5;
end;
hence thesis by Th6;
end;
theorem
(for x,y st x in a & y in a holds {x,y} in C) implies a c= union C
proof assume
A1: for x,y st x in a & y in a holds {x,y} in C;
let x; assume x in a;
then {x,x} in C by A1;
then A2: {x} in C by ENUMSET1:69;
x in {x} by TARSKI:def 1;
hence thesis by A2,TARSKI:def 4;
end;
theorem
Web(C) = Web(D) implies C = D
proof assume A1: Web(C) = Web(D);
thus C c= D
proof
let x; assume x in C;
then for z,y st z in x & y in x holds [z,y] in Web(D) by A1,Th7;
hence x in D by Th7;
end;
let x; assume x in D;
then for z,y st z in x & y in x holds [z,y] in Web(C) by A1,Th7;
hence x in C by Th7;
end;
theorem
union C in C implies C = bool union C
proof assume A1: union C in C;
thus C c= bool union C by ZFMISC_1:100;
let x; assume x in bool union C;
hence thesis by A1,CLASSES1:def 1;
end;
theorem
C = bool union C implies Web(C) = Total union C
proof assume
A1: C = bool union C;
reconsider t = Total union C as Tolerance of union C;
now let x,y;
thus [x,y] in t implies {x,y} in C
proof assume
[x,y] in t;
then A2: x in union C & y in union C by ZFMISC_1:106;
{x,y} c= union C
proof let z; assume z in {x,y};
hence thesis by A2,TARSKI:def 2;
end;
hence thesis by A1;
end;
assume {x,y} in C;
then x in union C & y in union C by A1,ZFMISC_1:38;
hence [x,y] in t by TOLER_1:15;
end;
hence thesis by Th5;
end;
definition let X be set; let E be Tolerance of X;
func CohSp(E) -> Coherence_Space means :Def4:
for a holds a in it iff for x,y st x in a & y in a holds [x,y] in E;
existence
proof
defpred P[set] means for x,y st x in $1 & y in $1 holds [x,y] in E;
consider Z be set such that
A1: for x holds x in Z iff x in bool X & P[x] from Separation;
A2: for a,b st a in Z & b c= a holds b in Z
proof let a,b; assume
A3: a in Z & b c= a;
then a in bool X by A1; then A4: b c= X by A3,XBOOLE_1:1;
for x,y st x in b & y in b holds [x,y] in E by A1,A3;
hence b in Z by A1,A4;
end;
A5: for A st A c= Z &
(for a,b st a in A & b in A holds a \/ b in Z) holds union A in Z
proof let A such that
A6: A c= Z & for a,b st a in A & b in A holds a \/ b in Z;
now let a; assume a in A;
then a in bool X by A1,A6;
hence a c= X;
end; then A7: union A c= X by ZFMISC_1:94;
now let x,y; assume A8: x in union A & y in union A;
then consider X1 be set such that A9: x in X1 & X1 in A by TARSKI:def 4;
consider Y1 be set such that A10: y in Y1 & Y1 in A by A8,TARSKI:def 4;
A11: X1 \/ Y1 in Z by A6,A9,A10;
A12: x in X1 \/ Y1 by A9,XBOOLE_0:def 2;
y in X1 \/ Y1 by A10,XBOOLE_0:def 2;
hence [x,y] in E by A1,A11,A12;
end;
hence thesis by A1,A7;
end;
A13: P[{}];
{} c= X by XBOOLE_1:2;
then reconsider Z as Coherence_Space by A1,A2,A5,A13,Def2,CLASSES1:def 1;
take Z;
let a;
thus a in Z implies for x,y st x in a & y in a holds [x,y] in E by A1;
assume A14: for x,y st x in a & y in a holds [x,y] in E;
then a is TolSet of E by TOLER_1:def 3;
then a c= X by TOLER_1:43;
hence thesis by A1,A14;
end;
uniqueness
proof let C,D; assume that
A15: for a holds a in C iff for x,y st x in a & y in a holds [x,y] in E and
A16: for a holds a in D iff for x,y st x in a & y in a holds [x,y] in E;
thus C c= D
proof let x; assume x in C;
then for z,y st z in x & y in x holds [z,y] in E by A15;
hence thesis by A16;
end;
let x; assume x in D;
then for z,y st z in x & y in x holds [z,y] in E by A16;
hence thesis by A15;
end;
end;
reserve E for Tolerance of X;
theorem
Web(CohSp(E)) = E
proof
now let x,y;
thus [x,y] in Web(CohSp(E)) implies [x,y] in E
proof
assume [x,y] in Web(CohSp(E)); then A1: {x,y} in CohSp(E) by Th5;
x in {x,y} & y in {x,y} by TARSKI:def 2;
hence thesis by A1,Def4;
end;
assume A2: [x,y] in E; then A3: x in X & y in X by ZFMISC_1:106;
for u,v be set st u in {x,y} & v in {x,y} holds [u,v] in E
proof let u,v be set; assume u in {x,y} & v in {x,y};
then (u = x or u = y) & (v = x or v = y) by TARSKI:def 2;
hence [u,v] in E by A2,A3,TOLER_1:27, EQREL_1:12;
end;
then {x,y} in CohSp(E) by Def4;
hence [x,y] in Web(CohSp(E)) by Th5;
end;
hence thesis by RELAT_1:def 2;
end;
theorem
CohSp(Web(C)) = C
proof
thus CohSp(Web(C)) c= C
proof let x; assume x in CohSp(Web(C));
then for y,z st y in x & z in x holds [y,z] in Web(C) by Def4;
hence thesis by Th7;
end;
let x; assume x in C;
then for y,z st y in x & z in x holds [y,z] in Web(C) by Th7;
hence x in CohSp(Web(C)) by Def4;
end;
theorem Th14:
a in CohSp(E) iff a is TolSet of E
proof
thus a in CohSp(E) implies a is TolSet of E
proof assume a in CohSp(E);
then for x,y st x in a & y in a holds [x,y] in E by Def4;
hence thesis by TOLER_1:def 3;
end;
assume a is TolSet of E;
then for x,y st x in a & y in a holds [x,y] in E by TOLER_1:def 3;
hence thesis by Def4;
end;
theorem
CohSp(E) = TolSets E
proof
thus CohSp(E) c= TolSets E
proof let x; assume x in CohSp(E);
then x is TolSet of E by Th14;
hence thesis by TOLER_1:def 6;
end;
let x; assume x in TolSets E;
then x is TolSet of E by TOLER_1:def 6;
hence thesis by Th14;
end;
begin :: Category of Coherence Spaces
definition let X;
func CSp(X) -> set equals :Def5:
{ x where x is Subset of bool X : x is Coherence_Space };
coherence;
end;
definition let X;
cluster CSp(X) -> non empty;
coherence
proof
set F = { x where x is Element of bool bool X: x is Coherence_Space };
reconsider b = bool X as Element of bool bool X by ZFMISC_1:def 1;
b is Coherence_Space by Th2;
then b in F;
hence thesis by Def5;
end;
end;
definition let X be set;
cluster -> subset-closed binary_complete non empty Element of CSp(X);
coherence
proof let C be Element of CSp(X);
C in CSp(X);
then C in { x where x is Element of bool bool X : x is Coherence_Space }
by Def5; then consider x be Element of bool bool X such that
A1: C = x & x is Coherence_Space;
thus thesis by A1;
end;
end;
reserve C,C1,C2 for Element of CSp(X);
theorem Th16:
{x,y} in C implies x in union C & y in union C
proof assume A1: {x,y} in C;
{x} c= {x,y} & {y} c= {x,y} by ZFMISC_1:12;
then x in {x} & {x} in C & y in {y} & {y} in C by A1,CLASSES1:def 1,TARSKI:
def 1;
hence thesis by TARSKI:def 4;
end;
definition let X;
canceled;
func FuncsC(X) -> set equals :Def7:
union { Funcs(union x,union y) where x is Element of CSp(X),
y is Element of CSp(X): not contradiction };
coherence;
end;
definition let X;
cluster FuncsC(X) -> non empty functional;
coherence
proof set F = { Funcs(union T,union TT) where T is Element of CSp(X),
TT is Element of CSp(X): not contradiction };
A1: FuncsC X = union F by Def7;
reconsider A = bool X as Element of bool bool X by ZFMISC_1:def 1;
A is Coherence_Space by Th2;
then A in { x where x is Element of bool bool X: x is Coherence_Space};
then reconsider A as Element of CSp(X) by Def5;
id union A in Funcs(union A,union A) & Funcs(union A,union A) in F
by FUNCT_2:12;
then reconsider UF = union F as non empty set by TARSKI:def 4;
now let f be set;
assume f in UF;
then consider C being set such that
A2: f in C and
A3: C in F by TARSKI:def 4;
ex A,B be Element of CSp(X) st C = Funcs(union A,union B) by A3;
hence f is Function by A2,FUNCT_2:121;
end; hence thesis by A1,FRAENKEL:def 1;
end;
end;
reserve g for Element of FuncsC(X);
theorem Th17:
x in FuncsC(X) iff
ex C1,C2 st (union C2 = {} implies union C1 = {}) &
x is Function of union C1,union C2
proof
set F = { Funcs(union xx,union y) where xx is Element of CSp(X),
y is Element of CSp(X): not contradiction };
A1: FuncsC(X) = union F by Def7;
thus x in FuncsC(X) implies
ex C1,C2 st (union C2 = {} implies union C1 = {}) &
x is Function of union C1,union C2
proof assume x in FuncsC(X);
then consider C being set such that
A2: x in C and
A3: C in F by A1,TARSKI:def 4;
consider A,B be Element of CSp(X) such that
A4: C = Funcs(union A,union B) by A3;
take A,B;
thus thesis by A2,A4,FUNCT_2:14,121;
end;
given A,B be Element of CSp(X) such that
A5: (union B={} implies union A={}) & x is Function of union A,union B;
x in Funcs(union A,union B) & Funcs(union A,union B) in F by A5,FUNCT_2:11;
hence thesis by A1,TARSKI:def 4;
end;
definition let X;
func MapsC(X) -> set equals :Def8:
{ [[C,CC],f] where C is Element of CSp(X), CC is Element of CSp(X),
f is Element of FuncsC(X) :
(union CC = {} implies union C = {}
) & f is Function of union C,union CC &
for x,y st {x,y} in C holds {f.x,f.y} in CC};
coherence;
end;
definition let X;
cluster MapsC(X) -> non empty;
coherence
proof
set FV = { [[T,TT],f] where T is Element of CSp(X), TT is Element of CSp(X),
f is Element of FuncsC(X) :
(union TT = {} implies union T = {}
) & f is Function of union T,union TT &
for x,y st {x,y} in T holds {f.x,f.y} in TT};
now
reconsider A = bool X as Element of bool bool X by ZFMISC_1:def 1;
A is Coherence_Space by Th2;
then A in { xx where xx is Element of bool bool X: xx is Coherence_Space};
then reconsider A as Element of CSp(X) by Def5;
set f = id union A;
take m = [[A,A],f];
A1: union A = {} implies union A = {};
then reconsider f as Element of FuncsC(X) by Th17;
now let x,y; assume A2: {x,y} in A;
then x in union A & y in union A by Th16;
then f.x = x & f.y = y by FUNCT_1:35;
hence {f.x,f.y} in A by A2;
end;
hence m in FV by A1;
end;
hence thesis by Def8;
end;
end;
reserve l,l1,l2,l3 for Element of MapsC(X);
theorem Th18:
ex g,C1,C2 st l = [[C1,C2],g] & (union C2 = {} implies union C1 = {}) &
g is Function of union C1,union C2 &
for x,y st {x,y} in C1 holds {g.x,g.y} in C2
proof l in MapsC(X);
then l in {[[C1,C2],g]: (union C2={} implies union C1={}) &
g is Function of union C1,union C2 &
for x,y st {x,y} in C1 holds {g.x,g.y} in C2} by Def8;
then ex C1,C2,g st l = [[C1,C2],g] & (union C2={} implies union C1={}) &
g is Function of union C1,union C2 &
for x,y st {x,y} in C1 holds {g.x,g.y} in C2;
hence thesis;
end;
theorem Th19:
for f being Function of union C1,union C2 st (union C2={} implies union C1={}
) &
(for x,y st {x,y} in C1 holds {f.x,f.y} in C2) holds [[C1,C2],f] in MapsC(X)
proof let f be Function of union C1,union C2; assume
A1: (union C2={} implies union C1={}) &
for x,y st {x,y} in C1 holds {f.x,f.y} in C2;
then reconsider f' = f as Element of FuncsC(X) by Th17;
for x,y st {x,y} in C1 holds {f'.x,f'.y} in C2 by A1;
then [[C1,C2],f] in {[[T,TT],g] where T is Element of CSp(X),
TT is Element of CSp(X),g is Element of FuncsC(X) :
(union TT={} implies union T={}) & g is Function of union T,union TT &
for x,y st {x,y} in T holds {g.x,g.y} in TT} by A1;
hence thesis by Def8;
end;
definition let X be set, l be Element of MapsC(X);
cluster l`2 -> Function-like Relation-like;
coherence
proof
consider g be Element of FuncsC(X),
C1,C2 be Element of CSp(X) such that
A1: l = [[C1,C2],g] and (union C2 = {} implies union C1 = {}) and
g is Function of union C1,union C2 &
for x,y st {x,y} in C1 holds {g.x,g.y} in C2 by Th18;
thus thesis by A1,MCART_1:def 2;
end;
end;
definition let X,l;
canceled;
func dom l -> Element of CSp(X) equals :Def10:
l`1`1;
coherence
proof
consider g,C1,C2 such that
A1: l = [[C1,C2],g] and (union C2 = {} implies union C1 = {}) &
g is Function of union C1,union C2 &
for x,y st {x,y} in C1 holds {g.x,g.y} in C2 by Th18;
[C1,C2] = l`1 by A1,MCART_1:def 1;
hence thesis by MCART_1:def 1;
end;
func cod l -> Element of CSp(X) equals :Def11:
l`1`2;
coherence
proof
consider g,C1,C2 such that
A2: l = [[C1,C2],g] and (union C2 = {} implies union C1 = {}) &
g is Function of union C1,union C2 &
for x,y st {x,y} in C1 holds {g.x,g.y} in C2 by Th18;
[C1,C2] = l`1 by A2,MCART_1:def 1;
hence thesis by MCART_1:def 2;
end;
end;
theorem Th20:
l = [[dom l,cod l],l`2]
proof
consider g,C1,C2 such that
A1: l = [[C1,C2],g] & (union C2 = {} implies union C1 = {}) &
g is Function of union C1,union C2 &
for x,y st {x,y} in C1 holds {g.x,g.y} in C2 by Th18;
dom l = l`1`1 & cod l = l`1`2 & [C1,C2] = l`1 by A1,Def10,Def11,MCART_1:def
1;
then l`1 = [dom l,cod l] & l`2 = l`2 by MCART_1:8;
hence thesis by A1,MCART_1:8;
end;
Lm1: l`2 = l1`2 & dom l = dom l1 & cod l = cod l1 implies l = l1
proof l = [[dom l,cod l],l`2] & l1 = [[dom l1,cod l1],l1`2] by Th20;
hence thesis;
end;
definition let X,C;
func id$ C -> Element of MapsC(X) equals :Def12:
[[C,C],id union C];
coherence
proof
A1: union C = {} implies union C = {};
set f = id union C;
now let x,y; assume A2: {x,y} in C;
then x in union C & y in union C by Th16;
then (id union C).x = x & (id union C).y = y by FUNCT_1:35;
hence {f.x,f.y} in C by A2;
end; hence thesis by A1,Th19;
end;
end;
Lm2: for x1,y1,x2,y2,x3,y3 being set st [[x1,x2],x3] = [[y1,y2],y3] holds
x1 = y1 & x2 = y2
proof let x1,y1,x2,y2,x3,y3 be set;
assume [[x1,x2],x3] = [[y1,y2],y3];
then [x1,x2] = [y1,y2] by ZFMISC_1:33;
hence thesis by ZFMISC_1:33;
end;
theorem Th21:
(union cod l <> {} or union dom l = {}) &
l`2 is Function of union dom l,union cod l &
for x,y st {x,y} in dom l holds {l`2.x,l`2.y} in cod l
proof
consider g,C1,C2 such that
A1: l = [[C1,C2],g] and
A2: (union C2={} implies union C1 = {}
) & g is Function of union C1,union C2 &
for x,y st {x,y} in C1 holds {g.x,g.y} in C2 by Th18;
l = [[dom l,cod l],l`2] by Th20;
then A3: g = l`2 & C1 = dom l & C2 = cod l by A1,Lm2,ZFMISC_1:33;
hence (union cod l <> {} or union dom l = {}) &
l`2 is Function of union dom l,union cod l by A2;
let x,y; assume {x,y} in dom l;
hence thesis by A2,A3;
end;
definition let X,l1,l2;
assume A1: cod l1 = dom l2;
func l2*l1 -> Element of MapsC(X) equals :Def13:
[[dom l1,cod l2],l2`2*l1`2];
coherence
proof
A2: (union cod l1 <> {} or union dom l1 = {}) &
l1`2 is Function of union dom l1,union cod l1 &
(for x,y st {x,y} in dom l1 holds {l1`2.x,l1`2.y} in cod l1) &
(union cod l2 <> {} or union dom l2 = {}) &
l2`2 is Function of union dom l2,union cod l2 &
(for x,y st {x,y} in dom l2 holds {l2`2.x,l2`2.y} in cod l2) by Th21;
then A3: l2`2*l1`2 is Function of union dom l1,union cod l2 by A1,FUNCT_2:19
;
now
let x,y; assume A4: {x,y} in dom l1;
then {l1`2.x,l1`2.y} in cod l1 by Th21;
then A5: {l2`2.(l1`2.x),l2`2.(l1`2.y)} in cod l2 by A1,Th21;
x in union dom l1 & y in union dom l1 by A4,Th16;
then A6: x in dom l1`2 & y in dom l1`2 by A2,FUNCT_2:def 1;
then {(l2`2*l1`2).x,l2`2.(l1`2.y)} in cod l2 by A5,FUNCT_1:23;
hence {(l2`2*l1`2).x,(l2`2*l1`2).y} in cod l2 by A6,FUNCT_1:23;
end; hence thesis by A1,A2,A3,Th19;
end;
end;
theorem Th22:
dom l2 = cod l1 implies
(l2*l1)`2 = l2`2*l1`2 & dom(l2*l1) = dom l1 & cod(l2*l1) = cod l2
proof assume dom l2 = cod l1;
then [[dom l1,cod l2],l2`2*l1`2] = l2*l1 by Def13
.= [[dom(l2*l1),cod(l2*l1)],(l2*l1)`2] by Th20;
hence thesis by Lm2,ZFMISC_1:33;
end;
theorem Th23:
dom l2 = cod l1 & dom l3 = cod l2 implies l3*(l2*l1) = (l3*l2)*l1
proof assume that
A1: dom l2 = cod l1 and
A2: dom l3 = cod l2;
(l2*l1)`2 = l2`2*l1`2 & dom(l2*l1) = dom l1 & cod(l2*l1) = cod l2 &
(l3*l2)`2 = l3`2*l2`2 & dom(l3*l2) = dom l2 &
cod(l3*l2) = cod l3 by A1,A2,Th22;
then (l3*(l2*l1))`2 = l3`2*(l2`2*l1`2) &
dom(l3*(l2*l1)) = dom l1 & cod(l3*(l2*l1)) = cod l3 &
((l3*l2)*l1)`2 = (l3`2*l2`2)*l1`2 &
dom((l3*l2)*l1) = dom l1 & cod((l3*l2)*l1) = cod l3 &
l3`2*(l2`2*l1`2) = (l3`2*l2`2)*l1`2 by A1,A2,Th22,RELAT_1:55;
hence thesis by Lm1;
end;
theorem Th24:
(id$ C)`2 = id union C & dom id$ C = C & cod id$ C = C
proof
[[dom id$ C,cod id$ C],(id$ C)`2] = id$ C by Th20
.= [[C,C],id union C] by Def12;
hence thesis by Lm2,ZFMISC_1:33;
end;
theorem Th25:
l*(id$ dom l) = l & (id$ cod l)*l = l
proof set i1 = id$ dom l, i2 = id$ cod l;
A1: (union cod l <> {} or union dom l = {}) &
l`2 is Function of union dom l,union cod l &
for x,y st {x,y} in dom l holds {l`2.x,l`2.y} in cod l by Th21;
cod i1 = dom l by Th24;
then dom l`2 = union dom l & i1`2 = id union dom l & dom i1 = dom l &
(l*i1)`2 = l`2*i1`2 & dom(l*i1) = dom i1 & cod(l*i1) = cod l &
l`2*(id dom l`2) = l`2 by A1,Th22,Th24,FUNCT_1:42,FUNCT_2:def 1;
hence l*i1 = l by Lm1;
dom i2 = cod l & rng l`2 c= union cod l by A1,Th24,RELSET_1:12;
then i2`2 = id union cod l & cod i2 = cod l &
(i2*l)`2 = i2`2*l`2 & dom(i2*l) = dom l & cod(i2*l) = cod i2 &
(id union cod l)*l`2 = l`2 by Th22,Th24,RELAT_1:79;
hence thesis by Lm1;
end;
definition let X;
func CDom X -> Function of MapsC(X),CSp(X) means :Def14:
for l holds it.l = dom l;
existence
proof
deffunc F(Element of MapsC(X)) = dom $1;
thus ex f being Function of MapsC(X),CSp(X) st
for x being Element of MapsC(X) holds f.x = F(x) from LambdaD;
end;
uniqueness
proof let h1,h2 be Function of MapsC(X),CSp(X) such that
A1: for l holds h1.l = dom l and
A2: for l holds h2.l = dom l;
now let l;
thus h1.l = dom l by A1
.= h2.l by A2;
end;
hence thesis by FUNCT_2:113;
end;
func CCod X -> Function of MapsC(X),CSp(X) means :Def15:
for l holds it.l = cod l;
existence
proof
deffunc F(Element of MapsC(X)) = cod $1;
thus ex f being Function of MapsC(X),CSp(X) st
for x being Element of MapsC(X) holds f.x = F(x) from LambdaD;
end;
uniqueness
proof let h1,h2 be Function of MapsC(X),CSp(X) such that
A3: for l holds h1.l = cod l and
A4: for l holds h2.l = cod l;
now let l;
thus h1.l = cod l by A3
.= h2.l by A4;
end;
hence thesis by FUNCT_2:113;
end;
func CComp X -> PartFunc of [:MapsC(X),MapsC(X):],MapsC(X) means :Def16:
(for l2,l1 holds [l2,l1] in dom it iff dom l2 = cod l1) &
(for l2,l1 st dom l2 = cod l1 holds it.[l2,l1] = l2*l1);
existence
proof
defpred P[set,set,set] means
for l2,l1 st l2=$1 & l1=$2 holds dom l2 = cod l1 & $3 = l2*l1;
A5: for x,y,z being set st x in MapsC(X) & y in MapsC(X) & P[x,y,z] holds
z in MapsC(X)
proof let x,y,z be set;
assume x in MapsC(X) & y in MapsC(X);
then reconsider l2 = x, l1 = y as Element of MapsC(X);
assume P[x,y,z]; then z = l2*l1;
hence thesis;
end;
A6: for x,y,z1,z2 being set st x in MapsC(X) & y in MapsC(X) &
P[x,y,z1] & P[x,y,z2] holds z1 = z2
proof let x,y,z1,z2 be set;
assume x in MapsC(X) & y in MapsC(X);
then reconsider l2 = x, l1 = y as Element of MapsC(X);
assume P[x,y,z1] & P[x,y,z2];
then z1 = l2*l1 & z2 = l2*l1;
hence thesis;
end;
consider h being PartFunc of [:MapsC(X),MapsC(X):],MapsC(X) such that
A7: for x,y holds [x,y] in dom h iff x in MapsC(X) & y in MapsC(X) &
ex z st P[x,y,z] and
A8: for x,y st [x,y] in dom h holds P[x,y,h.[x,y]] from PartFuncEx2(A5,A6);
take h;
thus A9: for l2,l1 holds [l2,l1] in dom h iff dom l2 = cod l1
proof let l2,l1;
thus [l2,l1] in dom h implies dom l2 = cod l1
proof assume [l2,l1] in dom h;
then ex z being set st P[l2,l1,z] by A7;
hence thesis;
end;
assume dom l2 = cod l1;
then P[l2,l1,l2*l1];
hence thesis by A7;
end;
let l2,l1;
assume dom l2 = cod l1; then [l2,l1] in dom h by A9;
hence thesis by A8;
end;
uniqueness
proof
let h1,h2 be PartFunc of [:MapsC(X),MapsC(X):],MapsC(X) such that
A10: for l2,l1 holds [l2,l1] in dom h1 iff dom l2 = cod l1 and
A11: for l2,l1 st dom l2 = cod l1 holds h1.[l2,l1] = l2*l1 and
A12: for l2,l1 holds [l2,l1] in dom h2 iff dom l2 = cod l1 and
A13: for l2,l1 st dom l2 = cod l1 holds h2.[l2,l1] = l2*l1;
now
thus dom h1 c= [:MapsC(X),MapsC(X):];
thus dom h2 c= [:MapsC(X),MapsC(X):];
let x,y be set;
thus [x,y] in dom h1 implies [x,y] in dom h2
proof assume
A14: [x,y] in dom h1;
then reconsider l2 = x, l1 = y as Element of MapsC(X) by ZFMISC_1:106;
dom l2 = cod l1 by A10,A14;
hence thesis by A12;
end;
assume
A15: [x,y] in dom h2;
then reconsider l2 = x, l1 = y as Element of MapsC(X) by ZFMISC_1:106;
dom l2 = cod l1 by A12,A15;
hence [x,y] in dom h1 by A10;
end;
then A16: dom h1 = dom h2 by ZFMISC_1:110;
now let l be Element of [:MapsC(X),MapsC(X):] such that
A17: l in dom h1; consider l2,l1 be Element of MapsC(X) such that
A18: l = [l2,l1] by DOMAIN_1:9;
dom l2 = cod l1 by A10,A17,A18;
then h1.[l2,l1] = l2*l1 & h2.[l2,l1] = l2*l1 by A11,A13;
hence h1.l = h2.l by A18;
end;
hence thesis by A16,PARTFUN1:34;
end;
func CId X -> Function of CSp(X),MapsC(X) means :Def17:
for C holds it.C = id$ C;
existence
proof
deffunc F(Element of CSp(X)) = id$ $1;
thus ex f being Function of CSp(X),MapsC(X) st
for x being Element of CSp(X) holds f.x = F(x) from LambdaD;
end;
uniqueness
proof let h1,h2 be Function of CSp(X),MapsC(X) such that
A19: for C holds h1.C = id$ C and
A20: for C holds h2.C = id$ C;
now let C; thus h1.C = id$ C by A19 .= h2.C by A20;end;
hence thesis by FUNCT_2:113;
end;
end;
theorem Th26:
CatStr(# CSp(X),MapsC(X),CDom X,CCod X,CComp X,CId X #) is Category
proof
set M = MapsC(X), d = CDom X, c = CCod X, p = CComp X, i = CId X;
now
thus for f,g being Element of M holds [g,f] in dom(p) iff d.g=c.f
proof let f,g be Element of M;
d.g = dom g & c.f = cod f by Def14,Def15;
hence thesis by Def16;
end;
thus for f,g being Element of M
st d.g=c.f holds d.(p.[g,f]) = d.f & c.(p.[g,f]) = c.g
proof let f,g be Element of M such that
A1: d.g=c.f;
d.g = dom g & c.f = cod f by Def14,Def15;
then dom(g*f) = dom f & cod(g*f) = cod g & p.[g,f] = g*f &
d.f = dom f & c.g = cod g by A1,Def14,Def15,Def16,Th22;
hence thesis by Def14,Def15;
end;
thus for f,g,h being Element of M
st d.h = c.g & d.g = c.f holds p.[h,p.[g,f]] = p.[p.[h,g],f]
proof let f,g,h be Element of M such that
A2: d.h = c.g and
A3: d.g = c.f;
A4: dom h = d.h & cod g = c.g & dom g = d.g & cod f = c.f by Def14,Def15;
then A5: cod(g*f) = dom h & dom(h*g) = dom g by A2,A3,Th22;
thus p.[h,p.[g,f]]
= p.[h,g*f] by A3,A4,Def16
.= h*(g*f) by A5,Def16
.= (h*g)*f by A2,A3,A4,Th23
.= p.[h*g,f] by A3,A4,A5,Def16
.= p.[p.[h,g],f] by A2,A4,Def16;
end;
let b be Element of CSp(X);
A6: i.b = id$ b & dom id$ b = b & cod id$ b = b by Def17,Th24;
hence d.(i.b) = b & c.(i.b) = b by Def14,Def15;
thus for f being Element of M st c.f=b holds p.[i.b,f] = f
proof let f be Element of M such that
A7: c.f = b;
A8: cod f = c.f by Def15;
then (id$ b)*f = f by A7,Th25;
hence thesis by A6,A7,A8,Def16;
end;
let g be Element of M such that
A9: d.g=b;
A10: dom g = d.g by Def14;
then g*(id$ b) = g by A9,Th25;
hence p.[g,i.b] = g by A6,A9,A10,Def16;
end;
hence thesis by CAT_1:def 8;
end;
definition let X;
func CohCat(X) -> Category equals
CatStr(# CSp(X),MapsC(X),CDom X,CCod X,CComp X,CId X #);
coherence by Th26;
end;
begin
::
:: Category of Tolerances
::
definition let X be set;
func Toler(X) -> set means :Def19:
x in it iff x is Tolerance of X;
existence
proof
defpred P[set] means $1 is Tolerance of X;
consider a such that
A1: for x holds x in a iff x in bool [:X,X:] & P[x] from Separation;
take a;
let x;
thus x in a implies x is Tolerance of X by A1;
assume x is Tolerance of X;
hence thesis by A1;
end;
uniqueness
proof let a,b be set; assume that
A2: x in a iff x is Tolerance of X and
A3: x in b iff x is Tolerance of X;
now let x;
A4: now assume x in a; then x is Tolerance of X by A2;
hence x in b by A3;
end;
now assume x in b; then x is Tolerance of X by A3;
hence x in a by A2;
end;
hence x in a iff x in b by A4;
end;
hence thesis by TARSKI:2;
end;
end;
definition let X be set;
cluster Toler(X) -> non empty;
coherence
proof
consider T being Tolerance of X;
T in Toler X by Def19;
hence thesis;
end;
end;
definition let X be set;
func Toler_on_subsets(X) -> set equals :Def20:
union {Toler(Y) where Y is Subset of X : not contradiction};
coherence;
end;
definition let X be set;
cluster Toler_on_subsets(X) -> non empty;
coherence
proof
set F = {Toler(Y) where Y is Element of bool X: not contradiction};
A1:union F = Toler_on_subsets(X) by Def20;
{} c= X by XBOOLE_1:2;
then {} in Toler({}) & Toler({}) in F by Def19,TOLER_1:39;
hence thesis by A1,TARSKI:def 4;
end;
end;
theorem
x in Toler_on_subsets(X) iff ex A st A c= X & x is Tolerance of A
proof
set f = {Toler(Y) where Y is Element of bool X: not contradiction};
thus x in Toler_on_subsets(X) implies ex A st A c= X & x is Tolerance of A
proof assume
x in Toler_on_subsets(X); then x in union f by Def20;
then consider a such that
A1: x in a & a in f by TARSKI:def 4;
consider Y be Element of bool X such that
A2: a = Toler(Y) by A1;
take Y;
thus thesis by A1,A2,Def19;
end;
given A such that
A3: A c= X & x is Tolerance of A;
reconsider A as Element of bool X by A3;
x in Toler(A) & Toler(A) in f by A3,Def19;
then x in union f by TARSKI:def 4;
hence thesis by Def20;
end;
theorem Th28:
Total a in Toler(a) by Def19;
canceled;
theorem Th30:
{} in Toler_on_subsets(X)
proof
set F = {Toler(Y) where Y is Element of bool X: not contradiction};
{} c= X by XBOOLE_1:2;
then {} in Toler({}) & Toler({}) in F by Def19,TOLER_1:39;
then {} in union F by TARSKI:def 4;
hence thesis by Def20;
end;
theorem Th31:
a c= X implies Total a in Toler_on_subsets(X)
proof
set F = {Toler(Y) where Y is Element of bool X: not contradiction};
assume a c= X;
then Total a in Toler(a) & Toler(a) in F by Th28;
then Total a in union F by TARSKI:def 4;
hence thesis by Def20;
end;
theorem Th32:
a c= X implies id a in Toler_on_subsets(X)
proof
set F = {Toler(Y) where Y is Element of bool X: not contradiction};
assume a c= X;
then id a in Toler(a) & Toler(a) in F by Def19;
then id a in union F by TARSKI:def 4;
hence thesis by Def20;
end;
theorem
Total X in Toler_on_subsets(X) by Th31;
theorem
id X in Toler_on_subsets(X) by Th32;
definition let X;
func TOL(X) -> set equals :Def21:
{ [t,Y] where t is Element of Toler_on_subsets(X),
Y is Element of bool X : t is Tolerance of Y};
coherence;
end;
definition let X;
cluster TOL(X) -> non empty;
coherence
proof
set FV = { [t,Y] where t is Element of Toler_on_subsets(X),
Y is Element of bool X : t is Tolerance of Y};
now
reconsider e = {} as Element of Toler_on_subsets(X) by Th30;
reconsider o = {} as Element of bool X by XBOOLE_1:2;
take m = [e,o];
thus m in FV by TOLER_1:39;
end;
hence thesis by Def21;
end;
end;
reserve T,T1,T2 for Element of TOL(X);
theorem
[{},{}] in TOL(X)
proof
{} in Toler_on_subsets(X) & {} c= X & {} is Tolerance of {}
by Th30,TOLER_1:39,XBOOLE_1:2;
then [{},{}] in{ [t,Y] where t is Element of Toler_on_subsets(X),
Y is Element of bool X : t is Tolerance of Y};
hence thesis by Def21;
end;
theorem Th36:
a c= X implies [id a,a] in TOL(X)
proof
assume a c= X;
then id a in Toler_on_subsets(X) & a in bool X &
id a is Tolerance of a by Th32;
then [id a,a] in{ [t,Y] where t is Element of Toler_on_subsets(X),
Y is Element of bool X : t is Tolerance of Y};
hence thesis by Def21;
end;
theorem Th37:
a c= X implies [Total a,a] in TOL(X)
proof
assume a c= X;
then Total a in Toler_on_subsets(X) & a in bool X &
Total a is Tolerance of a by Th31;
then [Total a,a] in{ [t,Y] where t is Element of Toler_on_subsets(X),
Y is Element of bool X : t is Tolerance of Y};
hence thesis by Def21;
end;
theorem
[id X,X] in TOL(X) by Th36;
theorem
[Total X,X] in TOL(X) by Th37;
definition let X,T;
redefine func T`2 -> Element of bool X;
coherence
proof T in TOL(X);
then T in { [t,Y] where t is Element of Toler_on_subsets(X),
Y is Element of bool X : t is Tolerance of Y} by Def21;
then consider t be Element of Toler_on_subsets(X),Y be Element of bool X
such that A1: T = [t,Y] & t is Tolerance of Y;
thus thesis by A1,MCART_1:def 2;
end;
func T`1 -> Tolerance of T`2;
coherence
proof T in TOL(X);
then T in { [t,Y] where t is Element of Toler_on_subsets(X),
Y is Element of bool X : t is Tolerance of Y} by Def21;
then consider t be Element of Toler_on_subsets(X),Y be Element of bool X
such that A2: T = [t,Y] & t is Tolerance of Y;
T`1 = t & T`2 = Y by A2,MCART_1:def 1,def 2;
hence thesis by A2;
end;
end;
definition let X;
func FuncsT(X) -> set equals :Def22:
union { Funcs(T`2,TT`2) where T is Element of TOL(X),
TT is Element of TOL(X): not contradiction };
coherence;
end;
definition let X;
cluster FuncsT(X) -> non empty functional;
coherence
proof set F = { Funcs(T`2,TT`2) where T is Element of TOL(X),
TT is Element of TOL(X): not contradiction };
A1: FuncsT X = union F by Def22;
consider A be Element of bool X;
reconsider T = [Total A,A] as Element of TOL(X) by Th37;
T`2 = A by MCART_1:def 2;
then id A in Funcs(T`2,T`2) & Funcs(T`2,T`2) in F by FUNCT_2:12;
then reconsider UF = union F as non empty set by TARSKI:def 4;
now let f be set;
assume f in UF;
then consider C being set such that
A2: f in C and
A3: C in F by TARSKI:def 4;
ex A,B be Element of TOL(X) st C = Funcs(A`2,B`2) by A3;
hence f is Function by A2,FUNCT_2:121;
end; hence thesis by A1,FRAENKEL:def 1;
end;
end;
reserve f for Element of FuncsT(X);
theorem Th40:
x in FuncsT(X) iff
ex T1,T2 st (T2`2 = {} implies T1`2 = {}) & x is Function of T1`2,T2`2
proof
set F = { Funcs(T`2,TT`2) where T is Element of TOL(X),
TT is Element of TOL(X): not contradiction };
A1: FuncsT(X) = union F by Def22;
thus x in FuncsT(X) implies
ex A,B be Element of TOL(X) st (B`2={} implies A`2={}) &
x is Function of A`2,B`2
proof assume x in FuncsT(X);
then consider C being set such that
A2: x in C and
A3: C in F by A1,TARSKI:def 4;
consider A,B be Element of TOL(X) such that
A4: C = Funcs(A`2,B`2) by A3;
take A,B;
thus thesis by A2,A4,FUNCT_2:14,121;
end;
given A,B be Element of TOL(X) such that
A5: (B`2={} implies A`2={}) & x is Function of A`2,B`2;
x in Funcs(A`2,B`2) & Funcs(A`2,B`2) in F by A5,FUNCT_2:11;
hence thesis by A1,TARSKI:def 4;
end;
definition let X;
func MapsT(X) -> set equals :Def23:
{ [[T,TT],f] where T is Element of TOL(X), TT is Element of TOL(X),
f is Element of FuncsT(X) :
(TT`2 = {} implies T`2 = {}) & f is Function of T`2,TT`2 &
for x,y st [x,y] in T`1 holds [f.x,f.y] in TT`1};
coherence;
end;
definition let X;
cluster MapsT(X) -> non empty;
coherence
proof
set FV = { [[T,TT],f] where T is Element of TOL(X), TT is Element of TOL(X),
f is Element of FuncsT(X) :
(TT`2 = {} implies T`2 = {}) & f is Function of T`2,TT`2 &
for x,y st [x,y] in T`1 holds [f.x,f.y] in TT`1};
now consider A be Element of bool X;
set a = [Total A,A],
f = id a`2;
take m = [[a,a],f];
reconsider a as Element of TOL(X) by Th37;
A1: a`2 = {} implies a`2 = {};
then reconsider f as Element of FuncsT(X) by Th40;
now let x,y; assume A2: [x,y] in a`1;
then x in a`2 & y in a`2 by ZFMISC_1:106;
then f.x = x & f.y = y by FUNCT_1:35;
hence [f.x,f.y] in a`1 by A2;
end;
hence m in FV by A1;
end;
hence thesis by Def23;
end;
end;
reserve m,m1,m2,m3 for Element of MapsT(X);
theorem Th41:
ex f,T1,T2 st m = [[T1,T2],f] & (T2`2 = {} implies T1`2 = {}) &
f is Function of T1`2,T2`2 & for x,y st [x,y] in T1`1 holds [f.x,f.y] in T2`1
proof m in MapsT(X);
then m in {[[T1,T2],f]: (T2`2={} implies T1`2={}) & f is Function of T1`2,T2
`2 &
for x,y st [x,y] in T1`1 holds [f.x,f.y] in T2`1}
by Def23;
then ex T1,T2,f st m = [[T1,T2],f] & (T2`2={} implies T1`2={}) &
f is Function of T1`2,T2`2 &
for x,y st [x,y] in T1`1 holds [f.x,f.y] in T2`1;
hence thesis;
end;
theorem Th42:
for f being Function of T1`2,T2`2 st (T2`2={} implies T1`2={}) &
(for x,y st [x,y] in T1`1 holds [f.x,f.y] in T2`1) holds [[T1,T2],f] in
MapsT(X)
proof let f be Function of T1`2,T2`2; assume
A1: (T2`2={} implies T1`2={}) &
(for x,y st [x,y] in T1`1 holds [f.x,f.y] in T2`1);
then reconsider f' = f as Element of FuncsT(X) by Th40;
for x,y st [x,y] in T1`1 holds [f'.x,f'.y] in T2`1 by A1;
then [[T1,T2],f] in {[[T,TT],g] where T is Element of TOL(X),
TT is Element of TOL(X),g is Element of FuncsT(X) :
(TT`2 = {} implies T`2 = {}) & g is Function of T`2,TT`2 &
for x,y st [x,y] in T`1 holds [g.x,g.y] in TT`1} by A1;
hence thesis by Def23;
end;
definition let X be set,m be Element of MapsT(X);
cluster m`2 -> Function-like Relation-like;
coherence
proof
consider f be Element of FuncsT(X),
T1,T2 be Element of TOL(X) such that
A1: m = [[T1,T2],f] and (T2`2 = {} implies T1`2 = {}) and
f is Function of T1`2,T2`2 &
for x,y st [x,y] in T1`1 holds [f.x,f.y] in T2`1 by Th41;
thus thesis by A1,MCART_1:def 2;
end;
end;
definition let X,m;
canceled;
func dom m -> Element of TOL(X) equals :Def25:
m`1`1;
coherence
proof
consider f,T1,T2 such that
A1: m = [[T1,T2],f] and (T2`2 = {} implies T1`2 = {}) &
f is Function of T1`2,T2`2 &
for x,y st [x,y] in T1`1 holds [f.x,f.y] in T2`1 by Th41;
[T1,T2] = m`1 by A1,MCART_1:def 1;
hence thesis by MCART_1:def 1;
end;
func cod m -> Element of TOL(X) equals :Def26:
m`1`2;
coherence
proof
consider f be Element of FuncsT(X),T1,T2 such that
A2: m = [[T1,T2],f] and (T2`2 = {} implies T1`2 = {}) &
f is Function of T1`2,T2`2 &
for x,y st [x,y] in T1`1 holds [f.x,f.y] in T2`1 by Th41;
[T1,T2] = m`1 by A2,MCART_1:def 1;
hence thesis by MCART_1:def 2;
end;
end;
theorem Th43:
m = [[dom m,cod m],m`2]
proof
consider f,T1,T2 such that
A1: m = [[T1,T2],f] & (T2`2 = {} implies T1`2 = {}) &
f is Function of T1`2,T2`2 & for x,y st [x,y] in T1`1 holds [f.x,f.y] in T2`1
by Th41;
dom m=m`1`1 & cod m=m`1`2 & [T1,T2] = m`1 by A1,Def25,Def26,MCART_1:def 1;
then m`1 = [dom m,cod m] & m`2 = m`2 by MCART_1:8;
hence thesis by A1,MCART_1:8;
end;
Lm3: m`2 = m1`2 & dom m = dom m1 & cod m = cod m1 implies m = m1
proof m = [[dom m,cod m],m`2] & m1 = [[dom m1,cod m1],m1`2] by Th43;
hence thesis;
end;
definition let X,T;
func id$ T -> Element of MapsT(X) equals :Def27:
[[T,T],id T`2];
coherence
proof
A1: T`2 = {} implies T`2 = {};
set f = id T`2;
now let x,y; assume A2: [x,y] in T`1;
then x in T`2 & y in T`2 by ZFMISC_1:106;
then (id T`2).x = x & (id T`2).y = y by FUNCT_1:35;
hence [f.x,f.y] in T`1 by A2;
end; hence thesis by A1,Th42;
end;
end;
theorem Th44:
((cod m)`2 <> {} or (dom m)`2 = {}) & m`2 is Function of (dom m)`2,(cod m)`2 &
for x,y st [x,y] in (dom m)`1 holds [m`2.x,m`2.y] in (cod m)`1
proof
consider f,T1,T2 such that
A1: m = [[T1,T2],f] and
A2: (T2`2 = {} implies T1`2 = {}) & f is Function of T1`2,T2`2 &
for x,y st [x,y] in T1`1 holds [f.x,f.y] in T2`1 by Th41;
m = [[dom m,cod m],m`2] by Th43;
then A3: f = m`2 & T1 = dom m & T2 = cod m by A1,Lm2,ZFMISC_1:33;
hence
((cod m)`2<>{} or (dom m)`2={}
) & m`2 is Function of (dom m)`2,(cod m)`2 by A2;
let x,y; assume [x,y] in (dom m)`1;
hence thesis by A2,A3;
end;
definition let X,m1,m2;
assume A1: cod m1 = dom m2;
func m2*m1 -> Element of MapsT(X) equals :Def28:
[[dom m1,cod m2],m2`2*m1`2];
coherence
proof
A2: ((cod m1)`2 <> {} or (dom m1)`2 = {}) &
m1`2 is Function of (dom m1)`2,(cod m1)`2 &
(for x,y st [x,y] in (dom m1)`1 holds [m1`2.x,m1`2.y] in (cod m1)`1) &
((cod m2)`2 <> {} or (dom m2)`2 = {}) &
m2`2 is Function of (dom m2)`2,(cod m2)`2 &
(for x,y st [x,y] in (dom m2)`1 holds [m2`2.x,m2`2.y] in
(cod m2)`1) by Th44;
then A3: m2`2*m1`2 is Function of (dom m1)`2,(cod m2)`2 by A1,FUNCT_2:19;
now
let x,y; assume A4: [x,y] in (dom m1)`1;
then [m1`2.x,m1`2.y] in (cod m1)`1 by Th44;
then A5: [m2`2.(m1`2.x),m2`2.(m1`2.y)] in (cod m2)`1 by A1,Th44;
x in (dom m1)`2 & y in (dom m1)`2 by A4,ZFMISC_1:106;
then A6: x in dom m1`2 & y in dom m1`2 by A2,FUNCT_2:def 1;
then [(m2`2*m1`2).x,m2`2.(m1`2.y)] in (cod m2)`1 by A5,FUNCT_1:23;
hence [(m2`2*m1`2).x,(m2`2*m1`2).y] in (cod m2)`1 by A6,FUNCT_1:23;
end; hence thesis by A1,A2,A3,Th42;
end;
end;
theorem Th45:
dom m2 = cod m1 implies
(m2*m1)`2 = m2`2*m1`2 & dom(m2*m1) = dom m1 & cod(m2*m1) = cod m2
proof assume dom m2 = cod m1;
then [[dom m1,cod m2],m2`2*m1`2]
= m2*m1 by Def28
.= [[dom(m2*m1),cod(m2*m1)],(m2*m1)`2] by Th43;
hence thesis by Lm2,ZFMISC_1:33;
end;
theorem Th46:
dom m2 = cod m1 & dom m3 = cod m2 implies m3*(m2*m1) = (m3*m2)*m1
proof assume that
A1: dom m2 = cod m1 and
A2: dom m3 = cod m2;
(m2*m1)`2 = m2`2*m1`2 & dom(m2*m1) = dom m1 & cod(m2*m1) = cod m2 &
(m3*m2)`2 = m3`2*m2`2 & dom(m3*m2) = dom m2 & cod(m3*m2) = cod m3
by A1,A2,Th45;
then (m3*(m2*m1))`2 = m3`2*(m2`2*m1`2) &
dom(m3*(m2*m1)) = dom m1 & cod(m3*(m2*m1)) = cod m3 &
((m3*m2)*m1)`2 = (m3`2*m2`2)*m1`2 &
dom((m3*m2)*m1) = dom m1 & cod((m3*m2)*m1) = cod m3 &
m3`2*(m2`2*m1`2) = (m3`2*m2`2)*m1`2 by A1,A2,Th45,RELAT_1:55;
hence thesis by Lm3;
end;
theorem Th47:
(id$ T)`2 = id T`2 & dom id$ T = T & cod id$ T = T
proof
[[dom id$ T,cod id$ T],(id$ T)`2] = id$ T by Th43
.= [[T,T],id T`2] by Def27;
hence thesis by Lm2,ZFMISC_1:33;
end;
theorem Th48:
m*(id$ dom m) = m & (id$ cod m)*m = m
proof set i1 = id$ dom m, i2 = id$ cod m;
A1: ((cod m)`2 <> {} or (dom m)`2 = {}) &
m`2 is Function of (dom m)`2,(cod m)`2 &
for x,y st [x,y] in (dom m)`1 holds [m`2.x,m`2.y] in (cod m)`1 by Th44;
cod i1 = dom m by Th47;
then dom m`2 = (dom m)`2 & i1`2 = id (dom m)`2 & dom i1 = dom m &
(m*i1)`2 = m`2*i1`2 & dom(m*i1) = dom i1 & cod(m*i1) = cod m &
m`2*(id dom m`2) = m`2 by A1,Th45,Th47,FUNCT_1:42,FUNCT_2:def 1;
hence m*i1 = m by Lm3;
dom i2 = cod m & rng m`2 c= (cod m)`2 by A1,Th47,RELSET_1:12;
then i2`2 = id (cod m)`2 & cod i2 = cod m &
(i2*m)`2 = i2`2*m`2 & dom(i2*m) = dom m & cod(i2*m) = cod i2 &
(id (cod m)`2)*m`2 = m`2 by Th45,Th47,RELAT_1:79;
hence thesis by Lm3;
end;
definition let X;
func fDom X -> Function of MapsT(X),TOL(X) means :Def29:
for m holds it.m = dom m;
existence
proof
deffunc F(Element of MapsT(X)) = dom $1;
thus ex f being Function of MapsT(X),TOL(X) st
for x being Element of MapsT(X) holds f.x = F(x) from LambdaD;
end;
uniqueness
proof let h1,h2 be Function of MapsT(X),TOL(X) such that
A1: for m holds h1.m = dom m and
A2: for m holds h2.m = dom m;
now let m;
thus h1.m = dom m by A1
.= h2.m by A2;
end;
hence thesis by FUNCT_2:113;
end;
func fCod X -> Function of MapsT(X),TOL(X) means :Def30:
for m holds it.m = cod m;
existence
proof
deffunc F(Element of MapsT(X)) = cod $1;
thus ex f being Function of MapsT(X),TOL(X) st
for x being Element of MapsT(X) holds f.x = F(x) from LambdaD;
end;
uniqueness
proof let h1,h2 be Function of MapsT(X),TOL(X) such that
A3: for m holds h1.m = cod m and
A4: for m holds h2.m = cod m;
now let m;
thus h1.m = cod m by A3
.= h2.m by A4;
end;
hence thesis by FUNCT_2:113;
end;
func fComp X -> PartFunc of [:MapsT(X),MapsT(X):],MapsT(X) means :Def31:
(for m2,m1 holds [m2,m1] in dom it iff dom m2 = cod m1) &
(for m2,m1 st dom m2 = cod m1 holds it.[m2,m1] = m2*m1);
existence
proof
defpred P[set,set,set] means
for m2,m1 st m2=$1 & m1=$2 holds dom m2 = cod m1 & $3 = m2*m1;
A5: for x,y,z being set st x in MapsT(X) & y in MapsT(X) & P[x,y,z] holds
z in MapsT(X)
proof let x,y,z be set;
assume x in MapsT(X) & y in MapsT(X);
then reconsider m2 = x, m1 = y as Element of MapsT(X);
assume P[x,y,z]; then z = m2*m1;
hence thesis;
end;
A6: for x,y,z1,z2 being set st x in MapsT(X) & y in MapsT(X) &
P[x,y,z1] & P[x,y,z2] holds z1 = z2
proof let x,y,z1,z2 be set;
assume x in MapsT(X) & y in MapsT(X);
then reconsider m2 = x, m1 = y as Element of MapsT(X);
assume P[x,y,z1] & P[x,y,z2];
then z1 = m2*m1 & z2 = m2*m1;
hence thesis;
end;
consider h being PartFunc of [:MapsT(X),MapsT(X):],MapsT(X) such that
A7: for x,y holds [x,y] in dom h iff x in MapsT(X) & y in MapsT(X) &
ex z st P[x,y,z] and
A8: for x,y st [x,y] in dom h holds P[x,y,h.[x,y]] from PartFuncEx2(A5,A6);
take h;
thus A9: for m2,m1 holds [m2,m1] in dom h iff dom m2 = cod m1
proof let m2,m1;
thus [m2,m1] in dom h implies dom m2 = cod m1
proof assume [m2,m1] in dom h;
then ex z being set st P[m2,m1,z] by A7;
hence thesis;
end;
assume dom m2 = cod m1;
then P[m2,m1,m2*m1];
hence thesis by A7;
end;
let m2,m1;
assume dom m2 = cod m1; then [m2,m1] in dom h by A9;
hence thesis by A8;
end;
uniqueness
proof
let h1,h2 be PartFunc of [:MapsT(X),MapsT(X):],MapsT(X) such that
A10: for m2,m1 holds [m2,m1] in dom h1 iff dom m2 = cod m1 and
A11: for m2,m1 st dom m2 = cod m1 holds h1.[m2,m1] = m2*m1 and
A12: for m2,m1 holds [m2,m1] in dom h2 iff dom m2 = cod m1 and
A13: for m2,m1 st dom m2 = cod m1 holds h2.[m2,m1] = m2*m1;
now
thus dom h1 c= [:MapsT(X),MapsT(X):];
thus dom h2 c= [:MapsT(X),MapsT(X):];
let x,y be set;
thus [x,y] in dom h1 implies [x,y] in dom h2
proof assume
A14: [x,y] in dom h1;
then reconsider m2 = x, m1 = y as Element of MapsT(X) by ZFMISC_1:106;
dom m2 = cod m1 by A10,A14;
hence thesis by A12;
end;
assume
A15: [x,y] in dom h2;
then reconsider m2 = x, m1 = y as Element of MapsT(X) by ZFMISC_1:106;
dom m2 = cod m1 by A12,A15;
hence [x,y] in dom h1 by A10;
end;
then A16: dom h1 = dom h2 by ZFMISC_1:110;
now let m be Element of [:MapsT(X),MapsT(X):] such that
A17: m in dom h1; consider m2,m1 be Element of MapsT(X) such that
A18: m = [m2,m1] by DOMAIN_1:9;
dom m2 = cod m1 by A10,A17,A18;
then h1.[m2,m1] = m2*m1 & h2.[m2,m1] = m2*m1 by A11,A13;
hence h1.m = h2.m by A18;
end;
hence thesis by A16,PARTFUN1:34;
end;
func fId X -> Function of TOL(X),MapsT(X) means :Def32:
for T holds it.T = id$ T;
existence
proof
deffunc F(Element of TOL(X)) = id$ $1;
thus ex f being Function of TOL(X),MapsT(X) st
for x being Element of TOL(X) holds f.x = F(x) from LambdaD;
end;
uniqueness
proof let h1,h2 be Function of TOL(X),MapsT(X) such that
A19: for T holds h1.T = id$ T and
A20: for T holds h2.T = id$ T;
now let T; thus h1.T = id$ T by A19 .= h2.T by A20;end;
hence thesis by FUNCT_2:113;
end;
end;
theorem Th49:
CatStr(# TOL(X),MapsT(X),fDom X,fCod X,fComp X,fId X #) is Category
proof
set M = MapsT(X), d = fDom X, c = fCod X, p = fComp X, i = fId X;
now
thus for f,g being Element of M holds [g,f] in dom(p) iff d.g=c.f
proof let f,g be Element of M;
d.g = dom g & c.f = cod f by Def29,Def30;
hence thesis by Def31;
end;
thus for f,g being Element of M
st d.g=c.f holds d.(p.[g,f]) = d.f & c.(p.[g,f]) = c.g
proof let f,g be Element of M such that
A1: d.g=c.f;
d.g = dom g & c.f = cod f by Def29,Def30;
then dom(g*f) = dom f & cod(g*f) = cod g & p.[g,f] = g*f &
d.f = dom f & c.g = cod g by A1,Def29,Def30,Def31,Th45;
hence thesis by Def29,Def30;
end;
thus for f,g,h being Element of M
st d.h = c.g & d.g = c.f holds p.[h,p.[g,f]] = p.[p.[h,g],f]
proof let f,g,h be Element of M such that
A2: d.h = c.g and
A3: d.g = c.f;
A4: dom h = d.h & cod g = c.g & dom g = d.g & cod f = c.f by Def29,Def30;
then A5: cod(g*f) = dom h & dom(h*g) = dom g by A2,A3,Th45;
thus p.[h,p.[g,f]]
= p.[h,g*f] by A3,A4,Def31
.= h*(g*f) by A5,Def31
.= (h*g)*f by A2,A3,A4,Th46
.= p.[h*g,f] by A3,A4,A5,Def31
.= p.[p.[h,g],f] by A2,A4,Def31;
end;
let b be Element of TOL(X);
A6: i.b = id$ b & dom id$ b = b & cod id$ b = b by Def32,Th47;
hence d.(i.b) = b & c.(i.b) = b by Def29,Def30;
thus for f being Element of M st c.f=b holds p.[i.b,f] = f
proof let f be Element of M such that
A7: c.f = b;
A8: cod f = c.f by Def30;
then (id$ b)*f = f by A7,Th48;
hence thesis by A6,A7,A8,Def31;
end;
let g be Element of M such that
A9: d.g=b;
A10: dom g = d.g by Def29;
then g*(id$ b) = g by A9,Th48;
hence p.[g,i.b] = g by A6,A9,A10,Def31;
end;
hence thesis by CAT_1:def 8;
end;
definition let X;
func TolCat(X) -> Category equals
CatStr(# TOL(X),MapsT(X),fDom X,fCod X,fComp X,fId X #);
coherence by Th49;
end;