coh_sp.miz
begin
reserve x,y,z,a,b,c,X,A for
set;
definition
let IT be
set;
::
COH_SP:def1
attr IT is
binary_complete means
:
Def1: 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
registration
cluster
subset-closed
binary_complete non
empty for
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 that
A1: a
in X and
A2: b
c= a;
a
=
{} by
A1,
TARSKI:def 1;
hence thesis by
A1,
A2;
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
A3: A
c= X and for a, b st a
in A & b
in A holds (a
\/ b)
in X;
now
per cases by
A3,
ZFMISC_1: 33;
suppose A
=
{} ;
hence thesis by
TARSKI:def 1,
ZFMISC_1: 2;
end;
suppose A
=
{
{} };
then (
union A)
=
{} by
ZFMISC_1: 25;
hence thesis by
TARSKI:def 1;
end;
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 ::
COH_SP:1
{}
in C
proof
{}
c= C & for a, b st a
in
{} & b
in
{} holds (a
\/ b)
in C;
hence thesis by
Def1,
ZFMISC_1: 2;
end;
theorem ::
COH_SP:2
Th2: (
bool X) is
Coherence_Space
proof
A1: 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: 76;
hence thesis;
end;
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;
hence thesis by
A1,
Def1,
CLASSES1:def 1;
end;
theorem ::
COH_SP:3
{
{} } is
Coherence_Space by
Th2,
ZFMISC_1: 1;
theorem ::
COH_SP:4
Th4: x
in (
union C) implies
{x}
in C
proof
assume x
in (
union C);
then
consider X such that
A1: x
in X and
A2: X
in C by
TARSKI:def 4;
{x}
c= X by
A1,
ZFMISC_1: 31;
hence thesis by
A2,
CLASSES1:def 1;
end;
definition
let C be
Coherence_Space;
::
COH_SP:def2
func
Web (C) ->
Tolerance of (
union C) means
:
Def2: for x,y be
object 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
TOLER_1:sch 1(
A1,
A3);
take T;
let x,y be
object;
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: 87;
hence thesis by
A4,
A5;
end;
given X such that
A6: X
in C & x
in X & y
in X;
x
in (
union C) & y
in (
union C) by
A6,
TARSKI:def 4;
hence thesis by
A4,
A6;
end;
uniqueness by
TOLER_1: 25;
end
reserve T for
Tolerance of (
union C);
theorem ::
COH_SP:5
Th5: T
= (
Web C) iff for x,y be
object holds
[x, y]
in T iff
{x, y}
in C
proof
thus T
= (
Web C) implies for x,y be
object holds
[x, y]
in T iff
{x, y}
in C
proof
assume
A1: T
= (
Web C);
let x,y be
object;
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 and
A3: x
in X & y
in X by
A1,
Def2;
{x, y}
c= X by
A3,
ZFMISC_1: 32;
hence thesis by
A2,
CLASSES1:def 1;
end;
A4: x
in
{x, y} & y
in
{x, y} by
TARSKI:def 2;
assume
{x, y}
in C;
hence thesis by
A1,
A4,
Def2;
end;
assume
A5: for x,y be
object holds
[x, y]
in T iff
{x, y}
in C;
for x,y be
object holds
[x, y]
in T iff ex X st X
in C & x
in X & y
in X
proof
let x,y be
object;
thus
[x, y]
in T implies ex X st X
in C & x
in X & y
in X
proof
assume
A6:
[x, y]
in T;
take
{x, y};
thus thesis by
A5,
A6,
TARSKI:def 2;
end;
given X such that
A7: X
in C and
A8: x
in X & y
in X;
{x, y}
c= X by
A8,
ZFMISC_1: 32;
then
{x, y}
in C by
A7,
CLASSES1:def 1;
hence thesis by
A5;
end;
hence thesis by
Def2;
end;
theorem ::
COH_SP:6
Th6: a
in C iff for x, y st x
in a & y
in a holds
{x, y}
in C
proof
defpred
P[
object,
object] means
{$1}
= $2;
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: 32;
hence thesis by
A1,
CLASSES1:def 1;
end;
A2: for x,y,z be
object st
P[x, y] &
P[x, z] holds y
= z;
consider X such that
A3: for x be
object holds x
in X iff ex y be
object st y
in a &
P[y, x] from
TARSKI:sch 1(
A2);
assume
A4: for x, y st x
in a & y
in a holds
{x, y}
in C;
A5: for b, c st b
in X & c
in X holds (b
\/ c)
in C
proof
let b, c;
assume that
A6: b
in X and
A7: c
in X;
consider z be
object such that
A8: z
in a and
A9:
{z}
= c by
A3,
A7;
consider y be
object such that
A10: y
in a and
A11:
{y}
= b by
A3,
A6;
{y, z}
in C by
A4,
A10,
A8;
hence thesis by
A11,
A9,
ENUMSET1: 1;
end;
A12: (
union X)
= a
proof
thus (
union X)
c= a
proof
let x be
object;
assume x
in (
union X);
then
consider Z be
set such that
A13: x
in Z and
A14: Z
in X by
TARSKI:def 4;
ex y be
object st y
in a & Z
=
{y} by
A3,
A14;
hence thesis by
A13,
TARSKI:def 1;
end;
let x be
object;
assume x
in a;
then
A15:
{x}
in X by
A3;
x
in
{x} by
TARSKI:def 1;
hence thesis by
A15,
TARSKI:def 4;
end;
X
c= C
proof
let x be
object;
assume x
in X;
then
consider y be
object such that
A16: y
in a and
A17:
{y}
= x by
A3;
{y, y}
in C by
A4,
A16;
hence thesis by
A17,
ENUMSET1: 29;
end;
hence thesis by
A5,
A12,
Def1;
end;
theorem ::
COH_SP:7
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 ::
COH_SP:8
(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 be
object;
assume x
in a;
then
{x, x}
in C by
A1;
then
A2:
{x}
in C by
ENUMSET1: 29;
x
in
{x} by
TARSKI:def 1;
hence thesis by
A2,
TARSKI:def 4;
end;
theorem ::
COH_SP:9
(
Web C)
= (
Web D) implies C
= D
proof
assume
A1: (
Web C)
= (
Web D);
thus C
c= D
proof
let x be
object;
reconsider xx = x as
set by
TARSKI: 1;
assume x
in C;
then for z, y st z
in xx & y
in xx holds
[z, y]
in (
Web D) by
A1,
Th7;
hence thesis by
Th7;
end;
let x be
object;
reconsider xx = x as
set by
TARSKI: 1;
assume x
in D;
then for z, y st z
in xx & y
in xx holds
[z, y]
in (
Web C) by
A1,
Th7;
hence thesis by
Th7;
end;
theorem ::
COH_SP:10
(
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: 82;
let x be
object;
assume x
in (
bool (
union C));
hence thesis by
A1,
CLASSES1:def 1;
end;
theorem ::
COH_SP:11
C
= (
bool (
union C)) implies (
Web C)
= (
Total (
union C))
proof
reconsider t = (
Total (
union C)) as
Tolerance of (
union C);
assume
A1: C
= (
bool (
union C));
now
let x,y be
object;
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: 87;
{x, y}
c= (
union C) by
A2,
TARSKI:def 2;
hence thesis by
A1;
end;
assume
{x, y}
in C;
then x
in (
union C) & y
in (
union C) by
A1,
ZFMISC_1: 32;
hence
[x, y]
in t by
TOLER_1: 2;
end;
hence thesis by
Th5;
end;
definition
let X be
set;
let E be
Tolerance of X;
::
COH_SP:def3
func
CohSp (E) ->
Coherence_Space means
:
Def3: 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
XFAMILY:sch 1;
A2: 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
A3: A
c= Z and
A4: for a, b st a
in A & b
in A holds (a
\/ b)
in Z;
A5:
now
let x, y;
assume that
A6: x
in (
union A) and
A7: y
in (
union A);
consider Y1 be
set such that
A8: y
in Y1 and
A9: Y1
in A by
A7,
TARSKI:def 4;
consider X1 be
set such that
A10: x
in X1 and
A11: X1
in A by
A6,
TARSKI:def 4;
A12: x
in (X1
\/ Y1) by
A10,
XBOOLE_0:def 3;
A13: y
in (X1
\/ Y1) by
A8,
XBOOLE_0:def 3;
(X1
\/ Y1)
in Z by
A4,
A11,
A9;
hence
[x, y]
in E by
A1,
A12,
A13;
end;
now
let a;
assume a
in A;
then a
in (
bool X) by
A1,
A3;
hence a
c= X;
end;
then (
union A)
c= X by
ZFMISC_1: 76;
hence thesis by
A1,
A5;
end;
A14: for a, b st a
in Z & b
c= a holds b
in Z
proof
let a, b;
assume that
A15: a
in Z and
A16: b
c= a;
a
in (
bool X) by
A1,
A15;
then
A17: b
c= X by
A16,
XBOOLE_1: 1;
for x, y st x
in b & y
in b holds
[x, y]
in E by
A1,
A15,
A16;
hence thesis by
A1,
A17;
end;
P[
{} ] &
{}
c= X;
then
reconsider Z as
Coherence_Space by
A1,
A14,
A2,
Def1,
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
A18: for x, y st x
in a & y
in a holds
[x, y]
in E;
then a
c= X by
TOLER_1: 18,
TOLER_1:def 1;
hence thesis by
A1,
A18;
end;
uniqueness
proof
let C, D;
assume that
A19: for a holds a
in C iff for x, y st x
in a & y
in a holds
[x, y]
in E and
A20: 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 be
object;
reconsider xx = x as
set by
TARSKI: 1;
assume x
in C;
then for z, y st z
in xx & y
in xx holds
[z, y]
in E by
A19;
hence thesis by
A20;
end;
let x be
object;
reconsider xx = x as
set by
TARSKI: 1;
assume x
in D;
then for z, y st z
in xx & y
in xx holds
[z, y]
in E by
A20;
hence thesis by
A19;
end;
end
reserve E for
Tolerance of X;
theorem ::
COH_SP:12
(
Web (
CohSp E))
= E
proof
now
let x,y be
object;
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,
Def3;
end;
assume
A2:
[x, y]
in E;
then
A3: x
in X & y
in X by
ZFMISC_1: 87;
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 that
A4: u
in
{x, y} and
A5: v
in
{x, y};
A6: v
= x or v
= y by
A5,
TARSKI:def 2;
u
= x or u
= y by
A4,
TARSKI:def 2;
hence thesis by
A2,
A3,
A6,
EQREL_1: 6,
TOLER_1: 7;
end;
then
{x, y}
in (
CohSp E) by
Def3;
hence
[x, y]
in (
Web (
CohSp E)) by
Th5;
end;
hence thesis;
end;
theorem ::
COH_SP:13
(
CohSp (
Web C))
= C
proof
thus (
CohSp (
Web C))
c= C
proof
let x be
object;
reconsider xx = x as
set by
TARSKI: 1;
assume x
in (
CohSp (
Web C));
then for y, z st y
in xx & z
in xx holds
[y, z]
in (
Web C) by
Def3;
hence thesis by
Th7;
end;
let x be
object;
reconsider xx = x as
set by
TARSKI: 1;
assume x
in C;
then for y, z st y
in xx & z
in xx holds
[y, z]
in (
Web C) by
Th7;
hence thesis by
Def3;
end;
theorem ::
COH_SP:14
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
Def3;
hence thesis by
TOLER_1:def 1;
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 1;
hence thesis by
Def3;
end;
theorem ::
COH_SP:15
(
CohSp E)
= (
TolSets E)
proof
thus (
CohSp E)
c= (
TolSets E)
proof
let x be
object;
assume x
in (
CohSp E);
then x is
TolSet of E by
Th14;
hence thesis by
TOLER_1:def 3;
end;
let x be
object;
assume x
in (
TolSets E);
then x is
TolSet of E by
TOLER_1:def 3;
hence thesis by
Th14;
end;
begin
definition
let X;
::
COH_SP:def4
func
CSp (X) ->
set equals { x where x be
Subset-Family of X : x is
Coherence_Space };
coherence ;
end
registration
let X;
cluster (
CSp X) -> non
empty;
coherence
proof
reconsider b = (
bool X) as
Subset-Family of X;
set F = { x where x be
Subset-Family of X : x is
Coherence_Space };
b is
Coherence_Space by
Th2;
then b
in F;
hence thesis;
end;
end
registration
let X be
set;
cluster ->
subset-closed
binary_complete non
empty for
Element of (
CSp X);
coherence
proof
let C be
Element of (
CSp X);
C
in { x where x be
Subset-Family of X : x is
Coherence_Space };
then ex x be
Subset-Family of X st C
= x & x is
Coherence_Space;
hence thesis;
end;
end
reserve C,C1,C2 for
Element of (
CSp X);
theorem ::
COH_SP:16
Th16:
{x, y}
in C implies x
in (
union C) & y
in (
union C)
proof
A1:
{x}
c=
{x, y} &
{y}
c=
{x, y} by
ZFMISC_1: 7;
A2: x
in
{x} & y
in
{y} by
TARSKI:def 1;
assume
{x, y}
in C;
hence thesis by
A1,
A2,
TARSKI:def 4;
end;
definition
let X;
::
COH_SP:def5
func
FuncsC (X) ->
set equals (
union the set of all (
Funcs ((
union x),(
union y))) where x be
Element of (
CSp X), y be
Element of (
CSp X));
coherence ;
end
registration
let X;
cluster (
FuncsC X) -> non
empty
functional;
coherence
proof
reconsider A = (
bool X) as
Subset-Family of X;
A is
Coherence_Space by
Th2;
then A
in { x where x be
Subset-Family of X : x is
Coherence_Space };
then
reconsider A as
Element of (
CSp X);
set F = the set of all (
Funcs ((
union T),(
union TT))) where T be
Element of (
CSp X), TT be
Element of (
CSp X);
(
id (
union A))
in (
Funcs ((
union A),(
union A))) & (
Funcs ((
union A),(
union A)))
in F by
FUNCT_2: 9;
then
reconsider UF = (
union F) as non
empty
set by
TARSKI:def 4;
now
let f be
object;
assume f
in UF;
then
consider C be
set such that
A1: f
in C and
A2: C
in F by
TARSKI:def 4;
ex A,B be
Element of (
CSp X) st C
= (
Funcs ((
union A),(
union B))) by
A2;
hence f is
Function by
A1;
end;
hence thesis by
FUNCT_1:def 13;
end;
end
reserve g for
Element of (
FuncsC X);
theorem ::
COH_SP:17
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 = the set of all (
Funcs ((
union xx),(
union y))) where xx be
Element of (
CSp X), y be
Element of (
CSp X);
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 be
set such that
A1: x
in C and
A2: C
in F by
TARSKI:def 4;
consider A,B be
Element of (
CSp X) such that
A3: C
= (
Funcs ((
union A),(
union B))) by
A2;
take A, B;
thus thesis by
A1,
A3,
FUNCT_2: 66;
end;
given A,B be
Element of (
CSp X) such that
A4: ((
union B)
=
{} implies (
union A)
=
{} ) & x is
Function of (
union A), (
union B);
A5: (
Funcs ((
union A),(
union B)))
in F;
x
in (
Funcs ((
union A),(
union B))) by
A4,
FUNCT_2: 8;
hence thesis by
A5,
TARSKI:def 4;
end;
definition
let X;
::
COH_SP:def6
func
MapsC (X) ->
set equals {
[
[C, CC], f] where C be
Element of (
CSp X), CC be
Element of (
CSp X), f be
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
registration
let X;
cluster (
MapsC X) -> non
empty;
coherence
proof
set FV = {
[
[T, TT], f] where T be
Element of (
CSp X), TT be
Element of (
CSp X), f be
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
Subset-Family of X;
A is
Coherence_Space by
Th2;
then A
in { xx where xx be
Subset-Family of X : xx is
Coherence_Space };
then
reconsider A as
Element of (
CSp X);
set f = (
id (
union A));
take m =
[
[A, A], f];
A1: (
union A)
=
{} implies (
union A)
=
{} ;
reconsider f as
Element of (
FuncsC X) by
Th17;
now
let x, y;
assume
A2:
{x, y}
in A;
then x
in (
union A) by
Th16;
then
A3: (f
. x)
= x by
FUNCT_1: 18;
y
in (
union A) by
A2,
Th16;
hence
{(f
. x), (f
. y)}
in A by
A2,
A3,
FUNCT_1: 18;
end;
hence m
in FV by
A1;
end;
hence thesis;
end;
end
reserve l,l1,l2,l3 for
Element of (
MapsC X);
theorem ::
COH_SP:18
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 {
[
[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 };
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 ::
COH_SP:19
Th19: for f be
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 that
A1: (
union C2)
=
{} implies (
union C1)
=
{} and
A2: for x, y st
{x, y}
in C1 holds
{(f
. x), (f
. y)}
in C2;
reconsider f9 = f as
Element of (
FuncsC X) by
A1,
Th17;
for x, y st
{x, y}
in C1 holds
{(f9
. x), (f9
. y)}
in C2 by
A2;
hence thesis by
A1;
end;
registration
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] & ((
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;
thus thesis by
A1;
end;
end
definition
let X, l;
::
COH_SP:def7
func
dom l ->
Element of (
CSp X) equals ((l
`1 )
`1 );
coherence
proof
consider g, C1, C2 such that
A1: l
=
[
[C1, C2], g] and (
union C2)
=
{} implies (
union C1)
=
{} and g is
Function of (
union C1), (
union C2) and for x, y st
{x, y}
in C1 holds
{(g
. x), (g
. y)}
in C2 by
Th18;
thus thesis by
A1;
end;
::
COH_SP:def8
func
cod l ->
Element of (
CSp X) equals ((l
`1 )
`2 );
coherence
proof
consider g, C1, C2 such that
A2: l
=
[
[C1, C2], g] and (
union C2)
=
{} implies (
union C1)
=
{} and g is
Function of (
union C1), (
union C2) and for x, y st
{x, y}
in C1 holds
{(g
. x), (g
. y)}
in C2 by
Th18;
thus thesis by
A2;
end;
end
theorem ::
COH_SP:20
Th20: l
=
[
[(
dom l), (
cod l)], (l
`2 )]
proof
consider g, C1, C2 such that
A1: l
=
[
[C1, C2], g] and (
union C2)
=
{} implies (
union C1)
=
{} and g is
Function of (
union C1), (
union C2) and for x, y st
{x, y}
in C1 holds
{(g
. x), (g
. y)}
in C2 by
Th18;
thus thesis by
A1;
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 )] by
Th20;
hence thesis by
Th20;
end;
definition
let X, C;
::
COH_SP:def9
func
id$ C ->
Element of (
MapsC X) equals
[
[C, C], (
id (
union C))];
coherence
proof
set f = (
id (
union C));
now
let x, y;
assume
A1:
{x, y}
in C;
then x
in (
union C) by
Th16;
then
A2: ((
id (
union C))
. x)
= x by
FUNCT_1: 18;
y
in (
union C) by
A1,
Th16;
hence
{(f
. x), (f
. y)}
in C by
A1,
A2,
FUNCT_1: 18;
end;
hence thesis by
Th19;
end;
end
Lm2: for x1,y1,x2,y2,x3,y3 be
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
XTUPLE_0: 1;
hence thesis by
XTUPLE_0: 1;
end;
theorem ::
COH_SP:21
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) and
A3: for x, y st
{x, y}
in C1 holds
{(g
. x), (g
. y)}
in C2 by
Th18;
A4: C2
= (
cod l) by
A1;
A5: g
= (l
`2 ) & C1
= (
dom l) by
A1;
thus ((
union (
cod l))
<>
{} or (
union (
dom l))
=
{} ) & (l
`2 ) is
Function of (
union (
dom l)), (
union (
cod l)) by
A1,
A2;
let x, y;
assume
{x, y}
in (
dom l);
hence thesis by
A3,
A5,
A4;
end;
definition
let X, l1, l2;
assume
A1: (
cod l1)
= (
dom l2);
::
COH_SP:def10
func l2
* l1 ->
Element of (
MapsC X) equals
:
Def10:
[
[(
dom l1), (
cod l2)], ((l2
`2 )
* (l1
`2 ))];
coherence
proof
A2: (
union (
cod l2))
<>
{} or (
union (
dom l2))
=
{} by
Th21;
A3: (
union (
cod l1))
<>
{} or (
union (
dom l1))
=
{} by
Th21;
A4: (l1
`2 ) is
Function of (
union (
dom l1)), (
union (
cod l1)) by
Th21;
A5:
now
let x, y;
assume
A6:
{x, y}
in (
dom l1);
then x
in (
union (
dom l1)) by
Th16;
then
A7: x
in (
dom (l1
`2 )) by
A3,
A4,
FUNCT_2:def 1;
y
in (
union (
dom l1)) by
A6,
Th16;
then
A8: y
in (
dom (l1
`2 )) by
A3,
A4,
FUNCT_2:def 1;
{((l1
`2 )
. x), ((l1
`2 )
. y)}
in (
cod l1) by
A6,
Th21;
then
{((l2
`2 )
. ((l1
`2 )
. x)), ((l2
`2 )
. ((l1
`2 )
. y))}
in (
cod l2) by
A1,
Th21;
then
{(((l2
`2 )
* (l1
`2 ))
. x), ((l2
`2 )
. ((l1
`2 )
. y))}
in (
cod l2) by
A7,
FUNCT_1: 13;
hence
{(((l2
`2 )
* (l1
`2 ))
. x), (((l2
`2 )
* (l1
`2 ))
. y)}
in (
cod l2) by
A8,
FUNCT_1: 13;
end;
(l2
`2 ) is
Function of (
union (
dom l2)), (
union (
cod l2)) by
Th21;
then ((l2
`2 )
* (l1
`2 )) is
Function of (
union (
dom l1)), (
union (
cod l2)) by
A1,
A3,
A4,
FUNCT_2: 13;
hence thesis by
A1,
A3,
A2,
A5,
Th19;
end;
end
theorem ::
COH_SP:22
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
Def10
.=
[
[(
dom (l2
* l1)), (
cod (l2
* l1))], ((l2
* l1)
`2 )] by
Th20;
hence thesis by
Lm2,
XTUPLE_0: 1;
end;
theorem ::
COH_SP:23
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);
A3: (
cod (l2
* l1))
= (
cod l2) by
A1,
Th22;
((l2
* l1)
`2 )
= ((l2
`2 )
* (l1
`2 )) by
A1,
Th22;
then
A4: ((l3
* (l2
* l1))
`2 )
= ((l3
`2 )
* ((l2
`2 )
* (l1
`2 ))) by
A2,
A3,
Th22;
A5: (
dom (l3
* l2))
= (
dom l2) by
A2,
Th22;
then
A6: (
dom ((l3
* l2)
* l1))
= (
dom l1) by
A1,
Th22;
(
dom (l2
* l1))
= (
dom l1) by
A1,
Th22;
then
A7: (
dom (l3
* (l2
* l1)))
= (
dom l1) by
A2,
A3,
Th22;
(
cod (l3
* l2))
= (
cod l3) by
A2,
Th22;
then
A8: (
cod ((l3
* l2)
* l1))
= (
cod l3) by
A1,
A5,
Th22;
((l3
* l2)
`2 )
= ((l3
`2 )
* (l2
`2 )) by
A2,
Th22;
then
A9: (((l3
* l2)
* l1)
`2 )
= (((l3
`2 )
* (l2
`2 ))
* (l1
`2 )) by
A1,
A5,
Th22;
(
cod (l3
* (l2
* l1)))
= (
cod l3) by
A2,
A3,
Th22;
hence thesis by
A4,
A7,
A9,
A6,
A8,
Lm1,
RELAT_1: 36;
end;
theorem ::
COH_SP:24
((
id$ C)
`2 )
= (
id (
union C)) & (
dom (
id$ C))
= C & (
cod (
id$ C))
= C;
theorem ::
COH_SP:25
Th25: (l
* (
id$ (
dom l)))
= l & ((
id$ (
cod l))
* l)
= l
proof
set i1 = (
id$ (
dom l)), i2 = (
id$ (
cod l));
A1: (l
`2 ) is
Function of (
union (
dom l)), (
union (
cod l)) by
Th21;
then
A2: (
rng (l
`2 ))
c= (
union (
cod l)) by
RELAT_1:def 19;
(
union (
cod l))
<>
{} or (
union (
dom l))
=
{} by
Th21;
then
A3: (
dom (l
`2 ))
= (
union (
dom l)) by
A1,
FUNCT_2:def 1;
A4: (
cod i1)
= (
dom l);
then
A5: (
cod (l
* i1))
= (
cod l) by
Th22;
((l
* i1)
`2 )
= ((l
`2 )
* (i1
`2 )) & (
dom (l
* i1))
= (
dom i1) by
A4,
Th22;
hence (l
* i1)
= l by
A3,
A5,
Lm1,
RELAT_1: 52;
A6: (
dom i2)
= (
cod l);
then
A7: (
cod (i2
* l))
= (
cod i2) by
Th22;
((i2
* l)
`2 )
= ((i2
`2 )
* (l
`2 )) & (
dom (i2
* l))
= (
dom l) by
A6,
Th22;
hence thesis by
A2,
A7,
Lm1,
RELAT_1: 53;
end;
definition
let X;
::
COH_SP:def11
func
CDom X ->
Function of (
MapsC X), (
CSp X) means
:
Def11: for l holds (it
. l)
= (
dom l);
existence
proof
deffunc
F(
Element of (
MapsC X)) = (
dom $1);
thus ex f be
Function of (
MapsC X), (
CSp X) st for x be
Element of (
MapsC X) holds (f
. x)
=
F(x) from
FUNCT_2:sch 4;
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: 63;
end;
::
COH_SP:def12
func
CCod X ->
Function of (
MapsC X), (
CSp X) means
:
Def12: for l holds (it
. l)
= (
cod l);
existence
proof
deffunc
F(
Element of (
MapsC X)) = (
cod $1);
thus ex f be
Function of (
MapsC X), (
CSp X) st for x be
Element of (
MapsC X) holds (f
. x)
=
F(x) from
FUNCT_2:sch 4;
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: 63;
end;
::
COH_SP:def13
func
CComp X ->
PartFunc of
[:(
MapsC X), (
MapsC X):], (
MapsC X) means
:
Def13: (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[
object,
object,
object] means for l2, l1 st l2
= $1 & l1
= $2 holds (
dom l2)
= (
cod l1) & $3
= (l2
* l1);
A5: for x,y,z1,z2 be
object 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
object;
assume x
in (
MapsC X) & y
in (
MapsC X);
then
reconsider l2 = x, l1 = y as
Element of (
MapsC X);
assume that
A6:
P[x, y, z1] and
A7:
P[x, y, z2];
z1
= (l2
* l1) by
A6;
hence thesis by
A7;
end;
A8: for x,y,z be
object st x
in (
MapsC X) & y
in (
MapsC X) &
P[x, y, z] holds z
in (
MapsC X)
proof
let x,y,z be
object;
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;
consider h be
PartFunc of
[:(
MapsC X), (
MapsC X):], (
MapsC X) such that
A9: for x,y be
object holds
[x, y]
in (
dom h) iff x
in (
MapsC X) & y
in (
MapsC X) & ex z be
object st
P[x, y, z] and
A10: for x,y be
object st
[x, y]
in (
dom h) holds
P[x, y, (h
. (x,y))] from
BINOP_1:sch 5(
A8,
A5);
take h;
thus
A11: 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 be
object st
P[l2, l1, z] by
A9;
hence thesis;
end;
assume (
dom l2)
= (
cod l1);
then
P[l2, l1, (l2
* l1)];
hence thesis by
A9;
end;
let l2, l1;
assume (
dom l2)
= (
cod l1);
then
[l2, l1]
in (
dom h) by
A11;
then
P[l2, l1, (h
. (l2,l1))] by
A10;
hence thesis;
end;
uniqueness
proof
let h1,h2 be
PartFunc of
[:(
MapsC X), (
MapsC X):], (
MapsC X) such that
A12: for l2, l1 holds
[l2, l1]
in (
dom h1) iff (
dom l2)
= (
cod l1) and
A13: for l2, l1 st (
dom l2)
= (
cod l1) holds (h1
.
[l2, l1])
= (l2
* l1) and
A14: for l2, l1 holds
[l2, l1]
in (
dom h2) iff (
dom l2)
= (
cod l1) and
A15: for l2, l1 st (
dom l2)
= (
cod l1) holds (h2
.
[l2, l1])
= (l2
* l1);
A16: (
dom h1)
= (
dom h2)
proof
let x,y be
object;
thus
[x, y]
in (
dom h1) implies
[x, y]
in (
dom h2)
proof
assume
A17:
[x, y]
in (
dom h1);
then
reconsider l2 = x, l1 = y as
Element of (
MapsC X) by
ZFMISC_1: 87;
(
dom l2)
= (
cod l1) by
A12,
A17;
hence thesis by
A14;
end;
assume
A18:
[x, y]
in (
dom h2);
then
reconsider l2 = x, l1 = y as
Element of (
MapsC X) by
ZFMISC_1: 87;
(
dom l2)
= (
cod l1) by
A14,
A18;
hence thesis by
A12;
end;
now
let l be
Element of
[:(
MapsC X), (
MapsC X):] such that
A19: l
in (
dom h1);
consider l2,l1 be
Element of (
MapsC X) such that
A20: l
=
[l2, l1] by
DOMAIN_1: 1;
A21: (
dom l2)
= (
cod l1) by
A12,
A19,
A20;
then (h1
.
[l2, l1])
= (l2
* l1) by
A13;
hence (h1
. l)
= (h2
. l) by
A15,
A20,
A21;
end;
hence thesis by
A16,
PARTFUN1: 5;
end;
end
::$Canceled
definition
::$Canceled
let X;
::
COH_SP:def15
func
CohCat (X) -> non
empty non
void
strict
CatStr equals
CatStr (# (
CSp X), (
MapsC X), (
CDom X), (
CCod X), (
CComp X) #);
coherence ;
end
registration
let X;
cluster (
CohCat X) ->
Category-like
transitive
associative
reflexive;
coherence
proof
set M = (
MapsC X), d = (
CDom X), c = (
CCod X), p = (
CComp X);
set C = (
CohCat X);
thus
A1: C is
Category-like
proof
let ff,gg be
Morphism of C;
reconsider f = ff, g = gg as
Element of M;
(d
. gg)
= (
dom g) & (c
. ff)
= (
cod f) by
Def11,
Def12;
hence thesis by
Def13;
end;
thus
A2: C is
transitive
proof
let ff,gg be
Morphism of C such that
A3: (
dom gg)
= (
cod ff);
[gg, ff]
in (
dom the
Comp of C) by
A3,
A1;
then
A4: (the
Comp of C
. (gg,ff))
= (gg
(*) ff) by
CAT_1:def 1;
reconsider f = ff, g = gg as
Element of M;
A5: (d
. g)
= (
dom g) & (c
. f)
= (
cod f) by
Def11,
Def12;
then
A6: (p
.
[g, f])
= (g
* f) by
A3,
Def13;
A7: (d
. f)
= (
dom f) & (c
. g)
= (
cod g) by
Def11,
Def12;
(
dom (g
* f))
= (
dom f) & (
cod (g
* f))
= (
cod g) by
A3,
A5,
Th22;
hence thesis by
A6,
A7,
Def11,
Def12,
A4;
end;
thus C is
associative
proof
let ff,gg,hh be
Morphism of C such that
A8: (
dom hh)
= (
cod gg) and
A9: (
dom gg)
= (
cod ff);
reconsider f = ff, g = gg, h = hh as
Element of M;
A10: (
dom h)
= (d
. h) & (
cod g)
= (c
. g) by
Def11,
Def12;
then
A11: (
dom (h
* g))
= (
dom g) by
A8,
Th22;
A12: (
dom g)
= (d
. g) & (
cod f)
= (c
. f) by
Def11,
Def12;
then
A13: (
cod (g
* f))
= (
dom h) by
A8,
A9,
A10,
Th22;
[hh, gg]
in (
dom the
Comp of C) by
A1,
A8;
then
A14: (hh
(*) gg)
= (the
Comp of C
. (hh,gg)) by
CAT_1:def 1;
(
dom (hh
(*) gg))
= (
dom gg) by
A2,
A8;
then
A15:
[(hh
(*) gg), ff]
in (
dom the
Comp of C) by
A1,
A9;
[gg, ff]
in (
dom the
Comp of C) by
A1,
A9;
then
A16: (gg
(*) ff)
= (the
Comp of C
. (gg,ff)) by
CAT_1:def 1;
(
cod (gg
(*) ff))
= (
cod gg) by
A2,
A9;
then
[hh, (gg
(*) ff)]
in (
dom the
Comp of C) by
A1,
A8;
hence (hh
(*) (gg
(*) ff))
= (the
Comp of C
. (hh,(the
Comp of C
. (gg,ff)))) by
A16,
CAT_1:def 1
.= (p
.
[h, (g
* f)]) by
A9,
A12,
Def13
.= (h
* (g
* f)) by
A13,
Def13
.= ((h
* g)
* f) by
A8,
A9,
A10,
A12,
Th23
.= (p
.
[(h
* g), f]) by
A9,
A12,
A11,
Def13
.= (the
Comp of C
. ((the
Comp of C
. (hh,gg)),ff)) by
A8,
A10,
Def13
.= ((hh
(*) gg)
(*) ff) by
A14,
A15,
CAT_1:def 1;
end;
let a be
Object of C;
reconsider aa = a as
Element of (
CSp X);
reconsider ii = (
id$ aa) as
Morphism of C;
A17: (
cod ii)
= (
cod (
id$ aa)) by
Def12
.= aa;
(
dom ii)
= (
dom (
id$ aa)) by
Def11
.= aa;
then (
id$ aa)
in (
Hom (a,a)) by
A17;
hence (
Hom (a,a))
<>
{} ;
end;
end
Lm3: for a be
Element of (
CohCat X), aa be
Element of (
CSp X) st a
= aa holds for i be
Morphism of a, a st i
= (
id$ aa) holds for b be
Element of (
CohCat X) holds ((
Hom (a,b))
<>
{} implies for g be
Morphism of a, b holds (g
(*) i)
= g) & ((
Hom (b,a))
<>
{} implies for f be
Morphism of b, a holds (i
(*) f)
= f)
proof
let a be
Element of (
CohCat X), aa be
Element of (
CSp X) such that
A1: a
= aa;
let i be
Morphism of a, a such that
A2: i
= (
id$ aa);
let b be
Element of (
CohCat X);
thus (
Hom (a,b))
<>
{} implies for g be
Morphism of a, b holds (g
(*) i)
= g
proof
assume
A3: (
Hom (a,b))
<>
{} ;
let g be
Morphism of a, b;
reconsider gg = g as
Element of (
MapsC X);
(
Hom (a,a))
<>
{} ;
then
A4: (
cod i)
= a by
CAT_1: 5
.= (
dom g) by
A3,
CAT_1: 5;
A5: (
dom gg)
= (
dom g) by
Def11
.= aa by
A1,
A3,
CAT_1: 5;
then
A6: (
cod (
id$ aa))
= (
dom gg);
[g, i]
in (
dom the
Comp of (
CohCat X)) by
A4,
CAT_1:def 6;
hence (g
(*) i)
= (the
Comp of (
CohCat X)
. (g,i)) by
CAT_1:def 1
.= (gg
* (
id$ aa)) by
A6,
A2,
Def13
.= g by
A5,
Th25;
end;
thus (
Hom (b,a))
<>
{} implies for f be
Morphism of b, a holds (i
(*) f)
= f
proof
assume
A7: (
Hom (b,a))
<>
{} ;
let g be
Morphism of b, a;
reconsider gg = g as
Element of (
MapsC X);
(
Hom (a,a))
<>
{} ;
then
A8: (
dom i)
= a by
CAT_1: 5
.= (
cod g) by
A7,
CAT_1: 5;
A9: (
cod gg)
= (
cod g) by
Def12
.= aa by
A1,
A7,
CAT_1: 5;
then
A10: (
dom (
id$ aa))
= (
cod gg);
[i, g]
in (
dom the
Comp of (
CohCat X)) by
A8,
CAT_1:def 6;
hence (i
(*) g)
= (the
Comp of (
CohCat X)
. (i,g)) by
CAT_1:def 1
.= ((
id$ aa)
* gg) by
A2,
A10,
Def13
.= g by
A9,
Th25;
end;
end;
registration
let X;
cluster (
CohCat X) ->
with_identities;
coherence
proof
let a be
Element of (
CohCat X);
reconsider aa = a as
Element of (
CSp X);
reconsider ii = (
id$ aa) as
Morphism of (
CohCat X);
A1: (
cod ii)
= (
cod (
id$ aa)) by
Def12
.= aa;
(
dom ii)
= (
dom (
id$ aa)) by
Def11
.= aa;
then ii
in (
Hom (a,a)) by
A1;
then
reconsider ii as
Morphism of a, a by
CAT_1:def 5;
take ii;
thus thesis by
Lm3;
end;
end
begin
definition
let X be
set;
::
COH_SP:def16
func
Toler (X) ->
set means
:
Def15: x
in it iff x is
Tolerance of X;
existence
proof
defpred
P[
object] means $1 is
Tolerance of X;
consider a such that
A1: for x be
object holds x
in a iff x
in (
bool
[:X, X:]) &
P[x] from
XBOOLE_0:sch 1;
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 be
object;
A4:
now
assume x
in b;
then x is
Tolerance of X by
A3;
hence x
in a by
A2;
end;
now
assume x
in a;
then x is
Tolerance of X by
A2;
hence x
in b by
A3;
end;
hence x
in a iff x
in b by
A4;
end;
hence thesis by
TARSKI: 2;
end;
end
registration
let X be
set;
cluster (
Toler X) -> non
empty;
coherence
proof
set T = the
Tolerance of X;
T
in (
Toler X) by
Def15;
hence thesis;
end;
end
definition
let X be
set;
::
COH_SP:def17
func
Toler_on_subsets (X) ->
set equals (
union the set of all (
Toler Y) where Y be
Subset of X);
coherence ;
end
registration
let X be
set;
cluster (
Toler_on_subsets X) -> non
empty;
coherence
proof
set F = the set of all (
Toler Y) where Y be
Subset of X;
{}
c= X;
then
A1: (
Toler
{} )
in F;
{}
in (
Toler
{} ) by
Def15,
TOLER_1: 14;
hence thesis by
A1,
TARSKI:def 4;
end;
end
theorem ::
COH_SP:27
x
in (
Toler_on_subsets X) iff ex A st A
c= X & x is
Tolerance of A
proof
set f = the set of all (
Toler Y) where Y be
Subset of X;
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
consider a such that
A1: x
in a and
A2: a
in f by
TARSKI:def 4;
consider Y be
Subset of X such that
A3: a
= (
Toler Y) by
A2;
take Y;
thus thesis by
A1,
A3,
Def15;
end;
given A such that
A4: A
c= X and
A5: x is
Tolerance of A;
reconsider A as
Subset of X by
A4;
A6: (
Toler A)
in f;
x
in (
Toler A) by
A5,
Def15;
hence thesis by
A6,
TARSKI:def 4;
end;
theorem ::
COH_SP:28
(
Total a)
in (
Toler a) by
Def15;
theorem ::
COH_SP:29
Th28:
{}
in (
Toler_on_subsets X)
proof
set F = the set of all (
Toler Y) where Y be
Subset of X;
{}
c= X;
then
A1: (
Toler
{} )
in F;
{}
in (
Toler
{} ) by
Def15,
TOLER_1: 14;
hence thesis by
A1,
TARSKI:def 4;
end;
theorem ::
COH_SP:30
Th29: a
c= X implies (
Total a)
in (
Toler_on_subsets X)
proof
set F = the set of all (
Toler Y) where Y be
Subset of X;
assume a
c= X;
then
A1: (
Toler a)
in F;
(
Total a)
in (
Toler a) by
Def15;
hence thesis by
A1,
TARSKI:def 4;
end;
theorem ::
COH_SP:31
Th30: a
c= X implies (
id a)
in (
Toler_on_subsets X)
proof
set F = the set of all (
Toler Y) where Y be
Subset of X;
assume a
c= X;
then
A1: (
Toler a)
in F;
(
id a)
in (
Toler a) by
Def15;
hence thesis by
A1,
TARSKI:def 4;
end;
theorem ::
COH_SP:32
(
Total X)
in (
Toler_on_subsets X) by
Th29;
theorem ::
COH_SP:33
(
id X)
in (
Toler_on_subsets X) by
Th30;
definition
let X;
::
COH_SP:def18
func
TOL (X) ->
set equals {
[t, Y] where t be
Element of (
Toler_on_subsets X), Y be
Subset of X : t is
Tolerance of Y };
coherence ;
end
registration
let X;
cluster (
TOL X) -> non
empty;
coherence
proof
set FV = {
[t, Y] where t be
Element of (
Toler_on_subsets X), Y be
Subset of X : t is
Tolerance of Y };
now
reconsider o =
{} as
Subset of X by
XBOOLE_1: 2;
reconsider e =
{} as
Element of (
Toler_on_subsets X) by
Th28;
take m =
[e, o];
thus m
in FV by
TOLER_1: 14;
end;
hence thesis;
end;
end
reserve T,T1,T2 for
Element of (
TOL X);
theorem ::
COH_SP:34
[
{} ,
{} ]
in (
TOL X)
proof
{}
in (
Toler_on_subsets X) &
{}
c= X by
Th28;
hence thesis by
TOLER_1: 14;
end;
theorem ::
COH_SP:35
Th34: a
c= X implies
[(
id a), a]
in (
TOL X)
proof
assume
A1: a
c= X;
then (
id a)
in (
Toler_on_subsets X) by
Th30;
hence thesis by
A1;
end;
theorem ::
COH_SP:36
Th35: a
c= X implies
[(
Total a), a]
in (
TOL X)
proof
assume
A1: a
c= X;
then (
Total a)
in (
Toler_on_subsets X) by
Th29;
hence thesis by
A1;
end;
theorem ::
COH_SP:37
[(
id X), X]
in (
TOL X) by
Th34;
theorem ::
COH_SP:38
[(
Total X), X]
in (
TOL X) by
Th35;
definition
let X, T;
:: original:
`2
redefine
func T
`2 ->
Subset of X ;
coherence
proof
T
in {
[t, Y] where t be
Element of (
Toler_on_subsets X), Y be
Subset of X : t is
Tolerance of Y };
then
consider t be
Element of (
Toler_on_subsets X), Y be
Subset of X such that
A1: T
=
[t, Y] & t is
Tolerance of Y;
thus thesis by
A1;
end;
:: original:
`1
redefine
func T
`1 ->
Tolerance of (T
`2 ) ;
coherence
proof
T
in {
[t, Y] where t be
Element of (
Toler_on_subsets X), Y be
Subset of X : t is
Tolerance of Y };
then
consider t be
Element of (
Toler_on_subsets X), Y be
Subset of X such that
A2: T
=
[t, Y] and
A3: t is
Tolerance of Y;
thus thesis by
A2,
A3;
end;
end
definition
let X;
::
COH_SP:def19
func
FuncsT (X) ->
set equals (
union the set of all (
Funcs ((T
`2 ),(TT
`2 ))) where T be
Element of (
TOL X), TT be
Element of (
TOL X));
coherence ;
end
registration
let X;
cluster (
FuncsT X) -> non
empty
functional;
coherence
proof
set F = the set of all (
Funcs ((T
`2 ),(TT
`2 ))) where T be
Element of (
TOL X), TT be
Element of (
TOL X);
reconsider T =
[(
Total (
{} X)), (
{} X)] as
Element of (
TOL X) by
Th35;
A1: (
id (
{} X))
in (
Funcs ((T
`2 ),(T
`2 ))) by
FUNCT_2: 9;
(
Funcs ((T
`2 ),(T
`2 )))
in F;
then
reconsider UF = (
union F) as non
empty
set by
A1,
TARSKI:def 4;
now
let f be
object;
assume f
in UF;
then
consider C be
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;
end;
hence thesis by
FUNCT_1:def 13;
end;
end
reserve f for
Element of (
FuncsT X);
theorem ::
COH_SP:39
Th38: 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 = the set of all (
Funcs ((T
`2 ),(TT
`2 ))) where T be
Element of (
TOL X), TT be
Element of (
TOL X);
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 be
set such that
A1: x
in C and
A2: C
in F by
TARSKI:def 4;
consider A,B be
Element of (
TOL X) such that
A3: C
= (
Funcs ((A
`2 ),(B
`2 ))) by
A2;
take A, B;
thus thesis by
A1,
A3,
FUNCT_2: 66;
end;
given A,B be
Element of (
TOL X) such that
A4: ((B
`2 )
=
{} implies (A
`2 )
=
{} ) & x is
Function of (A
`2 ), (B
`2 );
A5: (
Funcs ((A
`2 ),(B
`2 )))
in F;
x
in (
Funcs ((A
`2 ),(B
`2 ))) by
A4,
FUNCT_2: 8;
hence thesis by
A5,
TARSKI:def 4;
end;
definition
let X;
::
COH_SP:def20
func
MapsT (X) ->
set equals {
[
[T, TT], f] where T be
Element of (
TOL X), TT be
Element of (
TOL X), f be
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
registration
let X;
cluster (
MapsT X) -> non
empty;
coherence
proof
set FV = {
[
[T, TT], f] where T be
Element of (
TOL X), TT be
Element of (
TOL X), f be
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
set a =
[(
Total (
{} X)), (
{} X)], f = (
id (a
`2 ));
take m =
[
[a, a], f];
reconsider a as
Element of (
TOL X) by
Th35;
(a
`2 )
=
{} implies (a
`2 )
=
{} ;
then
reconsider f as
Element of (
FuncsT X) by
Th38;
for x, y st
[x, y]
in (a
`1 ) holds
[(f
. x), (f
. y)]
in (a
`1 );
hence m
in FV;
end;
hence thesis;
end;
end
reserve m,m1,m2,m3 for
Element of (
MapsT X);
theorem ::
COH_SP:40
Th39: 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 {
[
[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 ) };
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 ::
COH_SP:41
Th40: for f be
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 that
A1: (T2
`2 )
=
{} implies (T1
`2 )
=
{} and
A2: for x, y st
[x, y]
in (T1
`1 ) holds
[(f
. x), (f
. y)]
in (T2
`1 );
reconsider f9 = f as
Element of (
FuncsT X) by
A1,
Th38;
for x, y st
[x, y]
in (T1
`1 ) holds
[(f9
. x), (f9
. y)]
in (T2
`1 ) by
A2;
hence thesis by
A1;
end;
registration
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] & ((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
Th39;
thus thesis by
A1;
end;
end
definition
let X, m;
::
COH_SP:def21
func
dom m ->
Element of (
TOL X) equals ((m
`1 )
`1 );
coherence
proof
consider f, T1, T2 such that
A1: m
=
[
[T1, T2], f] and (T2
`2 )
=
{} implies (T1
`2 )
=
{} and f is
Function of (T1
`2 ), (T2
`2 ) and for x, y st
[x, y]
in (T1
`1 ) holds
[(f
. x), (f
. y)]
in (T2
`1 ) by
Th39;
thus thesis by
A1;
end;
::
COH_SP:def22
func
cod m ->
Element of (
TOL X) equals ((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 )
=
{} and f is
Function of (T1
`2 ), (T2
`2 ) and for x, y st
[x, y]
in (T1
`1 ) holds
[(f
. x), (f
. y)]
in (T2
`1 ) by
Th39;
thus thesis by
A2;
end;
end
theorem ::
COH_SP:42
Th41: m
=
[
[(
dom m), (
cod m)], (m
`2 )]
proof
consider f, T1, T2 such that
A1: m
=
[
[T1, T2], f] and (T2
`2 )
=
{} implies (T1
`2 )
=
{} and f is
Function of (T1
`2 ), (T2
`2 ) and for x, y st
[x, y]
in (T1
`1 ) holds
[(f
. x), (f
. y)]
in (T2
`1 ) by
Th39;
thus thesis by
A1;
end;
Lm4: (m
`2 )
= (m1
`2 ) & (
dom m)
= (
dom m1) & (
cod m)
= (
cod m1) implies m
= m1
proof
m
=
[
[(
dom m), (
cod m)], (m
`2 )] by
Th41;
hence thesis by
Th41;
end;
definition
let X, T;
::
COH_SP:def23
func
id$ T ->
Element of (
MapsT X) equals
[
[T, T], (
id (T
`2 ))];
coherence
proof
set f = (
id (T
`2 ));
now
let x, y;
assume
A1:
[x, y]
in (T
`1 );
then x
in (T
`2 ) by
ZFMISC_1: 87;
then
A2: ((
id (T
`2 ))
. x)
= x by
FUNCT_1: 18;
y
in (T
`2 ) by
A1,
ZFMISC_1: 87;
hence
[(f
. x), (f
. y)]
in (T
`1 ) by
A1,
A2,
FUNCT_1: 18;
end;
hence thesis by
Th40;
end;
end
theorem ::
COH_SP:43
Th42: (((
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 ) and
A3: for x, y st
[x, y]
in (T1
`1 ) holds
[(f
. x), (f
. y)]
in (T2
`1 ) by
Th39;
A4: T2
= (
cod m) by
A1;
A5: f
= (m
`2 ) & T1
= (
dom m) by
A1;
thus (((
cod m)
`2 )
<>
{} or ((
dom m)
`2 )
=
{} ) & (m
`2 ) is
Function of ((
dom m)
`2 ), ((
cod m)
`2 ) by
A1,
A2;
let x, y;
assume
[x, y]
in ((
dom m)
`1 );
hence thesis by
A3,
A5,
A4;
end;
definition
let X, m1, m2;
assume
A1: (
cod m1)
= (
dom m2);
::
COH_SP:def24
func m2
* m1 ->
Element of (
MapsT X) equals
:
Def23:
[
[(
dom m1), (
cod m2)], ((m2
`2 )
* (m1
`2 ))];
coherence
proof
A2: ((
cod m2)
`2 )
<>
{} or ((
dom m2)
`2 )
=
{} by
Th42;
A3: ((
cod m1)
`2 )
<>
{} or ((
dom m1)
`2 )
=
{} by
Th42;
A4: (m1
`2 ) is
Function of ((
dom m1)
`2 ), ((
cod m1)
`2 ) by
Th42;
A5:
now
let x, y;
assume
A6:
[x, y]
in ((
dom m1)
`1 );
then x
in ((
dom m1)
`2 ) by
ZFMISC_1: 87;
then
A7: x
in (
dom (m1
`2 )) by
A3,
A4,
FUNCT_2:def 1;
y
in ((
dom m1)
`2 ) by
A6,
ZFMISC_1: 87;
then
A8: y
in (
dom (m1
`2 )) by
A3,
A4,
FUNCT_2:def 1;
[((m1
`2 )
. x), ((m1
`2 )
. y)]
in ((
cod m1)
`1 ) by
A6,
Th42;
then
[((m2
`2 )
. ((m1
`2 )
. x)), ((m2
`2 )
. ((m1
`2 )
. y))]
in ((
cod m2)
`1 ) by
A1,
Th42;
then
[(((m2
`2 )
* (m1
`2 ))
. x), ((m2
`2 )
. ((m1
`2 )
. y))]
in ((
cod m2)
`1 ) by
A7,
FUNCT_1: 13;
hence
[(((m2
`2 )
* (m1
`2 ))
. x), (((m2
`2 )
* (m1
`2 ))
. y)]
in ((
cod m2)
`1 ) by
A8,
FUNCT_1: 13;
end;
(m2
`2 ) is
Function of ((
dom m2)
`2 ), ((
cod m2)
`2 ) by
Th42;
then ((m2
`2 )
* (m1
`2 )) is
Function of ((
dom m1)
`2 ), ((
cod m2)
`2 ) by
A1,
A3,
A4,
FUNCT_2: 13;
hence thesis by
A1,
A3,
A2,
A5,
Th40;
end;
end
theorem ::
COH_SP:44
Th43: (
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
Def23
.=
[
[(
dom (m2
* m1)), (
cod (m2
* m1))], ((m2
* m1)
`2 )] by
Th41;
hence thesis by
Lm2,
XTUPLE_0: 1;
end;
theorem ::
COH_SP:45
Th44: (
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);
A3: (
cod (m2
* m1))
= (
cod m2) by
A1,
Th43;
((m2
* m1)
`2 )
= ((m2
`2 )
* (m1
`2 )) by
A1,
Th43;
then
A4: ((m3
* (m2
* m1))
`2 )
= ((m3
`2 )
* ((m2
`2 )
* (m1
`2 ))) by
A2,
A3,
Th43;
A5: (
dom (m3
* m2))
= (
dom m2) by
A2,
Th43;
then
A6: (
dom ((m3
* m2)
* m1))
= (
dom m1) by
A1,
Th43;
(
dom (m2
* m1))
= (
dom m1) by
A1,
Th43;
then
A7: (
dom (m3
* (m2
* m1)))
= (
dom m1) by
A2,
A3,
Th43;
(
cod (m3
* m2))
= (
cod m3) by
A2,
Th43;
then
A8: (
cod ((m3
* m2)
* m1))
= (
cod m3) by
A1,
A5,
Th43;
((m3
* m2)
`2 )
= ((m3
`2 )
* (m2
`2 )) by
A2,
Th43;
then
A9: (((m3
* m2)
* m1)
`2 )
= (((m3
`2 )
* (m2
`2 ))
* (m1
`2 )) by
A1,
A5,
Th43;
(
cod (m3
* (m2
* m1)))
= (
cod m3) by
A2,
A3,
Th43;
hence thesis by
A4,
A7,
A9,
A6,
A8,
Lm4,
RELAT_1: 36;
end;
theorem ::
COH_SP:46
((
id$ T)
`2 )
= (
id (T
`2 )) & (
dom (
id$ T))
= T & (
cod (
id$ T))
= T;
theorem ::
COH_SP:47
Th46: (m
* (
id$ (
dom m)))
= m & ((
id$ (
cod m))
* m)
= m
proof
set i1 = (
id$ (
dom m)), i2 = (
id$ (
cod m));
A1: (m
`2 ) is
Function of ((
dom m)
`2 ), ((
cod m)
`2 ) by
Th42;
then
A2: (
rng (m
`2 ))
c= ((
cod m)
`2 ) by
RELAT_1:def 19;
((
cod m)
`2 )
<>
{} or ((
dom m)
`2 )
=
{} by
Th42;
then
A3: (
dom (m
`2 ))
= ((
dom m)
`2 ) by
A1,
FUNCT_2:def 1;
A4: (
cod i1)
= (
dom m);
then
A5: (
cod (m
* i1))
= (
cod m) by
Th43;
((m
* i1)
`2 )
= ((m
`2 )
* (i1
`2 )) & (
dom (m
* i1))
= (
dom i1) by
A4,
Th43;
hence (m
* i1)
= m by
A3,
A5,
Lm4,
RELAT_1: 52;
A6: (
dom i2)
= (
cod m);
then
A7: (
cod (i2
* m))
= (
cod i2) by
Th43;
((i2
* m)
`2 )
= ((i2
`2 )
* (m
`2 )) & (
dom (i2
* m))
= (
dom m) by
A6,
Th43;
hence thesis by
A2,
A7,
Lm4,
RELAT_1: 53;
end;
definition
let X;
::
COH_SP:def25
func
fDom X ->
Function of (
MapsT X), (
TOL X) means
:
Def24: for m holds (it
. m)
= (
dom m);
existence
proof
deffunc
F(
Element of (
MapsT X)) = (
dom $1);
thus ex f be
Function of (
MapsT X), (
TOL X) st for x be
Element of (
MapsT X) holds (f
. x)
=
F(x) from
FUNCT_2:sch 4;
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: 63;
end;
::
COH_SP:def26
func
fCod X ->
Function of (
MapsT X), (
TOL X) means
:
Def25: for m holds (it
. m)
= (
cod m);
existence
proof
deffunc
F(
Element of (
MapsT X)) = (
cod $1);
thus ex f be
Function of (
MapsT X), (
TOL X) st for x be
Element of (
MapsT X) holds (f
. x)
=
F(x) from
FUNCT_2:sch 4;
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: 63;
end;
::
COH_SP:def27
func
fComp X ->
PartFunc of
[:(
MapsT X), (
MapsT X):], (
MapsT X) means
:
Def26: (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[
object,
object,
object] means for m2, m1 st m2
= $1 & m1
= $2 holds (
dom m2)
= (
cod m1) & $3
= (m2
* m1);
A5: for x,y,z1,z2 be
object 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
object;
assume x
in (
MapsT X) & y
in (
MapsT X);
then
reconsider m2 = x, m1 = y as
Element of (
MapsT X);
assume that
A6:
P[x, y, z1] and
A7:
P[x, y, z2];
z1
= (m2
* m1) by
A6;
hence thesis by
A7;
end;
A8: for x,y,z be
object st x
in (
MapsT X) & y
in (
MapsT X) &
P[x, y, z] holds z
in (
MapsT X)
proof
let x,y,z be
object;
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;
consider h be
PartFunc of
[:(
MapsT X), (
MapsT X):], (
MapsT X) such that
A9: for x,y be
object holds
[x, y]
in (
dom h) iff x
in (
MapsT X) & y
in (
MapsT X) & ex z be
object st
P[x, y, z] and
A10: for x,y be
object st
[x, y]
in (
dom h) holds
P[x, y, (h
. (x,y))] from
BINOP_1:sch 5(
A8,
A5);
take h;
thus
A11: 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 be
object st
P[m2, m1, z] by
A9;
hence thesis;
end;
assume (
dom m2)
= (
cod m1);
then
P[m2, m1, (m2
* m1)];
hence thesis by
A9;
end;
let m2, m1;
assume (
dom m2)
= (
cod m1);
then
[m2, m1]
in (
dom h) by
A11;
then
P[m2, m1, (h
. (m2,m1))] by
A10;
hence thesis;
end;
uniqueness
proof
let h1,h2 be
PartFunc of
[:(
MapsT X), (
MapsT X):], (
MapsT X) such that
A12: for m2, m1 holds
[m2, m1]
in (
dom h1) iff (
dom m2)
= (
cod m1) and
A13: for m2, m1 st (
dom m2)
= (
cod m1) holds (h1
.
[m2, m1])
= (m2
* m1) and
A14: for m2, m1 holds
[m2, m1]
in (
dom h2) iff (
dom m2)
= (
cod m1) and
A15: for m2, m1 st (
dom m2)
= (
cod m1) holds (h2
.
[m2, m1])
= (m2
* m1);
A16: (
dom h1)
= (
dom h2)
proof
let x,y be
object;
thus
[x, y]
in (
dom h1) implies
[x, y]
in (
dom h2)
proof
assume
A17:
[x, y]
in (
dom h1);
then
reconsider m2 = x, m1 = y as
Element of (
MapsT X) by
ZFMISC_1: 87;
(
dom m2)
= (
cod m1) by
A12,
A17;
hence thesis by
A14;
end;
assume
A18:
[x, y]
in (
dom h2);
then
reconsider m2 = x, m1 = y as
Element of (
MapsT X) by
ZFMISC_1: 87;
(
dom m2)
= (
cod m1) by
A14,
A18;
hence thesis by
A12;
end;
now
let m be
Element of
[:(
MapsT X), (
MapsT X):] such that
A19: m
in (
dom h1);
consider m2,m1 be
Element of (
MapsT X) such that
A20: m
=
[m2, m1] by
DOMAIN_1: 1;
A21: (
dom m2)
= (
cod m1) by
A12,
A19,
A20;
then (h1
.
[m2, m1])
= (m2
* m1) by
A13;
hence (h1
. m)
= (h2
. m) by
A15,
A20,
A21;
end;
hence thesis by
A16,
PARTFUN1: 5;
end;
end
definition
::$Canceled
let X;
::
COH_SP:def29
func
TolCat (X) -> non
empty non
void
strict
CatStr equals
CatStr (# (
TOL X), (
MapsT X), (
fDom X), (
fCod X), (
fComp X) #);
coherence ;
end
registration
let X;
cluster (
TolCat X) ->
Category-like
transitive
associative
reflexive;
coherence
proof
set C = (
TolCat X);
set M = (
MapsT X), d = (
fDom X), c = (
fCod X), p = (
fComp X);
thus
A1: C is
Category-like
proof
let ff,gg be
Morphism of C;
reconsider f = ff, g = gg as
Element of M;
(d
. g)
= (
dom g) & (c
. f)
= (
cod f) by
Def24,
Def25;
hence thesis by
Def26;
end;
thus
A2: C is
transitive
proof
let ff,gg be
Morphism of C such that
A3: (
dom gg)
= (
cod ff);
[gg, ff]
in (
dom the
Comp of C) by
A3,
A1;
then
A4: (the
Comp of C
. (gg,ff))
= (gg
(*) ff) by
CAT_1:def 1;
reconsider f = ff, g = gg as
Element of M;
A5: (d
. g)
= (
dom g) & (c
. f)
= (
cod f) by
Def24,
Def25;
then
A6: (p
.
[g, f])
= (g
* f) by
A3,
Def26;
A7: (d
. f)
= (
dom f) & (c
. g)
= (
cod g) by
Def24,
Def25;
(
dom (g
* f))
= (
dom f) & (
cod (g
* f))
= (
cod g) by
A3,
A5,
Th43;
hence thesis by
A6,
A7,
Def24,
Def25,
A4;
end;
thus C is
associative
proof
let ff,gg,hh be
Morphism of C such that
A8: (
dom hh)
= (
cod gg) and
A9: (
dom gg)
= (
cod ff);
reconsider f = ff, g = gg, h = hh as
Element of M;
A10: (
dom h)
= (d
. h) & (
cod g)
= (c
. g) by
Def24,
Def25;
then
A11: (
dom (h
* g))
= (
dom g) by
A8,
Th43;
A12: (
dom g)
= (d
. g) & (
cod f)
= (c
. f) by
Def24,
Def25;
then
A13: (
cod (g
* f))
= (
dom h) by
A8,
A9,
A10,
Th43;
[hh, gg]
in (
dom the
Comp of C) by
A8,
A1;
then
A14: (hh
(*) gg)
= (the
Comp of C
. (hh,gg)) by
CAT_1:def 1;
[gg, ff]
in (
dom the
Comp of C) by
A9,
A1;
then
A15: (gg
(*) ff)
= (the
Comp of C
. (gg,ff)) by
CAT_1:def 1;
(
dom (hh
(*) gg))
= (
dom gg) by
A2,
A8;
then
A16:
[(hh
(*) gg), ff]
in (
dom the
Comp of C) by
A1,
A9;
(
cod (gg
(*) ff))
= (
cod gg) by
A2,
A9;
then
[hh, (gg
(*) ff)]
in (
dom the
Comp of C) by
A1,
A8;
hence (hh
(*) (gg
(*) ff))
= (the
Comp of C
. (hh,(the
Comp of C
. (gg,ff)))) by
A15,
CAT_1:def 1
.= (p
.
[h, (g
* f)]) by
A9,
A12,
Def26
.= (h
* (g
* f)) by
A13,
Def26
.= ((h
* g)
* f) by
A8,
A9,
A10,
A12,
Th44
.= (p
.
[(h
* g), f]) by
A9,
A12,
A11,
Def26
.= (the
Comp of C
. ((the
Comp of C
. (hh,gg)),ff)) by
A8,
A10,
Def26
.= ((hh
(*) gg)
(*) ff) by
A14,
A16,
CAT_1:def 1;
end;
let a be
Object of C;
reconsider aa = a as
Element of (
TOL X);
reconsider ii = (
id$ aa) as
Morphism of C;
A17: (
cod ii)
= (
cod (
id$ aa)) by
Def25
.= aa;
(
dom ii)
= (
dom (
id$ aa)) by
Def24
.= aa;
then (
id$ aa)
in (
Hom (a,a)) by
A17;
hence (
Hom (a,a))
<>
{} ;
end;
end
Lm5: for a be
Element of (
TolCat X), aa be
Element of (
TOL X) st a
= aa holds for i be
Morphism of a, a st i
= (
id$ aa) holds for b be
Element of (
TolCat X) holds ((
Hom (a,b))
<>
{} implies for g be
Morphism of a, b holds (g
(*) i)
= g) & ((
Hom (b,a))
<>
{} implies for f be
Morphism of b, a holds (i
(*) f)
= f)
proof
let a be
Element of (
TolCat X), aa be
Element of (
TOL X) such that
A1: a
= aa;
let i be
Morphism of a, a such that
A2: i
= (
id$ aa);
let b be
Element of (
TolCat X);
thus (
Hom (a,b))
<>
{} implies for g be
Morphism of a, b holds (g
(*) i)
= g
proof
assume
A3: (
Hom (a,b))
<>
{} ;
let g be
Morphism of a, b;
reconsider gg = g as
Element of (
MapsT X);
(
Hom (a,a))
<>
{} ;
then
A4: (
cod i)
= a by
CAT_1: 5
.= (
dom g) by
A3,
CAT_1: 5;
A5: (
dom gg)
= (
dom g) by
Def24
.= aa by
A1,
A3,
CAT_1: 5;
then
A6: (
cod (
id$ aa))
= (
dom gg);
[g, i]
in (
dom the
Comp of (
TolCat X)) by
A4,
CAT_1:def 6;
hence (g
(*) i)
= (the
Comp of (
TolCat X)
. (g,i)) by
CAT_1:def 1
.= (gg
* (
id$ aa)) by
A6,
A2,
Def26
.= g by
A5,
Th46;
end;
thus (
Hom (b,a))
<>
{} implies for f be
Morphism of b, a holds (i
(*) f)
= f
proof
assume
A7: (
Hom (b,a))
<>
{} ;
let g be
Morphism of b, a;
reconsider gg = g as
Element of (
MapsT X);
(
Hom (a,a))
<>
{} ;
then
A8: (
dom i)
= a by
CAT_1: 5
.= (
cod g) by
A7,
CAT_1: 5;
A9: (
cod gg)
= (
cod g) by
Def25
.= aa by
A1,
A7,
CAT_1: 5;
then
A10: (
dom (
id$ aa))
= (
cod gg);
[i, g]
in (
dom the
Comp of (
TolCat X)) by
A8,
CAT_1:def 6;
hence (i
(*) g)
= (the
Comp of (
TolCat X)
. (i,g)) by
CAT_1:def 1
.= ((
id$ aa)
* gg) by
A2,
A10,
Def26
.= g by
A9,
Th46;
end;
end;
registration
let X;
cluster (
TolCat X) ->
with_identities;
coherence
proof
let a be
Element of (
TolCat X);
reconsider aa = a as
Element of (
TOL X);
reconsider ii = (
id$ aa) as
Morphism of (
TolCat X);
A1: (
cod ii)
= (
cod (
id$ aa)) by
Def25
.= aa;
(
dom ii)
= (
dom (
id$ aa)) by
Def24
.= aa;
then ii
in (
Hom (a,a)) by
A1;
then
reconsider ii as
Morphism of a, a by
CAT_1:def 5;
take ii;
thus thesis by
Lm5;
end;
end