:: Basic Operations on Preordered Coherent Spaces
:: by Klaus E. Grue and Artur Korni{\l}owicz
::
:: Received August 28, 2007
:: Copyright (c) 2007-2021 Association of Mizar Users

reconsider z = 0 , j = 1 as Element of {0,1} by TARSKI:def 2;

definition

let R1, R2 be set ;
let R be Relation of R1,R2;
:: original: field
redefine func field R -> Subset of (R1 \/ R2);
coherence
field R is Subset of (R1 \/ R2) by RELSET_1:8;

end;

definition

let R1, R2, S1, S2 be set ;
let R be Relation of R1,R2;
let S be Relation of S1,S2;
:: original: \/
redefine func R \/ S -> Relation of (R1 \/ S1),(R2 \/ S2);
coherence
R \/ S is Relation of (R1 \/ S1),(R2 \/ S2) by ZFMISC_1:119;

end;

registration

let R1, S1 be set ;
let R be total Relation of R1;
let S be total Relation of S1;

cluster R \/ S -> total for Relation of (R1 \/ S1);

coherence
for b₁ being Relation of (R1 \/ S1) st b₁ = R \/ S holds
b₁ is total

proof end;

end;

registration

let R1, S1 be set ;
let R be reflexive Relation of R1;
let S be reflexive Relation of S1;

cluster R \/ S -> reflexive for Relation of (R1 \/ S1);

coherence
for b₁ being Relation of (R1 \/ S1) st b₁ = R \/ S holds
b₁ is reflexive ;

end;

registration

let R1, S1 be set ;
let R be symmetric Relation of R1;
let S be symmetric Relation of S1;

cluster R \/ S -> symmetric for Relation of (R1 \/ S1);

coherence
for b₁ being Relation of (R1 \/ S1) st b₁ = R \/ S holds
b₁ is symmetric ;

end;

Lm1: now :: thesis: for R1, S1 being set
for R being Relation of R1
for S being Relation of S1 st R1 misses S1 holds
for q1, q2 being object st [q1,q2] in R \/ S & q2 in S1 holds
( [q1,q2] in S & q1 in S1 )

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 object 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 object 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 object 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 object st [q1,q2] in R \/ S & q2 in S1 holds
( [q1,q2] in S & q1 in S1 )
let q1, q2 be object ; :: 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;

now :: thesis: not [q1,q2] in R

assume [q1,q2] in R ; :: thesis: contradiction
then q2 in R1 by ZFMISC_1:87;
hence contradiction by A1, A3, XBOOLE_0:3; :: thesis: verum

end;

hence ( [q1,q2] in S & q1 in S1 ) by A4, ZFMISC_1:87; :: thesis: verum

end;

theorem Th1: :: PCS_0:1

for R1, S1 being set
for R being transitive Relation of R1
for S being transitive Relation of S1 st R1 misses S1 holds
R \/ S is transitive

proof end;

definition

let I be non empty set ;
let C be 1-sorted-yielding ManySortedSet of I;

:: original: Carrier
redefine func Carrier C -> ManySortedSet of I means :Def1: :: PCS_0:def 1
for i being Element of I holds it . i = the carrier of (C . i);

compatibility
for b₁ being ManySortedSet of I holds
( b₁ = Carrier C iff for i being Element of I holds b₁ . i = the carrier of (C . i) )

proof end;

coherence
Carrier C is ManySortedSet of I

proof end;

end;

:: deftheorem Def1 defines Carrier PCS_0:def 1 :
for I being non empty set
for C being 1-sorted-yielding ManySortedSet of I
for b₃ being ManySortedSet of I holds
( b₃ = Carrier C iff for i being Element of I holds b₃ . i = the carrier of (C . i) );

definition

let R1, R2, S1, S2 be set ;
let R be Relation of R1,R2;
let S be Relation of S1,S2;
defpred S₁[ object , object ] 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 object 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 b₁ being Relation of [:R1,S1:],[:R2,S2:] st
for x, y being object holds
( [x,y] in b₁ 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 ) ) )

proof end;

uniqueness
for b₁, b₂ being Relation of [:R1,S1:],[:R2,S2:] st ( for x, y being object holds
( [x,y] in b₁ 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 object holds
( [x,y] in b₂ 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
b₁ = b₂

proof end;

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 b₇ being Relation of [:R1,S1:],[:R2,S2:] holds
( b₇ = [^R,S^] iff for x, y being object holds
( [x,y] in b₇ 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 b₁ being Relation of [:R1,S1:],[:R2,S2:] holds
( b₁ = [^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 b₁ iff ( [r1,r2] in R or [s1,s2] in S ) ) )

proof end;

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 b₇ being Relation of [:R1,S1:],[:R2,S2:] holds
( b₇ = [^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 b₇ iff ( [r1,r2] in R or [s1,s2] in S ) ) );

registration

let R1, S1 be set ;
let R be total Relation of R1;
let S be total Relation of S1;

cluster [^R,S^] -> total ;

coherence
[^R,S^] is total

proof end;

end;

registration

let R1, S1 be set ;
let R be reflexive Relation of R1;
let S be reflexive Relation of S1;

cluster [^R,S^] -> reflexive ;

coherence
[^R,S^] is reflexive

proof end;

end;

registration

let R1, S1 be set ;
let R be Relation of R1;
let S be total reflexive Relation of S1;

cluster [^R,S^] -> reflexive ;

coherence
[^R,S^] is reflexive

proof end;

end;

registration

let R1, S1 be set ;
let R be total reflexive Relation of R1;
let S be Relation of S1;

cluster [^R,S^] -> reflexive ;

coherence
[^R,S^] is reflexive

proof end;

end;

registration

let R1, S1 be set ;
let R be symmetric Relation of R1;
let S be symmetric Relation of S1;

cluster [^R,S^] -> symmetric ;

coherence
[^R,S^] is symmetric

proof end;

end;

registration

cluster empty -> total for RelStr ;

coherence
for b₁ being RelStr st b₁ is empty holds
b₁ is total ;

end;

definition

let R be Relation;

attr R is transitive-yielding means :Def4: :: PCS_0:def 4
for S being RelStr st S in rng R holds
S is transitive ;

end;

:: deftheorem Def4 defines transitive-yielding PCS_0:def 4 :
for R being Relation holds
( R is transitive-yielding iff for S being RelStr st S in rng R holds
S is transitive );

registration

cluster Relation-like Poset-yielding -> transitive-yielding for set ;

coherence
for b₁ being Relation st b₁ is Poset-yielding holds
b₁ is transitive-yielding by YELLOW16:def 5;

end;

registration

cluster Relation-like Function-like Poset-yielding for set ;

existence
ex b₁ being Function st b₁ is Poset-yielding

proof end;

end;

registration

let I be set ;

cluster Relation-like I -defined Function-like total Poset-yielding for set ;

existence
ex b₁ being ManySortedSet of I st b₁ is Poset-yielding

proof end;

end;

definition

let I be set ;
let C be RelStr-yielding ManySortedSet of I;

func pcs-InternalRels C -> ManySortedSet of I means :Def5: :: PCS_0:def 5
for i being set st i in I holds
ex P being RelStr st
( P = C . i & it . i = the InternalRel of P );

existence
ex b₁ being ManySortedSet of I st
for i being set st i in I holds
ex P being RelStr st
( P = C . i & b₁ . i = the InternalRel of P )

proof end;

uniqueness
for b₁, b₂ being ManySortedSet of I st ( for i being set st i in I holds
ex P being RelStr st
( P = C . i & b₁ . i = the InternalRel of P ) ) & ( for i being set st i in I holds
ex P being RelStr st
( P = C . i & b₂ . i = the InternalRel of P ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines pcs-InternalRels PCS_0:def 5 :
for I being set
for C being RelStr-yielding ManySortedSet of I
for b₃ being ManySortedSet of I holds
( b₃ = pcs-InternalRels C iff for i being set st i in I holds
ex P being RelStr st
( P = C . i & b₃ . i = the InternalRel of P ) );

definition

let I be non empty set ;
let C be RelStr-yielding ManySortedSet of I;

redefine func pcs-InternalRels C means :Def6: :: PCS_0:def 6
for i being Element of I holds it . i = the InternalRel of (C . i);

compatibility
for b₁ being ManySortedSet of I holds
( b₁ = pcs-InternalRels C iff for i being Element of I holds b₁ . i = the InternalRel of (C . i) )

proof end;

end;

:: deftheorem Def6 defines pcs-InternalRels PCS_0:def 6 :
for I being non empty set
for C being RelStr-yielding ManySortedSet of I
for b₃ being ManySortedSet of I holds
( b₃ = pcs-InternalRels C iff for i being Element of I holds b₃ . i = the InternalRel of (C . i) );

registration

let I be set ;
let C be RelStr-yielding ManySortedSet of I;

cluster pcs-InternalRels C -> Relation-yielding ;

coherence
pcs-InternalRels C is Relation-yielding

proof end;

end;

registration

let I be non empty set ;
let C be RelStr-yielding transitive-yielding ManySortedSet of I;
let i be Element of I;

cluster C . i -> transitive for RelStr ;

coherence
for b₁ being RelStr st b₁ = C . i holds
b₁ is transitive

proof end;

end;

definition

attr c₁ is strict ;
struct TolStr -> 1-sorted ;
aggr TolStr(# carrier, ToleranceRel #) -> TolStr ;
sel ToleranceRel c₁ -> Relation of the carrier of c₁;

end;

definition

let P be TolStr ;
let p, q be Element of P;

pred p (--) q means :Def7: :: PCS_0:def 7
[p,q] in the ToleranceRel of P;

end;

:: deftheorem Def7 defines (--) PCS_0:def 7 :
for P being TolStr
for p, q being Element of P holds
( p (--) q iff [p,q] in the ToleranceRel of P );

definition

let P be TolStr ;

attr P is pcs-tol-total means :Def8: :: PCS_0:def 8
the ToleranceRel of P is total ;

attr P is pcs-tol-reflexive means :Def9: :: PCS_0:def 9
the ToleranceRel of P is_reflexive_in the carrier of P;

attr P is pcs-tol-irreflexive means :Def10: :: PCS_0:def 10
the ToleranceRel of P is_irreflexive_in the carrier of P;

attr P is pcs-tol-symmetric means :Def11: :: PCS_0:def 11
the ToleranceRel of P is_symmetric_in the carrier of P;

end;

:: deftheorem Def8 defines pcs-tol-total PCS_0:def 8 :
for P being TolStr holds
( P is pcs-tol-total iff the ToleranceRel of P is total );

:: deftheorem Def9 defines pcs-tol-reflexive PCS_0:def 9 :
for P being TolStr holds
( P is pcs-tol-reflexive iff the ToleranceRel of P is_reflexive_in the carrier of P );

:: deftheorem Def10 defines pcs-tol-irreflexive PCS_0:def 10 :
for P being TolStr holds
( P is pcs-tol-irreflexive iff the ToleranceRel of P is_irreflexive_in the carrier of P );

:: deftheorem Def11 defines pcs-tol-symmetric PCS_0:def 11 :
for P being TolStr holds
( P is pcs-tol-symmetric iff the ToleranceRel of P is_symmetric_in the carrier of P );

definition

func emptyTolStr -> TolStr equals :: PCS_0:def 12
TolStr(# {},({} ({},{})) #);

coherence
TolStr(# {},({} ({},{})) #) is TolStr ;

end;

:: deftheorem defines emptyTolStr PCS_0:def 12 :
emptyTolStr = TolStr(# {},({} ({},{})) #);

registration

cluster emptyTolStr -> empty strict ;

coherence
( emptyTolStr is empty & emptyTolStr is strict ) ;

end;

theorem :: PCS_0:2

for P being TolStr st P is empty holds
TolStr(# the carrier of P, the ToleranceRel of P #) = emptyTolStr

proof end;

registration

cluster pcs-tol-reflexive -> pcs-tol-total for TolStr ;

coherence
for b₁ being TolStr st b₁ is pcs-tol-reflexive holds
b₁ is pcs-tol-total

proof end;

end;

registration

cluster empty -> pcs-tol-reflexive pcs-tol-irreflexive pcs-tol-symmetric for TolStr ;

coherence
for b₁ being TolStr st b₁ is empty holds
( b₁ is pcs-tol-reflexive & b₁ is pcs-tol-irreflexive & b₁ is pcs-tol-symmetric )

proof end;

end;

registration

cluster empty strict for TolStr ;

existence
ex b₁ being TolStr st
( b₁ is empty & b₁ is strict )

proof end;

end;

registration

let P be pcs-tol-total TolStr ;

cluster the ToleranceRel of P -> total ;

coherence
the ToleranceRel of P is total by Def8;

end;

registration

let P be pcs-tol-reflexive TolStr ;

cluster the ToleranceRel of P -> reflexive ;

coherence
the ToleranceRel of P is reflexive

proof end;

end;

registration

let P be pcs-tol-irreflexive TolStr ;

cluster the ToleranceRel of P -> irreflexive ;

coherence
the ToleranceRel of P is irreflexive

proof end;

end;

registration

let P be pcs-tol-symmetric TolStr ;

cluster the ToleranceRel of P -> symmetric ;

coherence
the ToleranceRel of P is symmetric

proof end;

end;

registration

let L be pcs-tol-total TolStr ;

cluster TolStr(# the carrier of L, the ToleranceRel of L #) -> pcs-tol-total ;

coherence
TolStr(# the carrier of L, the ToleranceRel of L #) is pcs-tol-total ;

end;

definition

let P be pcs-tol-symmetric TolStr ;
let p, q be Element of P;
:: original: (--)
redefine pred p (--) q;
symmetry
for p, q being Element of P st (P,b₁,b₂) holds
(P,b₂,b₁)

proof end;

end;

registration

let D be set ;

cluster TolStr(# D,(nabla D) #) -> pcs-tol-reflexive pcs-tol-symmetric ;

coherence
( TolStr(# D,(nabla D) #) is pcs-tol-reflexive & TolStr(# D,(nabla D) #) is pcs-tol-symmetric )

proof end;

end;

registration

let D be set ;

cluster TolStr(# D,({} (D,D)) #) -> pcs-tol-irreflexive pcs-tol-symmetric ;

coherence
( TolStr(# D,({} (D,D)) #) is pcs-tol-irreflexive & TolStr(# D,({} (D,D)) #) is pcs-tol-symmetric )

proof end;

end;

registration

cluster non empty strict pcs-tol-reflexive pcs-tol-symmetric for TolStr ;

existence
ex b₁ being TolStr st
( b₁ is strict & not b₁ is empty & b₁ is pcs-tol-reflexive & b₁ is pcs-tol-symmetric )

proof end;

end;

registration

cluster non empty strict pcs-tol-irreflexive pcs-tol-symmetric for TolStr ;

existence
ex b₁ being TolStr st
( b₁ is strict & not b₁ is empty & b₁ is pcs-tol-irreflexive & b₁ is pcs-tol-symmetric )

proof end;

end;

definition

let R be Relation;

attr R is TolStr-yielding means :: PCS_0:def 13
for P being set st P in rng R holds
P is TolStr ;

end;

:: deftheorem defines TolStr-yielding PCS_0:def 13 :
for R being Relation holds
( R is TolStr-yielding iff for P being set st P in rng R holds
P is TolStr );

definition

let f be Function;

redefine attr f is TolStr-yielding means :Def14: :: PCS_0:def 14
for x being set st x in dom f holds
f . x is TolStr ;

compatibility
( f is TolStr-yielding iff for x being set st x in dom f holds
f . x is TolStr )

proof end;

end;

:: deftheorem Def14 defines TolStr-yielding PCS_0:def 14 :
for f being Function holds
( f is TolStr-yielding iff for x being set st x in dom f holds
f . x is TolStr );

definition

let I be set ;
let f be ManySortedSet of I;
A1: dom f = I by PARTFUN1:def 2;

:: original: TolStr-yielding
redefine attr f is TolStr-yielding means :: PCS_0:def 15
for x being set st x in I holds
f . x is TolStr ;

compatibility
( f is TolStr-yielding iff for x being set st x in I holds
f . x is TolStr ) by A1;

end;

:: deftheorem defines TolStr-yielding PCS_0:def 15 :
for I being set
for f being ManySortedSet of I holds
( f is TolStr-yielding iff for x being set st x in I holds
f . x is TolStr );

definition

let R be Relation;

attr R is pcs-tol-reflexive-yielding means :Def16: :: PCS_0:def 16
for S being TolStr st S in rng R holds
S is pcs-tol-reflexive ;

attr R is pcs-tol-irreflexive-yielding means :Def17: :: PCS_0:def 17
for S being TolStr st S in rng R holds
S is pcs-tol-irreflexive ;

attr R is pcs-tol-symmetric-yielding means :Def18: :: PCS_0:def 18
for S being TolStr st S in rng R holds
S is pcs-tol-symmetric ;

end;

:: deftheorem Def16 defines pcs-tol-reflexive-yielding PCS_0:def 16 :
for R being Relation holds
( R is pcs-tol-reflexive-yielding iff for S being TolStr st S in rng R holds
S is pcs-tol-reflexive );

:: deftheorem Def17 defines pcs-tol-irreflexive-yielding PCS_0:def 17 :
for R being Relation holds
( R is pcs-tol-irreflexive-yielding iff for S being TolStr st S in rng R holds
S is pcs-tol-irreflexive );

:: deftheorem Def18 defines pcs-tol-symmetric-yielding PCS_0:def 18 :
for R being Relation holds
( R is pcs-tol-symmetric-yielding iff for S being TolStr st S in rng R holds
S is pcs-tol-symmetric );

registration

cluster Relation-like empty -> pcs-tol-reflexive-yielding pcs-tol-irreflexive-yielding pcs-tol-symmetric-yielding for set ;

coherence
for b₁ being Relation st b₁ is empty holds
( b₁ is pcs-tol-reflexive-yielding & b₁ is pcs-tol-irreflexive-yielding & b₁ is pcs-tol-symmetric-yielding ) ;

end;

registration

let I be set ;
let P be TolStr ;

cluster I --> P -> () for ManySortedSet of I;

coherence
for b₁ being ManySortedSet of I st b₁ = I --> P holds
b₁ is TolStr-yielding by FUNCOP_1:7;

end;

registration

let I be set ;
let P be pcs-tol-reflexive TolStr ;

cluster I --> P -> pcs-tol-reflexive-yielding for ManySortedSet of I;

coherence
for b₁ being ManySortedSet of I st b₁ = I --> P holds
b₁ is pcs-tol-reflexive-yielding

proof end;

end;

registration

let I be set ;
let P be pcs-tol-irreflexive TolStr ;

cluster I --> P -> pcs-tol-irreflexive-yielding for ManySortedSet of I;

coherence
for b₁ being ManySortedSet of I st b₁ = I --> P holds
b₁ is pcs-tol-irreflexive-yielding

proof end;

end;

registration

let I be set ;
let P be pcs-tol-symmetric TolStr ;

cluster I --> P -> pcs-tol-symmetric-yielding for ManySortedSet of I;

coherence
for b₁ being ManySortedSet of I st b₁ = I --> P holds
b₁ is pcs-tol-symmetric-yielding

proof end;

end;

registration

cluster Relation-like Function-like TolStr-yielding -> 1-sorted-yielding for set ;

coherence
for b₁ being Function st b₁ is TolStr-yielding holds
b₁ is 1-sorted-yielding

proof end;

end;

registration

let I be set ;

cluster Relation-like I -defined Function-like total () pcs-tol-reflexive-yielding pcs-tol-symmetric-yielding for set ;

existence
ex b₁ being ManySortedSet of I st
( b₁ is pcs-tol-reflexive-yielding & b₁ is pcs-tol-symmetric-yielding & b₁ is () )

proof end;

end;

registration

let I be set ;

cluster Relation-like I -defined Function-like total () pcs-tol-irreflexive-yielding pcs-tol-symmetric-yielding for set ;

existence
ex b₁ being ManySortedSet of I st
( b₁ is pcs-tol-irreflexive-yielding & b₁ is pcs-tol-symmetric-yielding & b₁ is () )

proof end;

end;

registration

let I be set ;

cluster Relation-like I -defined Function-like total () for set ;

existence
not for b₁ being ManySortedSet of I holds b₁ is ()

proof end;

end;

definition

let I be non empty set ;
let C be () ManySortedSet of I;
let i be Element of I;
:: original: .
redefine func C . i -> TolStr ;
coherence
C . i is TolStr

proof end;

end;

definition

let I be set ;
let C be () ManySortedSet of I;

func pcs-ToleranceRels C -> ManySortedSet of I means :Def19: :: PCS_0:def 19
for i being set st i in I holds
ex P being TolStr st
( P = C . i & it . i = the ToleranceRel of P );

existence
ex b₁ being ManySortedSet of I st
for i being set st i in I holds
ex P being TolStr st
( P = C . i & b₁ . i = the ToleranceRel of P )

proof end;

uniqueness
for b₁, b₂ being ManySortedSet of I st ( for i being set st i in I holds
ex P being TolStr st
( P = C . i & b₁ . i = the ToleranceRel of P ) ) & ( for i being set st i in I holds
ex P being TolStr st
( P = C . i & b₂ . i = the ToleranceRel of P ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def19 defines pcs-ToleranceRels PCS_0:def 19 :
for I being set
for C being () ManySortedSet of I
for b₃ being ManySortedSet of I holds
( b₃ = pcs-ToleranceRels C iff for i being set st i in I holds
ex P being TolStr st
( P = C . i & b₃ . i = the ToleranceRel of P ) );

definition

let I be non empty set ;
let C be () ManySortedSet of I;

redefine func pcs-ToleranceRels C means :Def20: :: PCS_0:def 20
for i being Element of I holds it . i = the ToleranceRel of (C . i);

compatibility
for b₁ being ManySortedSet of I holds
( b₁ = pcs-ToleranceRels C iff for i being Element of I holds b₁ . i = the ToleranceRel of (C . i) )

proof end;

end;

:: deftheorem Def20 defines pcs-ToleranceRels PCS_0:def 20 :
for I being non empty set
for C being () ManySortedSet of I
for b₃ being ManySortedSet of I holds
( b₃ = pcs-ToleranceRels C iff for i being Element of I holds b₃ . i = the ToleranceRel of (C . i) );

registration

let I be set ;
let C be () ManySortedSet of I;

cluster pcs-ToleranceRels C -> Relation-yielding ;

coherence
pcs-ToleranceRels C is Relation-yielding

proof end;

end;

registration

let I be non empty set ;
let C be () pcs-tol-reflexive-yielding ManySortedSet of I;
let i be Element of I;

cluster C . i -> pcs-tol-reflexive for TolStr ;

coherence
for b₁ being TolStr st b₁ = C . i holds
b₁ is pcs-tol-reflexive

proof end;

end;

registration

let I be non empty set ;
let C be () pcs-tol-irreflexive-yielding ManySortedSet of I;
let i be Element of I;

cluster C . i -> pcs-tol-irreflexive for TolStr ;

coherence
for b₁ being TolStr st b₁ = C . i holds
b₁ is pcs-tol-irreflexive

proof end;

end;

registration

let I be non empty set ;
let C be () pcs-tol-symmetric-yielding ManySortedSet of I;
let i be Element of I;

cluster C . i -> pcs-tol-symmetric for TolStr ;

coherence
for b₁ being TolStr st b₁ = C . i holds
b₁ is pcs-tol-symmetric

proof end;

end;

theorem Th3: :: PCS_0:3

for P, Q being TolStr st TolStr(# the carrier of P, the ToleranceRel of P #) = TolStr(# the carrier of Q, the ToleranceRel of Q #) & P is pcs-tol-reflexive holds
Q is pcs-tol-reflexive ;

theorem Th4: :: PCS_0:4

for P, Q being TolStr st TolStr(# the carrier of P, the ToleranceRel of P #) = TolStr(# the carrier of Q, the ToleranceRel of Q #) & P is pcs-tol-irreflexive holds
Q is pcs-tol-irreflexive ;

theorem Th5: :: PCS_0:5

for P, Q being TolStr st TolStr(# the carrier of P, the ToleranceRel of P #) = TolStr(# the carrier of Q, the ToleranceRel of Q #) & P is pcs-tol-symmetric holds
Q is pcs-tol-symmetric ;

definition

let P, Q be TolStr ;

func [^P,Q^] -> TolStr equals :: PCS_0:def 21
TolStr(# [: the carrier of P, the carrier of Q:],[^ the ToleranceRel of P, the ToleranceRel of Q^] #);

coherence
TolStr(# [: the carrier of P, the carrier of Q:],[^ the ToleranceRel of P, the ToleranceRel of Q^] #) is TolStr ;

end;

:: deftheorem defines [^ PCS_0:def 21 :
for P, Q being TolStr holds [^P,Q^] = TolStr(# [: the carrier of P, the carrier of Q:],[^ the ToleranceRel of P, the ToleranceRel of Q^] #);

notation

let P, Q be TolStr ;
let p be Element of P;
let q be Element of Q;
synonym [^p,q^] for [P,Q];

end;

definition

let P, Q be non empty TolStr ;
let p be Element of P;
let q be Element of Q;
:: original: [^
redefine func [^p,q^] -> Element of [^P,Q^];
coherence
[^,^] is Element of [^P,Q^]

proof end;

end;

notation

let P, Q be TolStr ;
let p be Element of [^P,Q^];
synonym p ^`1 for P `1 ;
synonym p ^`2 for P `2 ;

end;

definition

let P, Q be non empty TolStr ;
let p be Element of [^P,Q^];
:: original: ^`1
redefine func p ^`1 -> Element of P;
coherence
^`1 is Element of P by MCART_1:10;
:: original: ^`2
redefine func p ^`2 -> Element of Q;
coherence
^`2 is Element of Q by MCART_1:10;

end;

theorem Th6: :: PCS_0:6

for S1, S2 being non empty TolStr
for a, c being Element of S1
for b, d being Element of S2 holds
( [^a,b^] (--) [^c,d^] iff ( a (--) c or b (--) d ) ) by Def3;

theorem :: PCS_0:7

for S1, S2 being non empty TolStr
for x, y being Element of [^S1,S2^] holds
( x (--) y iff ( x ^`1 (--) y ^`1 or x ^`2 (--) y ^`2 ) )

proof end;

registration

let P be TolStr ;
let Q be pcs-tol-reflexive TolStr ;

cluster [^P,Q^] -> pcs-tol-reflexive ;

coherence
[^P,Q^] is pcs-tol-reflexive

proof end;

end;

registration

let P be pcs-tol-reflexive TolStr ;
let Q be TolStr ;

cluster [^P,Q^] -> pcs-tol-reflexive ;

coherence
[^P,Q^] is pcs-tol-reflexive

proof end;

end;

registration

let P, Q be pcs-tol-symmetric TolStr ;

cluster [^P,Q^] -> pcs-tol-symmetric ;

coherence
[^P,Q^] is pcs-tol-symmetric

proof end;

end;

definition

attr c₁ is strict ;
struct pcs-Str -> RelStr , TolStr ;
aggr pcs-Str(# carrier, InternalRel, ToleranceRel #) -> pcs-Str ;

end;

definition

let P be pcs-Str ;

attr P is pcs-compatible means :Def22: :: PCS_0:def 22
for p, p9, q, q9 being Element of P st p (--) q & p9 <= p & q9 <= q holds
p9 (--) q9;

end;

:: deftheorem Def22 defines pcs-compatible PCS_0:def 22 :
for P being pcs-Str holds
( P is pcs-compatible iff for p, p9, q, q9 being Element of P st p (--) q & p9 <= p & q9 <= q holds
p9 (--) q9 );

definition

let P be pcs-Str ;

attr P is pcs-like means :: PCS_0:def 23
( P is reflexive & P is transitive & P is pcs-tol-reflexive & P is pcs-tol-symmetric & P is pcs-compatible );

attr P is anti-pcs-like means :: PCS_0:def 24
( P is reflexive & P is transitive & P is pcs-tol-irreflexive & P is pcs-tol-symmetric & P is pcs-compatible );

end;

:: deftheorem defines pcs-like PCS_0:def 23 :
for P being pcs-Str holds
( P is pcs-like iff ( P is reflexive & P is transitive & P is pcs-tol-reflexive & P is pcs-tol-symmetric & P is pcs-compatible ) );

:: deftheorem defines anti-pcs-like PCS_0:def 24 :
for P being pcs-Str holds
( P is anti-pcs-like iff ( P is reflexive & P is transitive & P is pcs-tol-irreflexive & P is pcs-tol-symmetric & P is pcs-compatible ) );

registration

cluster pcs-like -> reflexive transitive pcs-tol-reflexive pcs-tol-symmetric pcs-compatible for pcs-Str ;

coherence
for b₁ being pcs-Str st b₁ is pcs-like holds
( b₁ is reflexive & b₁ is transitive & b₁ is pcs-tol-reflexive & b₁ is pcs-tol-symmetric & b₁ is pcs-compatible ) ;

cluster reflexive transitive pcs-tol-reflexive pcs-tol-symmetric pcs-compatible -> pcs-like for pcs-Str ;

coherence
for b₁ being pcs-Str st b₁ is reflexive & b₁ is transitive & b₁ is pcs-tol-reflexive & b₁ is pcs-tol-symmetric & b₁ is pcs-compatible holds
b₁ is pcs-like ;

cluster anti-pcs-like -> reflexive transitive pcs-tol-irreflexive pcs-tol-symmetric pcs-compatible for pcs-Str ;

coherence
for b₁ being pcs-Str st b₁ is anti-pcs-like holds
( b₁ is reflexive & b₁ is transitive & b₁ is pcs-tol-irreflexive & b₁ is pcs-tol-symmetric & b₁ is pcs-compatible ) ;

cluster reflexive transitive pcs-tol-irreflexive pcs-tol-symmetric pcs-compatible -> anti-pcs-like for pcs-Str ;

coherence
for b₁ being pcs-Str st b₁ is reflexive & b₁ is transitive & b₁ is pcs-tol-irreflexive & b₁ is pcs-tol-symmetric & b₁ is pcs-compatible holds
b₁ is anti-pcs-like ;

end;

definition

let D be set ;

func pcs-total D -> pcs-Str equals :: PCS_0:def 25
pcs-Str(# D,(nabla D),(nabla D) #);

coherence
pcs-Str(# D,(nabla D),(nabla D) #) is pcs-Str ;

end;

:: deftheorem defines pcs-total PCS_0:def 25 :
for D being set holds pcs-total D = pcs-Str(# D,(nabla D),(nabla D) #);

registration

let D be set ;

cluster pcs-total D -> strict ;

coherence
pcs-total D is strict ;

end;

registration

let D be non empty set ;

cluster pcs-total D -> non empty ;

coherence
not pcs-total D is empty ;

end;

registration

let D be set ;

cluster pcs-total D -> reflexive transitive pcs-tol-reflexive pcs-tol-symmetric ;

coherence
( pcs-total D is reflexive & pcs-total D is transitive & pcs-total D is pcs-tol-reflexive & pcs-total D is pcs-tol-symmetric )

proof end;

end;

registration

let D be set ;

cluster pcs-total D -> pcs-like ;

coherence
pcs-total D is pcs-like

proof end;

end;

registration

let D be set ;

cluster pcs-Str(# D,(nabla D),({} (D,D)) #) -> anti-pcs-like ;

coherence
pcs-Str(# D,(nabla D),({} (D,D)) #) is anti-pcs-like

proof end;

end;

registration

cluster non empty strict pcs-like for pcs-Str ;

existence
ex b₁ being pcs-Str st
( b₁ is strict & not b₁ is empty & b₁ is pcs-like )

proof end;

cluster non empty strict anti-pcs-like for pcs-Str ;

existence
ex b₁ being pcs-Str st
( b₁ is strict & not b₁ is empty & b₁ is anti-pcs-like )

proof end;

end;

definition

mode pcs is pcs-like pcs-Str ;
mode anti-pcs is anti-pcs-like pcs-Str ;

end;

definition

func pcs-empty -> pcs-Str equals :: PCS_0:def 26
pcs-total 0;

coherence
pcs-total 0 is pcs-Str ;

end;

:: deftheorem defines pcs-empty PCS_0:def 26 :
pcs-empty = pcs-total 0;

registration

cluster pcs-empty -> empty strict pcs-like ;

coherence
( pcs-empty is strict & pcs-empty is empty & pcs-empty is pcs-like ) ;

end;

definition

let p be set ;

func pcs-singleton p -> pcs-Str equals :: PCS_0:def 27
pcs-total {p};

coherence
pcs-total {p} is pcs-Str ;

end;

:: deftheorem defines pcs-singleton PCS_0:def 27 :
for p being set holds pcs-singleton p = pcs-total {p};

registration

let p be set ;

cluster pcs-singleton p -> non empty strict pcs-like ;

coherence
( pcs-singleton p is strict & not pcs-singleton p is empty & pcs-singleton p is pcs-like ) ;

end;

definition

let R be Relation;

attr R is pcs-Str-yielding means :: PCS_0:def 28
for P being set st P in rng R holds
P is pcs-Str ;

attr R is pcs-yielding means :: PCS_0:def 29
for P being set st P in rng R holds
P is pcs;

end;

:: deftheorem defines pcs-Str-yielding PCS_0:def 28 :
for R being Relation holds
( R is pcs-Str-yielding iff for P being set st P in rng R holds
P is pcs-Str );

:: deftheorem defines pcs-yielding PCS_0:def 29 :
for R being Relation holds
( R is pcs-yielding iff for P being set st P in rng R holds
P is pcs );

definition

let f be Function;

redefine attr f is pcs-Str-yielding means :: PCS_0:def 30
for x being set st x in dom f holds
f . x is pcs-Str ;

compatibility
( f is pcs-Str-yielding iff for x being set st x in dom f holds
f . x is pcs-Str )

proof end;

redefine attr f is pcs-yielding means :: PCS_0:def 31
for x being set st x in dom f holds
f . x is pcs;

compatibility
( f is pcs-yielding iff for x being set st x in dom f holds
f . x is pcs )

proof end;

end;

:: deftheorem defines pcs-Str-yielding PCS_0:def 30 :
for f being Function holds
( f is pcs-Str-yielding iff for x being set st x in dom f holds
f . x is pcs-Str );

:: deftheorem defines pcs-yielding PCS_0:def 31 :
for f being Function holds
( f is pcs-yielding iff for x being set st x in dom f holds
f . x is pcs );

definition

let I be set ;
let f be ManySortedSet of I;
A1: dom f = I by PARTFUN1:def 2;

:: original: pcs-Str-yielding
redefine attr f is pcs-Str-yielding means :Def32: :: PCS_0:def 32
for x being set st x in I holds
f . x is pcs-Str ;

compatibility
( f is pcs-Str-yielding iff for x being set st x in I holds
f . x is pcs-Str ) by A1;

:: original: pcs-yielding
redefine attr f is pcs-yielding means :Def33: :: PCS_0:def 33
for x being set st x in I holds
f . x is pcs;

compatibility
( f is pcs-yielding iff for x being set st x in I holds
f . x is pcs ) by A1;

end;

:: deftheorem Def32 defines pcs-Str-yielding PCS_0:def 32 :
for I being set
for f being ManySortedSet of I holds
( f is pcs-Str-yielding iff for x being set st x in I holds
f . x is pcs-Str );

:: deftheorem Def33 defines pcs-yielding PCS_0:def 33 :
for I being set
for f being ManySortedSet of I holds
( f is pcs-yielding iff for x being set st x in I holds
f . x is pcs );

registration

cluster Relation-like pcs-Str-yielding -> RelStr-yielding TolStr-yielding for set ;

coherence
for b₁ being Relation st b₁ is pcs-Str-yielding holds
( b₁ is TolStr-yielding & b₁ is RelStr-yielding )

proof end;

cluster Relation-like pcs-yielding -> pcs-Str-yielding for set ;

coherence
for b₁ being Relation st b₁ is pcs-yielding holds
b₁ is pcs-Str-yielding ;

cluster Relation-like pcs-yielding -> reflexive-yielding transitive-yielding pcs-tol-reflexive-yielding pcs-tol-symmetric-yielding for set ;

coherence
for b₁ being Relation st b₁ is pcs-yielding holds
( b₁ is reflexive-yielding & b₁ is transitive-yielding & b₁ is pcs-tol-reflexive-yielding & b₁ is pcs-tol-symmetric-yielding ) ;

end;

registration

let I be set ;
let P be pcs;

cluster I --> P -> () for ManySortedSet of I;

coherence
for b₁ being ManySortedSet of I st b₁ = I --> P holds
b₁ is pcs-yielding by FUNCOP_1:7;

end;

registration

let I be set ;

cluster Relation-like I -defined Function-like total () for set ;

existence
not for b₁ being ManySortedSet of I holds b₁ is ()

proof end;

end;

definition

let I be non empty set ;
let C be () ManySortedSet of I;
let i be Element of I;
:: original: .
redefine func C . i -> pcs-Str ;
coherence
C . i is pcs-Str by Def32;

end;

definition

let I be non empty set ;
let C be () ManySortedSet of I;
let i be Element of I;
:: original: .
redefine func C . i -> pcs;
coherence
C . i is pcs by Def33;

end;

:: Union of PCS's

definition

let P, Q be pcs-Str ;

pred P c= Q means :: PCS_0:def 34
( the carrier of P c= the carrier of Q & the InternalRel of P c= the InternalRel of Q & the ToleranceRel of P c= the ToleranceRel of Q );

reflexivity
for P being pcs-Str holds
( the carrier of P c= the carrier of P & the InternalRel of P c= the InternalRel of P & the ToleranceRel of P c= the ToleranceRel of P ) ;

end;

:: deftheorem defines c= PCS_0:def 34 :
for P, Q being pcs-Str holds
( P c= Q iff ( the carrier of P c= the carrier of Q & the InternalRel of P c= the InternalRel of Q & the ToleranceRel of P c= the ToleranceRel of Q ) );

theorem :: PCS_0:8

for P, Q being RelStr
for p, q being Element of P
for p1, q1 being Element of Q st the InternalRel of P c= the InternalRel of Q & p = p1 & q = q1 & p <= q holds
p1 <= q1 ;

theorem :: PCS_0:9

for P, Q being TolStr
for p, q being Element of P
for p1, q1 being Element of Q st the ToleranceRel of P c= the ToleranceRel of Q & p = p1 & q = q1 & p (--) q holds
p1 (--) q1 ;

Lm2: 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
;

definition

let C be Relation;

attr C is pcs-chain-like means :Def35: :: PCS_0:def 35
for P, Q being pcs-Str st P in rng C & Q in rng C & not P c= Q holds
Q c= P;

end;

:: deftheorem Def35 defines pcs-chain-like PCS_0:def 35 :
for C being Relation holds
( C is pcs-chain-like iff for P, Q being pcs-Str st P in rng C & Q in rng C & not P c= Q holds
Q c= P );

registration

let I be set ;
let P be pcs-Str ;

cluster I --> P -> pcs-chain-like for ManySortedSet of I;

coherence
for b₁ being ManySortedSet of I st b₁ = I --> P holds
b₁ is pcs-chain-like

proof end;

end;

registration

cluster Relation-like Function-like pcs-yielding pcs-chain-like for set ;

existence
ex b₁ being Function st
( b₁ is pcs-chain-like & b₁ is pcs-yielding )

proof end;

end;

registration

let I be set ;

cluster Relation-like I -defined Function-like total () pcs-chain-like for set ;

existence
ex b₁ being ManySortedSet of I st
( b₁ is pcs-chain-like & b₁ is () )

proof end;

end;

definition

let I be set ;
mode pcs-Chain of I is () pcs-chain-like ManySortedSet of I;

end;

definition

let I be set ;
let C be () ManySortedSet of I;

func pcs-union C -> strict pcs-Str means :Def36: :: PCS_0:def 36
( the carrier of it = Union (Carrier C) & the InternalRel of it = Union (pcs-InternalRels C) & the ToleranceRel of it = Union (pcs-ToleranceRels C) );

existence
ex b₁ being strict pcs-Str st
( the carrier of b₁ = Union (Carrier C) & the InternalRel of b₁ = Union (pcs-InternalRels C) & the ToleranceRel of b₁ = Union (pcs-ToleranceRels C) )

proof end;

uniqueness
for b₁, b₂ being strict pcs-Str st the carrier of b₁ = Union (Carrier C) & the InternalRel of b₁ = Union (pcs-InternalRels C) & the ToleranceRel of b₁ = Union (pcs-ToleranceRels C) & the carrier of b₂ = Union (Carrier C) & the InternalRel of b₂ = Union (pcs-InternalRels C) & the ToleranceRel of b₂ = Union (pcs-ToleranceRels C) holds
b₁ = b₂ ;

end;

:: deftheorem Def36 defines pcs-union PCS_0:def 36 :
for I being set
for C being () ManySortedSet of I
for b₃ being strict pcs-Str holds
( b₃ = pcs-union C iff ( the carrier of b₃ = Union (Carrier C) & the InternalRel of b₃ = Union (pcs-InternalRels C) & the ToleranceRel of b₃ = Union (pcs-ToleranceRels C) ) );

theorem Th10: :: PCS_0:10

for I being set
for C being () ManySortedSet of I
for p, q being Element of (pcs-union C) holds
( p <= q iff ex i being object ex P being pcs-Str ex p9, q9 being Element of P st
( i in I & P = C . i & p9 = p & q9 = q & p9 <= q9 ) )

proof end;

theorem :: PCS_0:11

for I being non empty set
for C being () ManySortedSet of I
for p, q being Element of (pcs-union C) holds
( p <= q iff ex i being Element of I ex p9, q9 being Element of (C . i) st
( p9 = p & q9 = q & p9 <= q9 ) )

proof end;

theorem Th12: :: PCS_0:12

for I being set
for C being () ManySortedSet of I
for p, q being Element of (pcs-union C) holds
( p (--) q iff ex i being object ex P being pcs-Str ex p9, q9 being Element of P st
( i in I & P = C . i & p9 = p & q9 = q & p9 (--) q9 ) )

proof end;

theorem :: PCS_0:13

for I being non empty set
for C being () ManySortedSet of I
for p, q being Element of (pcs-union C) holds
( p (--) q iff ex i being Element of I ex p9, q9 being Element of (C . i) st
( p9 = p & q9 = q & p9 (--) q9 ) )

proof end;

registration

let I be set ;
let C be reflexive-yielding () ManySortedSet of I;

cluster pcs-union C -> reflexive strict ;

coherence
pcs-union C is reflexive

proof end;

end;

registration

let I be set ;
let C be pcs-tol-reflexive-yielding () ManySortedSet of I;

cluster pcs-union C -> pcs-tol-reflexive strict ;

coherence
pcs-union C is pcs-tol-reflexive

proof end;

end;

registration

let I be set ;
let C be pcs-tol-symmetric-yielding () ManySortedSet of I;

cluster pcs-union C -> pcs-tol-symmetric strict ;

coherence
pcs-union C is pcs-tol-symmetric

proof end;

end;

registration

let I be set ;
let C be pcs-Chain of I;

cluster pcs-union C -> transitive strict pcs-compatible ;

coherence
( pcs-union C is transitive & pcs-union C is pcs-compatible )

proof end;

end;

:: Direct Sum of PCS's

definition

let p, q be set ;

func <%p,q%> -> ManySortedSet of {0,1} equals :: PCS_0:def 37
<%p,q%>;

coherence
<%p,q%> is ManySortedSet of {0,1} by CARD_1:50;

end;

:: deftheorem defines <% PCS_0:def 37 :
for p, q being set holds <%p,q%> = <%p,q%>;

registration

let P, Q be 1-sorted ;

cluster <%P,Q%> -> 1-sorted-yielding ;

coherence
<%P,Q%> is 1-sorted-yielding

proof end;

end;

Lm3: now :: thesis: for a, b being object holds rng <%a,b%> = {a,b}

let a, b be object ; :: thesis: rng <%a,b%> = {a,b}
<%a,b%> = (0,1) --> (a,b) by AFINSQ_1:76;
hence rng <%a,b%> = {a,b} by FUNCT_4:64; :: thesis: verum

end;

registration

let P, Q be RelStr ;

cluster <%P,Q%> -> RelStr-yielding ;

coherence
<%P,Q%> is RelStr-yielding

proof end;

end;

registration

let P, Q be TolStr ;

cluster <%P,Q%> -> () ;

coherence
<%P,Q%> is TolStr-yielding

proof end;

end;

registration

let P, Q be pcs-Str ;

cluster <%P,Q%> -> () ;

coherence
<%P,Q%> is pcs-Str-yielding

proof end;

end;

registration

let P, Q be reflexive pcs-Str ;

cluster <%P,Q%> -> reflexive-yielding ;

coherence
<%P,Q%> is reflexive-yielding

proof end;

end;

registration

let P, Q be transitive pcs-Str ;

cluster <%P,Q%> -> transitive-yielding ;

coherence
<%P,Q%> is transitive-yielding

proof end;

end;

registration

let P, Q be pcs-tol-reflexive pcs-Str ;

cluster <%P,Q%> -> pcs-tol-reflexive-yielding ;

coherence
<%P,Q%> is pcs-tol-reflexive-yielding

proof end;

end;

registration

let P, Q be pcs-tol-symmetric pcs-Str ;

cluster <%P,Q%> -> pcs-tol-symmetric-yielding ;

coherence
<%P,Q%> is pcs-tol-symmetric-yielding

proof end;

end;

registration

let P, Q be pcs;

cluster <%P,Q%> -> () ;

coherence
<%P,Q%> is pcs-yielding

proof end;

end;

definition

let P, Q be pcs-Str ;

func pcs-sum (P,Q) -> pcs-Str equals :: PCS_0:def 39
pcs-union <%P,Q%>;

coherence
pcs-union <%P,Q%> is pcs-Str ;

end;

:: deftheorem PCS_0:def 38 :
canceled;

:: deftheorem defines pcs-sum PCS_0:def 39 :
for P, Q being pcs-Str holds pcs-sum (P,Q) = pcs-union <%P,Q%>;

deffunc H₁( 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

for P, Q being pcs-Str holds
( the carrier of (pcs-sum (P,Q)) = the carrier of P \/ the carrier of Q & the InternalRel of (pcs-sum (P,Q)) = the InternalRel of P \/ the InternalRel of Q & the ToleranceRel of (pcs-sum (P,Q)) = the ToleranceRel of P \/ the ToleranceRel of Q )

proof end;

theorem Th15: :: PCS_0:15

for P, Q being pcs-Str holds pcs-sum (P,Q) = 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) #)

proof end;

theorem :: PCS_0:16

for P, Q being pcs-Str
for p, q being Element of (pcs-sum (P,Q)) holds
( p <= q iff ( ex p9, q9 being Element of P st
( p9 = p & q9 = q & p9 <= q9 ) or ex p9, q9 being Element of Q st
( p9 = p & q9 = q & p9 <= q9 ) ) )

proof end;

theorem :: PCS_0:17

for P, Q being pcs-Str
for p, q being Element of (pcs-sum (P,Q)) holds
( p (--) q iff ( ex p9, q9 being Element of P st
( p9 = p & q9 = q & p9 (--) q9 ) or ex p9, q9 being Element of Q st
( p9 = p & q9 = q & p9 (--) q9 ) ) )

proof end;

registration

let P, Q be reflexive pcs-Str ;

cluster pcs-sum (P,Q) -> reflexive ;

coherence
pcs-sum (P,Q) is reflexive ;

end;

registration

let P, Q be pcs-tol-reflexive pcs-Str ;

cluster pcs-sum (P,Q) -> pcs-tol-reflexive ;

coherence
pcs-sum (P,Q) is pcs-tol-reflexive ;

end;

registration

let P, Q be pcs-tol-symmetric pcs-Str ;

cluster pcs-sum (P,Q) -> pcs-tol-symmetric ;

coherence
pcs-sum (P,Q) is pcs-tol-symmetric ;

end;

theorem Th18: :: PCS_0:18

for P, Q being pcs st P misses Q holds
the InternalRel of (pcs-sum (P,Q)) is transitive

proof end;

theorem Th19: :: PCS_0:19

for P, Q being pcs st P misses Q holds
pcs-sum (P,Q) is pcs-compatible

proof end;

theorem :: PCS_0:20

for P, Q being pcs st P misses Q holds
pcs-sum (P,Q) is pcs

proof end;

:: Extension

definition

let P be pcs-Str ;
let a be set ;

func pcs-extension (P,a) -> strict pcs-Str means :Def39: :: PCS_0:def 40
( 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 b₁ being strict pcs-Str st
( the carrier of b₁ = {a} \/ the carrier of P & the InternalRel of b₁ = [:{a}, the carrier of b₁:] \/ the InternalRel of P & the ToleranceRel of b₁ = ([:{a}, the carrier of b₁:] \/ [: the carrier of b₁,{a}:]) \/ the ToleranceRel of P )

proof end;

uniqueness
for b₁, b₂ being strict pcs-Str st the carrier of b₁ = {a} \/ the carrier of P & the InternalRel of b₁ = [:{a}, the carrier of b₁:] \/ the InternalRel of P & the ToleranceRel of b₁ = ([:{a}, the carrier of b₁:] \/ [: the carrier of b₁,{a}:]) \/ the ToleranceRel of P & the carrier of b₂ = {a} \/ the carrier of P & the InternalRel of b₂ = [:{a}, the carrier of b₂:] \/ the InternalRel of P & the ToleranceRel of b₂ = ([:{a}, the carrier of b₂:] \/ [: the carrier of b₂,{a}:]) \/ the ToleranceRel of P holds
b₁ = b₂ ;

end;

:: deftheorem Def39 defines pcs-extension PCS_0:def 40 :
for P being pcs-Str
for a being set
for b₃ being strict pcs-Str holds
( b₃ = pcs-extension (P,a) iff ( the carrier of b₃ = {a} \/ the carrier of P & the InternalRel of b₃ = [:{a}, the carrier of b₃:] \/ the InternalRel of P & the ToleranceRel of b₃ = ([:{a}, the carrier of b₃:] \/ [: the carrier of b₃,{a}:]) \/ the ToleranceRel of P ) );

registration

let P be pcs-Str ;
let a be set ;

cluster pcs-extension (P,a) -> non empty strict ;

coherence
not pcs-extension (P,a) is empty

proof end;

end;

theorem Th21: :: PCS_0:21

for P being pcs-Str
for a being set holds
( the carrier of P c= the carrier of (pcs-extension (P,a)) & the InternalRel of P c= the InternalRel of (pcs-extension (P,a)) & the ToleranceRel of P c= the ToleranceRel of (pcs-extension (P,a)) )

proof end;

theorem :: PCS_0:22

for P being pcs-Str
for a being set
for p, q being Element of (pcs-extension (P,a)) st p = a holds
p <= q

proof end;

theorem Th23: :: PCS_0:23

for P being pcs-Str
for a being set
for p, q being Element of P
for p1, q1 being Element of (pcs-extension (P,a)) st p = p1 & q = q1 & p <= q holds
p1 <= q1

proof end;

theorem Th24: :: PCS_0:24

for P being pcs-Str
for a being set
for p being Element of P
for p1, q1 being Element of (pcs-extension (P,a)) st p = p1 & p <> a & p1 <= q1 & not a in the carrier of P holds
( q1 in the carrier of P & q1 <> a )

proof end;

theorem Th25: :: PCS_0:25

for P being pcs-Str
for a being set
for p being Element of (pcs-extension (P,a)) st p <> a holds
p in the carrier of P

proof end;

theorem Th26: :: PCS_0:26

for P being pcs-Str
for a being set
for p, q being Element of P
for p1, q1 being Element of (pcs-extension (P,a)) st p = p1 & q = q1 & p <> a & p1 <= q1 holds
p <= q

proof end;

theorem Th27: :: PCS_0:27

for P being pcs-Str
for a being set
for p, q being Element of (pcs-extension (P,a)) st p = a holds
( p (--) q & q (--) p )

proof end;

theorem Th28: :: PCS_0:28

for P being pcs-Str
for a being set
for p, q being Element of P
for p1, q1 being Element of (pcs-extension (P,a)) st p = p1 & q = q1 & p (--) q holds
p1 (--) q1

proof end;

theorem Th29: :: PCS_0:29

for P being pcs-Str
for a being set
for p, q being Element of P
for p1, q1 being Element of (pcs-extension (P,a)) st p = p1 & q = q1 & p <> a & q <> a & p1 (--) q1 holds
p (--) q

proof end;

registration

let P be reflexive pcs-Str ;
let a be set ;

cluster pcs-extension (P,a) -> reflexive strict ;

coherence
pcs-extension (P,a) is reflexive

proof end;

end;

theorem Th30: :: PCS_0:30

for P being transitive pcs-Str
for a being set st not a in the carrier of P holds
pcs-extension (P,a) is transitive

proof end;

registration

let P be pcs-tol-reflexive pcs-Str ;
let a be set ;

cluster pcs-extension (P,a) -> pcs-tol-reflexive strict ;

coherence
pcs-extension (P,a) is pcs-tol-reflexive

proof end;

end;

registration

let P be pcs-tol-symmetric pcs-Str ;
let a be set ;

cluster pcs-extension (P,a) -> pcs-tol-symmetric strict ;

coherence
pcs-extension (P,a) is pcs-tol-symmetric

proof end;

end;

theorem Th31: :: PCS_0:31

for P being pcs-compatible pcs-Str
for a being set st not a in the carrier of P holds
pcs-extension (P,a) is pcs-compatible

proof end;

theorem :: PCS_0:32

for P being pcs
for a being set st not a in the carrier of P holds
pcs-extension (P,a) is pcs

proof end;

:: Reverse

definition

let P be pcs-Str ;

func pcs-reverse P -> strict pcs-Str means :Def40: :: PCS_0:def 41
( the carrier of it = the carrier of P & the InternalRel of it = the InternalRel of P ~ & the ToleranceRel of it = the ToleranceRel of P ` );

existence
ex b₁ being strict pcs-Str st
( the carrier of b₁ = the carrier of P & the InternalRel of b₁ = the InternalRel of P ~ & the ToleranceRel of b₁ = the ToleranceRel of P ` )

proof end;

uniqueness
for b₁, b₂ being strict pcs-Str st the carrier of b₁ = the carrier of P & the InternalRel of b₁ = the InternalRel of P ~ & the ToleranceRel of b₁ = the ToleranceRel of P ` & the carrier of b<sub>2</sub> = the carrier of P & the InternalRel of b<sub>2</sub> = the InternalRel of P ~ & the ToleranceRel of b<sub>2</sub> = the ToleranceRel of P ` holds
b₁ = b₂ ;

end;

:: deftheorem Def40 defines pcs-reverse PCS_0:def 41 :
for P being pcs-Str
for b₂ being strict pcs-Str holds
( b₂ = pcs-reverse P iff ( the carrier of b₂ = the carrier of P & the InternalRel of b₂ = the InternalRel of P ~ & the ToleranceRel of b₂ = the ToleranceRel of P ` ) );

registration

let P be non empty pcs-Str ;

cluster pcs-reverse P -> non empty strict ;

coherence
not pcs-reverse P is empty

proof end;

end;

theorem Th33: :: PCS_0:33

for P being pcs-Str
for p, q being Element of P
for p9, q9 being Element of (pcs-reverse P) st p = p9 & q = q9 holds
( p <= q iff q9 <= p9 )

proof end;

theorem Th34: :: PCS_0:34

for P being pcs-Str
for p, q being Element of P
for p9, q9 being Element of (pcs-reverse P) st p = p9 & q = q9 & p (--) q holds
not p9 (--) q9

proof end;

theorem Th35: :: PCS_0:35

for P being non empty pcs-Str
for p, q being Element of P
for p9, q9 being Element of (pcs-reverse P) st p = p9 & q = q9 & not p9 (--) q9 holds
p (--) q

proof end;

registration

let P be reflexive pcs-Str ;

cluster pcs-reverse P -> reflexive strict ;

coherence
pcs-reverse P is reflexive

proof end;

end;

registration

let P be transitive pcs-Str ;

cluster pcs-reverse P -> transitive strict ;

coherence
pcs-reverse P is transitive

proof end;

end;

registration

let P be pcs-tol-reflexive pcs-Str ;

cluster pcs-reverse P -> pcs-tol-irreflexive strict ;

coherence
pcs-reverse P is pcs-tol-irreflexive

proof end;

end;

registration

let P be pcs-tol-irreflexive pcs-Str ;

cluster pcs-reverse P -> pcs-tol-reflexive strict ;

coherence
pcs-reverse P is pcs-tol-reflexive

proof end;

end;

registration

let P be pcs-tol-symmetric pcs-Str ;

cluster pcs-reverse P -> pcs-tol-symmetric strict ;

coherence
pcs-reverse P is pcs-tol-symmetric

proof end;

end;

registration

let P be pcs-compatible pcs-Str ;

cluster pcs-reverse P -> strict pcs-compatible ;

coherence
pcs-reverse P is pcs-compatible

proof end;

end;

:: Times

definition

let P, Q be pcs-Str ;

func P pcs-times Q -> pcs-Str equals :: PCS_0:def 42
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 42 :
for P, Q being pcs-Str holds P pcs-times Q = 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^] #);

registration

let P, Q be pcs-Str ;

cluster P pcs-times Q -> strict ;

coherence
P pcs-times Q is strict ;

end;

registration

let P, Q be non empty pcs-Str ;

cluster P pcs-times Q -> non empty ;

coherence
not P pcs-times Q is empty ;

end;

theorem :: PCS_0:36

for P, Q being pcs-Str
for p, q being Element of (P pcs-times Q)
for p1, p2 being Element of P
for q1, q2 being Element of Q st p = [p1,q1] & q = [p2,q2] holds
( p <= q iff ( p1 <= p2 & q1 <= q2 ) )

proof end;

theorem :: PCS_0:37

for P, Q being pcs-Str
for p, q being Element of (P pcs-times Q)
for p1, p2 being Element of P
for q1, q2 being Element of Q st p = [p1,q1] & q = [p2,q2] & p (--) q & not p1 (--) p2 holds
q1 (--) q2

proof end;

theorem Th38: :: PCS_0:38

for P, Q being non empty pcs-Str
for p, q being Element of (P pcs-times Q)
for p1, p2 being Element of P
for q1, q2 being Element of Q st p = [p1,q1] & q = [p2,q2] & ( p1 (--) p2 or q1 (--) q2 ) holds
p (--) q by Def2;

registration

let P, Q be reflexive pcs-Str ;

cluster P pcs-times Q -> reflexive ;

coherence
P pcs-times Q is reflexive

proof end;

end;

registration

let P, Q be transitive pcs-Str ;

cluster P pcs-times Q -> transitive ;

coherence
P pcs-times Q is transitive

proof end;

end;

registration

let P be pcs-Str ;
let Q be pcs-tol-reflexive pcs-Str ;

cluster P pcs-times Q -> pcs-tol-reflexive ;

coherence
P pcs-times Q is pcs-tol-reflexive

proof end;

end;

registration

let P be pcs-tol-reflexive pcs-Str ;
let Q be pcs-Str ;

cluster P pcs-times Q -> pcs-tol-reflexive ;

coherence
P pcs-times Q is pcs-tol-reflexive

proof end;

end;

registration

let P, Q be pcs-tol-symmetric pcs-Str ;

cluster P pcs-times Q -> pcs-tol-symmetric ;

coherence
P pcs-times Q is pcs-tol-symmetric

proof end;

end;

registration

let P, Q be pcs-compatible pcs-Str ;

cluster P pcs-times Q -> pcs-compatible ;

coherence
P pcs-times Q is pcs-compatible

proof end;

end;

definition

let P, Q be pcs-Str ;

func P --> Q -> pcs-Str equals :: PCS_0:def 43
(pcs-reverse P) pcs-times Q;

coherence
(pcs-reverse P) pcs-times Q is pcs-Str ;

end;

:: deftheorem defines --> PCS_0:def 43 :
for P, Q being pcs-Str holds P --> Q = (pcs-reverse P) pcs-times Q;

registration

let P, Q be pcs-Str ;

cluster P --> Q -> strict ;

coherence
P --> Q is strict ;

end;

registration

let P, Q be non empty pcs-Str ;

cluster P --> Q -> non empty ;

coherence
not P --> Q is empty ;

end;

theorem :: PCS_0:39

for P, Q being pcs-Str
for p, q being Element of (P --> Q)
for p1, p2 being Element of P
for q1, q2 being Element of Q st p = [p1,q1] & q = [p2,q2] holds
( p <= q iff ( p2 <= p1 & q1 <= q2 ) )

proof end;

theorem :: PCS_0:40

for P, Q being pcs-Str
for p, q being Element of (P --> Q)
for p1, p2 being Element of P
for q1, q2 being Element of Q st p = [p1,q1] & q = [p2,q2] & p (--) q & p1 (--) p2 holds
q1 (--) q2

proof end;

theorem :: PCS_0:41

for P, Q being non empty pcs-Str
for p, q being Element of (P --> Q)
for p1, p2 being Element of P
for q1, q2 being Element of Q st p = [p1,q1] & q = [p2,q2] & ( not p1 (--) p2 or q1 (--) q2 ) holds
p (--) q

proof end;

registration

let P, Q be reflexive pcs-Str ;

cluster P --> Q -> reflexive ;

coherence
P --> Q is reflexive ;

end;

registration

let P, Q be transitive pcs-Str ;

cluster P --> Q -> transitive ;

coherence
P --> Q is transitive ;

end;

registration

let P be pcs-Str ;
let Q be pcs-tol-reflexive pcs-Str ;

cluster P --> Q -> pcs-tol-reflexive ;

coherence
P --> Q is pcs-tol-reflexive ;

end;

registration

let P be pcs-tol-irreflexive pcs-Str ;
let Q be pcs-Str ;

cluster P --> Q -> pcs-tol-reflexive ;

coherence
P --> Q is pcs-tol-reflexive ;

end;

registration

let P, Q be pcs-tol-symmetric pcs-Str ;

cluster P --> Q -> pcs-tol-symmetric ;

coherence
P --> Q is pcs-tol-symmetric ;

end;

registration

let P, Q be pcs-compatible pcs-Str ;

cluster P --> Q -> pcs-compatible ;

coherence
P --> Q is pcs-compatible ;

end;

registration

let P, Q be pcs;

cluster P --> Q -> pcs-like ;

coherence
P --> Q is pcs-like ;

end;

:: Self-coherence

definition

let P be TolStr ;
let S be Subset of P;

attr S is pcs-self-coherent means :: PCS_0:def 44
for x, y being Element of P st x in S & y in S holds
x (--) y;

end;

:: deftheorem defines pcs-self-coherent PCS_0:def 44 :
for P being TolStr
for S being Subset of P holds
( S is pcs-self-coherent iff for x, y being Element of P st x in S & y in S holds
x (--) y );

registration

let P be TolStr ;

cluster empty -> pcs-self-coherent for Element of bool the carrier of P;

coherence
for b₁ being Subset of P st b₁ is empty holds
b₁ is pcs-self-coherent ;

end;

definition

let P be TolStr ;
let F be Subset-Family of P;

attr F is pcs-self-coherent-membered means :Def44: :: PCS_0:def 45
for S being Subset of P st S in F holds
S is pcs-self-coherent ;

end;

:: deftheorem Def44 defines pcs-self-coherent-membered PCS_0:def 45 :
for P being TolStr
for F being Subset-Family of P holds
( F is pcs-self-coherent-membered iff for S being Subset of P st S in F holds
S is pcs-self-coherent );

registration

let P be TolStr ;

cluster non empty pcs-self-coherent-membered for Element of bool (bool the carrier of P);

existence
ex b₁ being Subset-Family of P st
( not b₁ is empty & b₁ is pcs-self-coherent-membered )

proof end;

end;

definition

let P be RelStr ;
let D be set ;
defpred S₁[ 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 46
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 b₁ being Relation of D st
for A, B being set holds
( [A,B] in b₁ 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 ) ) ) )

proof end;

uniqueness
for b₁, b₂ being Relation of D st ( for A, B being set holds
( [A,B] in b₁ 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 b₂ 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
b₁ = b₂

proof end;

end;

:: deftheorem Def45 defines pcs-general-power-IR PCS_0:def 46 :
for P being RelStr
for D being set
for b₃ being Relation of D holds
( b₃ = pcs-general-power-IR (P,D) iff for A, B being set holds
( [A,B] in b₃ 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 ) ) ) ) );

definition

let P be TolStr ;
let D be set ;
defpred S₁[ 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 47
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 b₁ being Relation of D st
for A, B being set holds
( [A,B] in b₁ 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 ) ) )

proof end;

uniqueness
for b₁, b₂ being Relation of D st ( for A, B being set holds
( [A,B] in b₁ 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 b₂ 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
b₁ = b₂

proof end;

end;

:: deftheorem Def46 defines pcs-general-power-TR PCS_0:def 47 :
for P being TolStr
for D being set
for b₃ being Relation of D holds
( b₃ = pcs-general-power-TR (P,D) iff for A, B being set holds
( [A,B] in b₃ 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 ) ) ) );

theorem :: PCS_0:42

for P being RelStr
for D being Subset-Family of P
for A, B being set holds
( [A,B] in pcs-general-power-IR (P,D) iff ( A in D & B in D & ( for a being Element of P st a in A holds
ex b being Element of P st
( b in B & a <= b ) ) ) )

proof end;

theorem :: PCS_0:43

for P being TolStr
for D being Subset-Family of P
for A, B being set holds
( [A,B] in pcs-general-power-TR (P,D) iff ( A in D & B in D & ( for a, b being Element of P st a in A & b in B holds
a (--) b ) ) )

proof end;

definition

let P be pcs-Str ;
let D be set ;

func pcs-general-power (P,D) -> pcs-Str equals :: PCS_0:def 48
pcs-Str(# D,(pcs-general-power-IR (P,D)),(pcs-general-power-TR (P,D)) #);

coherence
pcs-Str(# D,(pcs-general-power-IR (P,D)),(pcs-general-power-TR (P,D)) #) is pcs-Str ;

end;

:: deftheorem defines pcs-general-power PCS_0:def 48 :
for P being pcs-Str
for D being set holds pcs-general-power (P,D) = pcs-Str(# D,(pcs-general-power-IR (P,D)),(pcs-general-power-TR (P,D)) #);

notation

let P be pcs-Str ;
let D be Subset-Family of P;
synonym pcs-general-power D for pcs-general-power (P,D);

end;

registration

let P be pcs-Str ;
let D be non empty set ;

cluster pcs-general-power (P,D) -> non empty ;

coherence
not pcs-general-power (P,D) is empty ;

end;

theorem Th44: :: PCS_0:44

for P being pcs-Str
for D being set
for p, q being Element of (pcs-general-power (P,D)) st p <= q holds
for p9 being Element of P st p9 in p holds
ex q9 being Element of P st
( q9 in q & p9 <= q9 )

proof end;

theorem :: PCS_0:45

for P being pcs-Str
for D being non empty Subset-Family of P
for p, q being Element of (pcs-general-power D) st ( for p9 being Element of P st p9 in p holds
ex q9 being Element of P st
( q9 in q & p9 <= q9 ) ) holds
p <= q

proof end;

theorem Th46: :: PCS_0:46

for P being pcs-Str
for D being set
for p, q being Element of (pcs-general-power (P,D)) st p (--) q holds
for p9, q9 being Element of P st p9 in p & q9 in q holds
p9 (--) q9 by Def46;

theorem :: PCS_0:47

for P being pcs-Str
for D being non empty Subset-Family of P
for p, q being Element of (pcs-general-power D) st ( for p9, q9 being Element of P st p9 in p & q9 in q holds
p9 (--) q9 ) holds
p (--) q

proof end;

registration

let P be pcs-Str ;
let D be set ;

cluster pcs-general-power (P,D) -> strict ;

coherence
pcs-general-power (P,D) is strict ;

end;

registration

let P be reflexive pcs-Str ;
let D be Subset-Family of P;

cluster pcs-general-power (P,D) -> reflexive ;

coherence
pcs-general-power D is reflexive

proof end;

end;

registration

let P be transitive pcs-Str ;
let D be set ;

cluster pcs-general-power (P,D) -> transitive ;

coherence
pcs-general-power (P,D) is transitive

proof end;

end;

registration

let P be pcs-tol-reflexive pcs-Str ;
let D be pcs-self-coherent-membered Subset-Family of P;

cluster pcs-general-power (P,D) -> pcs-tol-reflexive ;

coherence
pcs-general-power D is pcs-tol-reflexive

proof end;

end;

registration

let P be pcs-tol-symmetric pcs-Str ;
let D be Subset-Family of P;

cluster pcs-general-power (P,D) -> pcs-tol-symmetric ;

coherence
pcs-general-power D is pcs-tol-symmetric

proof end;

end;

registration

let P be pcs-compatible pcs-Str ;
let D be Subset-Family of P;

cluster pcs-general-power (P,D) -> pcs-compatible ;

coherence
pcs-general-power D is pcs-compatible

proof end;

end;

definition

let P be pcs-Str ;

func pcs-coherent-power P -> set equals :: PCS_0:def 49
{ X where X is Subset of P : X is pcs-self-coherent } ;

coherence
{ X where X is Subset of P : X is pcs-self-coherent } is set ;

end;

:: deftheorem defines pcs-coherent-power PCS_0:def 49 :
for P being pcs-Str holds pcs-coherent-power P = { X where X is Subset of P : X is pcs-self-coherent } ;

registration

let P be pcs-Str ;

cluster pcs-self-coherent for Element of bool the carrier of P;

existence
ex b₁ being Subset of P st b₁ is pcs-self-coherent

proof end;

end;

theorem Th48: :: PCS_0:48

for P being pcs-Str
for X being set st X in pcs-coherent-power P holds
X is pcs-self-coherent Subset of P

proof end;

registration

let P be pcs-Str ;

cluster pcs-coherent-power P -> non empty ;

coherence
not pcs-coherent-power P is empty

proof end;

end;

definition

let P be pcs-Str ;
:: original: pcs-coherent-power
redefine func pcs-coherent-power P -> Subset-Family of P;
coherence
pcs-coherent-power P is Subset-Family of P

proof end;

end;

registration

let P be pcs-Str ;

cluster pcs-coherent-power P -> pcs-self-coherent-membered for Subset-Family of P;

coherence
for b₁ being Subset-Family of P st b₁ = pcs-coherent-power P holds
b₁ is pcs-self-coherent-membered by Th48;

end;

definition

let P be pcs-Str ;

func pcs-power P -> pcs-Str equals :: PCS_0:def 50
pcs-general-power (pcs-coherent-power P);

coherence
pcs-general-power (pcs-coherent-power P) is pcs-Str ;

end;

:: deftheorem defines pcs-power PCS_0:def 50 :
for P being pcs-Str holds pcs-power P = pcs-general-power (pcs-coherent-power P);

registration

let P be pcs-Str ;

cluster pcs-power P -> strict ;

coherence
pcs-power P is strict ;

end;

registration

let P be pcs-Str ;

cluster pcs-power P -> non empty ;

coherence
not pcs-power P is empty ;

end;

registration

let P be reflexive pcs-Str ;

cluster pcs-power P -> reflexive ;

coherence
pcs-power P is reflexive ;

end;

registration

let P be transitive pcs-Str ;

cluster pcs-power P -> transitive ;

coherence
pcs-power P is transitive ;

end;

registration

let P be pcs-tol-reflexive pcs-Str ;

cluster pcs-power P -> pcs-tol-reflexive ;

coherence
pcs-power P is pcs-tol-reflexive ;

end;

registration

let P be pcs-tol-symmetric pcs-Str ;

cluster pcs-power P -> pcs-tol-symmetric ;

coherence
pcs-power P is pcs-tol-symmetric ;

end;

registration

let P be pcs-compatible pcs-Str ;

cluster pcs-power P -> pcs-compatible ;

coherence
pcs-power P is pcs-compatible ;

end;

registration

let P be pcs;

cluster pcs-power P -> pcs-like ;

coherence
pcs-power P is pcs-like ;

end;