:: Basic Operations on Preordered Coherent Spaces
:: by Klaus E. Grue and Artur Korni{\l}owicz
::
:: Received August 28, 2007
:: Copyright (c) 2007 Association of Mizar Users
reconsider z = 0 , j = 1 as Element of {0 ,1} by TARSKI:def 2;
Lm1:
now
let R1,
S1 be
set ;
:: thesis: for R being Relation of R1
for S being Relation of S1 st R1 misses S1 holds
for q1, q2 being set st [q1,q2] in R \/ S & q2 in S1 holds
( [q1,q2] in S & q1 in S1 )let R be
Relation of
R1;
:: thesis: for S being Relation of S1 st R1 misses S1 holds
for q1, q2 being set st [q1,q2] in R \/ S & q2 in S1 holds
( [q1,q2] in S & q1 in S1 )let S be
Relation of
S1;
:: thesis: ( R1 misses S1 implies for q1, q2 being set st [q1,q2] in R \/ S & q2 in S1 holds
( [q1,q2] in S & q1 in S1 ) )assume A1:
R1 misses S1
;
:: thesis: for q1, q2 being set st [q1,q2] in R \/ S & q2 in S1 holds
( [q1,q2] in S & q1 in S1 )let q1,
q2 be
set ;
:: thesis: ( [q1,q2] in R \/ S & q2 in S1 implies ( [q1,q2] in S & q1 in S1 ) )assume that A2:
[q1,q2] in R \/ S
and A3:
q2 in S1
;
:: thesis: ( [q1,q2] in S & q1 in S1 )A4:
(
[q1,q2] in R or
[q1,q2] in S )
by A2, XBOOLE_0:def 3;
hence
(
[q1,q2] in S &
q1 in S1 )
by A4, ZFMISC_1:106;
:: thesis: verum
end;
theorem Th1: :: PCS_0:1
:: deftheorem Def1 defines Carrier PCS_0:def 1 :
definition
let R1,
R2,
S1,
S2 be
set ;
let R be
Relation of
R1,
R2;
let S be
Relation of
S1,
S2;
defpred S1[
set ,
set ]
means ex
r1,
s1,
r2,
s2 being
set st
( $1
= [r1,s1] & $2
= [r2,s2] &
r1 in R1 &
s1 in S1 &
r2 in R2 &
s2 in S2 & (
[r1,r2] in R or
[s1,s2] in S ) );
func [^R,S^] -> Relation of
[:R1,S1:],
[:R2,S2:] means :
Def2:
:: PCS_0:def 2
for
x,
y being
set holds
(
[x,y] in it iff ex
r1,
s1,
r2,
s2 being
set st
(
x = [r1,s1] &
y = [r2,s2] &
r1 in R1 &
s1 in S1 &
r2 in R2 &
s2 in S2 & (
[r1,r2] in R or
[s1,s2] in S ) ) );
existence
ex b1 being Relation of [:R1,S1:],[:R2,S2:] st
for x, y being set holds
( [x,y] in b1 iff ex r1, s1, r2, s2 being set st
( x = [r1,s1] & y = [r2,s2] & r1 in R1 & s1 in S1 & r2 in R2 & s2 in S2 & ( [r1,r2] in R or [s1,s2] in S ) ) )
uniqueness
for b1, b2 being Relation of [:R1,S1:],[:R2,S2:] st ( for x, y being set holds
( [x,y] in b1 iff ex r1, s1, r2, s2 being set st
( x = [r1,s1] & y = [r2,s2] & r1 in R1 & s1 in S1 & r2 in R2 & s2 in S2 & ( [r1,r2] in R or [s1,s2] in S ) ) ) ) & ( for x, y being set holds
( [x,y] in b2 iff ex r1, s1, r2, s2 being set st
( x = [r1,s1] & y = [r2,s2] & r1 in R1 & s1 in S1 & r2 in R2 & s2 in S2 & ( [r1,r2] in R or [s1,s2] in S ) ) ) ) holds
b1 = b2
end;
:: deftheorem Def2 defines [^ PCS_0:def 2 :
for
R1,
R2,
S1,
S2 being
set for
R being
Relation of
R1,
R2 for
S being
Relation of
S1,
S2 for
b7 being
Relation of
[:R1,S1:],
[:R2,S2:] holds
(
b7 = [^R,S^] iff for
x,
y being
set holds
(
[x,y] in b7 iff ex
r1,
s1,
r2,
s2 being
set st
(
x = [r1,s1] &
y = [r2,s2] &
r1 in R1 &
s1 in S1 &
r2 in R2 &
s2 in S2 & (
[r1,r2] in R or
[s1,s2] in S ) ) ) );
definition
let R1,
R2,
S1,
S2 be non
empty set ;
let R be
Relation of
R1,
R2;
let S be
Relation of
S1,
S2;
redefine func [^R,S^] means :
Def3:
:: PCS_0:def 3
for
r1 being
Element of
R1 for
r2 being
Element of
R2 for
s1 being
Element of
S1 for
s2 being
Element of
S2 holds
(
[[r1,s1],[r2,s2]] in it iff (
[r1,r2] in R or
[s1,s2] in S ) );
compatibility
for b1 being Relation of [:R1,S1:],[:R2,S2:] holds
( b1 = [^R,S^] iff for r1 being Element of R1
for r2 being Element of R2
for s1 being Element of S1
for s2 being Element of S2 holds
( [[r1,s1],[r2,s2]] in b1 iff ( [r1,r2] in R or [s1,s2] in S ) ) )
end;
:: deftheorem Def3 defines [^ PCS_0:def 3 :
for
R1,
R2,
S1,
S2 being non
empty set for
R being
Relation of
R1,
R2 for
S being
Relation of
S1,
S2 for
b7 being
Relation of
[:R1,S1:],
[:R2,S2:] holds
(
b7 = [^R,S^] iff for
r1 being
Element of
R1 for
r2 being
Element of
R2 for
s1 being
Element of
S1 for
s2 being
Element of
S2 holds
(
[[r1,s1],[r2,s2]] in b7 iff (
[r1,r2] in R or
[s1,s2] in S ) ) );
:: deftheorem Def4 defines transitive-yielding PCS_0:def 4 :
:: deftheorem Def5 defines pcs-InternalRels PCS_0:def 5 :
:: deftheorem Def6 defines pcs-InternalRels PCS_0:def 6 :
:: deftheorem Def7 defines (--) PCS_0:def 7 :
:: deftheorem Def8 defines pcs-tol-total PCS_0:def 8 :
:: deftheorem Def9 defines pcs-tol-reflexive PCS_0:def 9 :
:: deftheorem Def10 defines pcs-tol-irreflexive PCS_0:def 10 :
:: deftheorem Def11 defines pcs-tol-symmetric PCS_0:def 11 :
:: deftheorem defines emptyTolStr PCS_0:def 12 :
theorem Th2: :: PCS_0:2
:: deftheorem Def13 defines TolStr-yielding PCS_0:def 13 :
:: deftheorem Def14 defines TolStr-yielding PCS_0:def 14 :
:: deftheorem defines TolStr-yielding PCS_0:def 15 :
:: deftheorem Def16 defines pcs-tol-reflexive-yielding PCS_0:def 16 :
:: deftheorem Def17 defines pcs-tol-irreflexive-yielding PCS_0:def 17 :
:: deftheorem Def18 defines pcs-tol-symmetric-yielding PCS_0:def 18 :
:: deftheorem Def19 defines pcs-ToleranceRels PCS_0:def 19 :
:: deftheorem Def20 defines pcs-ToleranceRels PCS_0:def 20 :
theorem Th3: :: PCS_0:3
theorem Th4: :: PCS_0:4
theorem Th5: :: PCS_0:5
:: deftheorem defines [^ PCS_0:def 21 :
Lm2:
for x, a1, a2, b1, b2 being set st x = [[a1,a2],[b1,b2]] holds
( (x `1 ) `1 = a1 & (x `1 ) `2 = a2 & (x `2 ) `1 = b1 & (x `2 ) `2 = b2 )
theorem Th6: :: PCS_0:6
theorem :: PCS_0:7
:: deftheorem Def22 defines pcs-compatible PCS_0:def 22 :
:: deftheorem Def23 defines pcs-like PCS_0:def 23 :
:: deftheorem Def24 defines anti-pcs-like PCS_0:def 24 :
:: deftheorem defines pcs-total PCS_0:def 25 :
:: deftheorem defines pcs-empty PCS_0:def 26 :
:: deftheorem defines pcs-singleton PCS_0:def 27 :
:: deftheorem Def28 defines pcs-Str-yielding PCS_0:def 28 :
:: deftheorem Def29 defines pcs-yielding PCS_0:def 29 :
:: deftheorem Def30 defines pcs-Str-yielding PCS_0:def 30 :
:: deftheorem Def31 defines pcs-yielding PCS_0:def 31 :
:: deftheorem Def32 defines pcs-Str-yielding PCS_0:def 32 :
:: deftheorem Def33 defines pcs-yielding PCS_0:def 33 :
:: deftheorem Def34 defines c= PCS_0:def 34 :
theorem Th8: :: PCS_0:8
theorem Th9: :: PCS_0:9
Lm3:
for P, Q being pcs-Str
for p being set st p in the carrier of P & P c= Q holds
p is Element of Q
:: deftheorem Def35 defines pcs-chain-like PCS_0:def 35 :
:: deftheorem Def36 defines pcs-union PCS_0:def 36 :
theorem Th10: :: PCS_0:10
theorem :: PCS_0:11
theorem Th12: :: PCS_0:12
theorem :: PCS_0:13
:: deftheorem defines MSSet PCS_0:def 37 :
:: deftheorem defines pcs-sum PCS_0:def 38 :
deffunc H1( pcs-Str , pcs-Str ) -> pcs-Str = pcs-Str(# (the carrier of $1 \/ the carrier of $2),(the InternalRel of $1 \/ the InternalRel of $2),(the ToleranceRel of $1 \/ the ToleranceRel of $2) #);
theorem Th14: :: PCS_0:14
theorem Th15: :: PCS_0:15
theorem :: PCS_0:16
theorem :: PCS_0:17
theorem Th18: :: PCS_0:18
theorem Th19: :: PCS_0:19
theorem :: PCS_0:20
definition
let P be
pcs-Str ;
let a be
set ;
func pcs-extension P,
a -> strict pcs-Str means :
Def39:
:: PCS_0:def 39
( the
carrier of
it = {a} \/ the
carrier of
P & the
InternalRel of
it = [:{a},the carrier of it:] \/ the
InternalRel of
P & the
ToleranceRel of
it = ([:{a},the carrier of it:] \/ [:the carrier of it,{a}:]) \/ the
ToleranceRel of
P );
existence
ex b1 being strict pcs-Str st
( the carrier of b1 = {a} \/ the carrier of P & the InternalRel of b1 = [:{a},the carrier of b1:] \/ the InternalRel of P & the ToleranceRel of b1 = ([:{a},the carrier of b1:] \/ [:the carrier of b1,{a}:]) \/ the ToleranceRel of P )
uniqueness
for b1, b2 being strict pcs-Str st the carrier of b1 = {a} \/ the carrier of P & the InternalRel of b1 = [:{a},the carrier of b1:] \/ the InternalRel of P & the ToleranceRel of b1 = ([:{a},the carrier of b1:] \/ [:the carrier of b1,{a}:]) \/ the ToleranceRel of P & the carrier of b2 = {a} \/ the carrier of P & the InternalRel of b2 = [:{a},the carrier of b2:] \/ the InternalRel of P & the ToleranceRel of b2 = ([:{a},the carrier of b2:] \/ [:the carrier of b2,{a}:]) \/ the ToleranceRel of P holds
b1 = b2
;
end;
:: deftheorem Def39 defines pcs-extension PCS_0:def 39 :
theorem Th21: :: PCS_0:21
theorem :: PCS_0:22
theorem Th23: :: PCS_0:23
theorem Th24: :: PCS_0:24
theorem Th25: :: PCS_0:25
theorem Th26: :: PCS_0:26
theorem Th27: :: PCS_0:27
theorem Th28: :: PCS_0:28
theorem Th29: :: PCS_0:29
theorem Th30: :: PCS_0:30
theorem Th31: :: PCS_0:31
theorem :: PCS_0:32
:: deftheorem Def40 defines pcs-reverse PCS_0:def 40 :
theorem Th33: :: PCS_0:33
theorem Th34: :: PCS_0:34
theorem Th35: :: PCS_0:35
definition
let P,
Q be
pcs-Str ;
func P pcs-times Q -> pcs-Str equals :: PCS_0:def 41
pcs-Str(#
[:the carrier of P,the carrier of Q:],
["the InternalRel of P,the InternalRel of Q"],
[^the ToleranceRel of P,the ToleranceRel of Q^] #);
coherence
pcs-Str(# [:the carrier of P,the carrier of Q:],["the InternalRel of P,the InternalRel of Q"],[^the ToleranceRel of P,the ToleranceRel of Q^] #) is pcs-Str
;
end;
:: deftheorem defines pcs-times PCS_0:def 41 :
theorem :: PCS_0:36
theorem :: PCS_0:37
theorem Th38: :: PCS_0:38
:: deftheorem defines --> PCS_0:def 42 :
theorem :: PCS_0:39
theorem :: PCS_0:40
theorem :: PCS_0:41
:: deftheorem Def43 defines pcs-self-coherent PCS_0:def 43 :
:: deftheorem Def44 defines pcs-self-coherent-membered PCS_0:def 44 :
definition
let P be
RelStr ;
let D be
set ;
defpred S1[
set ,
set ]
means ( $1
in D & $2
in D & ( for
a being
set st
a in $1 holds
ex
b being
set st
(
b in $2 &
[a,b] in the
InternalRel of
P ) ) );
func pcs-general-power-IR P,
D -> Relation of
D means :
Def45:
:: PCS_0:def 45
for
A,
B being
set holds
(
[A,B] in it iff (
A in D &
B in D & ( for
a being
set st
a in A holds
ex
b being
set st
(
b in B &
[a,b] in the
InternalRel of
P ) ) ) );
existence
ex b1 being Relation of D st
for A, B being set holds
( [A,B] in b1 iff ( A in D & B in D & ( for a being set st a in A holds
ex b being set st
( b in B & [a,b] in the InternalRel of P ) ) ) )
uniqueness
for b1, b2 being Relation of D st ( for A, B being set holds
( [A,B] in b1 iff ( A in D & B in D & ( for a being set st a in A holds
ex b being set st
( b in B & [a,b] in the InternalRel of P ) ) ) ) ) & ( for A, B being set holds
( [A,B] in b2 iff ( A in D & B in D & ( for a being set st a in A holds
ex b being set st
( b in B & [a,b] in the InternalRel of P ) ) ) ) ) holds
b1 = b2
end;
:: deftheorem Def45 defines pcs-general-power-IR PCS_0:def 45 :
definition
let P be
TolStr ;
let D be
set ;
defpred S1[
set ,
set ]
means ( $1
in D & $2
in D & ( for
a,
b being
set st
a in $1 &
b in $2 holds
[a,b] in the
ToleranceRel of
P ) );
func pcs-general-power-TR P,
D -> Relation of
D means :
Def46:
:: PCS_0:def 46
for
A,
B being
set holds
(
[A,B] in it iff (
A in D &
B in D & ( for
a,
b being
set st
a in A &
b in B holds
[a,b] in the
ToleranceRel of
P ) ) );
existence
ex b1 being Relation of D st
for A, B being set holds
( [A,B] in b1 iff ( A in D & B in D & ( for a, b being set st a in A & b in B holds
[a,b] in the ToleranceRel of P ) ) )
uniqueness
for b1, b2 being Relation of D st ( for A, B being set holds
( [A,B] in b1 iff ( A in D & B in D & ( for a, b being set st a in A & b in B holds
[a,b] in the ToleranceRel of P ) ) ) ) & ( for A, B being set holds
( [A,B] in b2 iff ( A in D & B in D & ( for a, b being set st a in A & b in B holds
[a,b] in the ToleranceRel of P ) ) ) ) holds
b1 = b2
end;
:: deftheorem Def46 defines pcs-general-power-TR PCS_0:def 46 :
theorem :: PCS_0:42
theorem :: PCS_0:43
:: deftheorem defines pcs-general-power PCS_0:def 47 :
theorem Th44: :: PCS_0:44
theorem :: PCS_0:45
theorem Th46: :: PCS_0:46
theorem :: PCS_0:47
:: deftheorem defines pcs-coherent-power PCS_0:def 48 :
theorem Th48: :: PCS_0:48
:: deftheorem defines pcs-power PCS_0:def 49 :