:: Basic Operations on Preordered Coherent Spaces
:: by Klaus E. Grue and Artur Korni{\l}owicz
::
:: Received August 28, 2007
:: Copyright (c) 2007-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies CARD_1, SUBSET_1, RELAT_1, XBOOLE_0, PARTFUN1, RELAT_2, PRALG_1,
PBOOLE, RLVECT_2, FUNCT_1, STRUCT_0, ZFMISC_1, TARSKI, ORDERS_2,
YELLOW16, YELLOW_1, MSUALG_4, EQREL_1, FUNCOP_1, MCART_1, XXREAL_0,
WAYBEL_3, CARD_3, YELLOW_3, SETFAM_1, PCS_0, AFINSQ_1;
notations TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, ZFMISC_1, MCART_1, DOMAIN_1,
RELAT_1, FUNCT_1, PARTFUN1, RELSET_1, RELAT_2, EQREL_1, CARD_3, PARTIT_2,
FUNCT_4, ORDINAL1, NUMBERS, PBOOLE, FUNCOP_1, AFINSQ_1, STRUCT_0, TSEP_1,
ORDERS_2, PRALG_1, YELLOW_1, WAYBEL_3, YELLOW16, YELLOW_3;
constructors PRALG_1, PARTIT_2, TSEP_1, YELLOW16, YELLOW_3, DOMAIN_1,
RELSET_1, FUNCT_4, AFINSQ_1, XTUPLE_0, NUMBERS;
registrations EQREL_1, PARTFUN1, SUBSET_1, XBOOLE_0, WAYBEL_3, RELAT_1,
ORDERS_2, PRALG_1, STRUCT_0, YELLOW16, YELLOW_3, RELSET_1, FUNCOP_1,
AFINSQ_1, RELAT_2, XTUPLE_0, ORDINAL1;
requirements BOOLE, SUBSET, NUMERALS;
definitions XBOOLE_0, RELAT_1, PARTFUN1, RELAT_2, ORDERS_2, STRUCT_0, TSEP_1,
PRALG_1, YELLOW_1, WAYBEL_3, TARSKI, FUNCOP_1;
equalities SUBSET_1, RELAT_1, EQREL_1, CARD_3, PARTIT_2, ORDINAL1;
expansions RELAT_1, PARTFUN1, RELAT_2, ORDERS_2, WAYBEL_3;
theorems ZFMISC_1, ORDERS_2, RELSET_1, PARTFUN1, RELAT_1, RELAT_2, XBOOLE_0,
TARSKI, FUNCT_1, PBOOLE, FUNCOP_1, PRALG_1, XBOOLE_1, ORDERS_1, FUNCT_4,
YELLOW16, YELLOW_0, WAYBEL_8, YELLOW_3, MCART_1, SETFAM_1, AFINSQ_1,
CARD_1, XTUPLE_0, FUNCT_2;
schemes RELSET_1, CLASSES1, RELAT_1;
begin :: Preliminaries
reconsider z = 0, j = 1 as Element of {0,1} by TARSKI:def 2;
definition
let R1, R2 be set, R be Relation of R1,R2;
redefine func field R -> Subset of R1 \/ R2; :: redefines field (RELAT_1, definition)
coherence 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;
redefine func R \/ S -> Relation of R1 \/ S1, R2 \/ S2; :: redefines \/ (XBOOLE_0, definition)
coherence by ZFMISC_1:119;
end;
registration
let R1, S1 be set;
let R being total Relation of R1;
let S being total Relation of S1;
cluster R \/ S -> total for Relation of R1 \/ S1;
coherence
proof
dom (R \/ S) = (dom R) \/ dom S by XTUPLE_0:23
.= R1 \/ dom S by PARTFUN1:def 2
.= R1 \/ S1 by PARTFUN1:def 2;
hence thesis;
end;
end;
registration
let R1, S1 be set;
let R being reflexive Relation of R1;
let S being reflexive Relation of S1;
cluster R \/ S -> reflexive for Relation of R1 \/ S1;
coherence;
end;
registration
let R1, S1 be set;
let R being symmetric Relation of R1;
let S being symmetric Relation of S1;
cluster R \/ S -> symmetric for Relation of R1 \/ S1;
coherence;
end;
Lm1: now
let R1, S1 be set;
let R be Relation of R1;
let S be Relation of S1 such that
A1: R1 misses S1;
let q1, q2 be object such that
A2: [q1,q2] in R \/ S and
A3: q2 in S1;
A4: [q1,q2] in R or [q1,q2] in S by A2,XBOOLE_0:def 3;
now
assume [q1,q2] in R;
then q2 in R1 by ZFMISC_1:87;
hence contradiction by A1,A3,XBOOLE_0:3;
end;
hence [q1,q2] in S & q1 in S1 by A4,ZFMISC_1:87;
end;
theorem Th1:
for R1, S1 being set, R being transitive (Relation of R1),
S being transitive Relation of S1 st R1 misses S1 holds R \/ S is transitive
proof
let R1, S1 be set, R be transitive (Relation of R1),
S be transitive Relation of S1 such that
A1: R1 misses S1;
let p1, p2, p3 be object;
set RS = R \/ S;
set D = field RS;
assume that
p1 in D and p2 in D and
A2: p3 in D and
A3: [p1,p2] in RS and
A4: [p2,p3] in RS;
per cases by A2,XBOOLE_0:def 3;
suppose
A5: p3 in R1;
then p2 in R1 by A1,A4,Lm1;
then
A6: [p1,p2] in R by A1,A3,Lm1;
[p2,p3] in R by A1,A4,A5,Lm1;
then [p1,p3] in R by A6,RELAT_2:31;
hence thesis by XBOOLE_0:def 3;
end;
suppose
A7: p3 in S1;
then p2 in S1 by A1,A4,Lm1;
then
A8: [p1,p2] in S by A1,A3,Lm1;
[p2,p3] in S by A1,A4,A7,Lm1;
then [p1,p3] in S by A8,RELAT_2:31;
hence thesis by XBOOLE_0:def 3;
end;
end;
definition
let I be non empty set, C be 1-sorted-yielding ManySortedSet of I;
redefine func Carrier C -> ManySortedSet of I means :: redefines Carrier (PRALG_1, definition)
:Def1:
for i being Element of I holds it.i = the carrier of C.i;
compatibility
proof
let X be ManySortedSet of I;
thus X = Carrier C implies
for i being Element of I holds X.i = the carrier of C.i
proof
assume
A1: X = Carrier C;
let i be Element of I;
ex P being 1-sorted st P = C.i & X.i = the carrier of P
by A1,PRALG_1:def 15;
hence thesis;
end;
assume
A2: for i being Element of I holds X.i = the carrier of C.i;
for j being object st j in I holds X.j = (Carrier C).j
proof
let j be object;
assume
b2: j in I; then
reconsider jj = j as Element of I;
B2: X.j = the carrier of (C.jj) by A2;
I = dom C by PARTFUN1:def 2; then
ex R1 being 1-sorted st
R1 = C.j & (Carrier C).j = the carrier of R1 by b2,PRALG_1:def 14;
hence thesis by B2;
end;
hence thesis by PBOOLE:3;
end;
coherence
proof
dom Carrier C = I by PARTFUN1:def 2;
hence thesis;
end;
end;
definition
let R1, R2, S1, S2 be set;
let R be Relation of R1,R2, S be Relation of S1,S2;
defpred P[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:
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
proof
consider Q being Relation of [:R1,S1:],[:R2,S2:] such that
A1: for x, y being object holds [x,y] in Q iff x in [:R1,S1:] &
y in [:R2,S2:] & P[x,y] from RELSET_1:sch 1;
take Q;
let x, y be object;
thus [x,y] in Q implies P[x,y] by A1;
given r1, s1, r2, s2 being set such that
A2: x = [r1,s1] and
A3: y = [r2,s2] and
A4: r1 in R1 and
A5: s1 in S1 and
A6: r2 in R2 and
A7: s2 in S2 and
A8: [r1,r2] in R or [s1,s2] in S;
A9: x in [:R1,S1:] by A2,A4,A5,ZFMISC_1:87;
y in [:R2,S2:] by A3,A6,A7,ZFMISC_1:87;
hence thesis by A1,A2,A3,A4,A5,A6,A7,A8,A9;
end;
uniqueness
proof
let A, B be Relation of [:R1,S1:],[:R2,S2:] such that
A10: for x, y being object holds [x,y] in A iff P[x,y]and
A11: for x, y being object holds [x,y] in B iff P[x,y];
thus A = B from RELAT_1:sch 2(A10,A11);
end;
end;
definition
let R1, R2, S1, S2 be non empty set;
let R be Relation of R1,R2, S be Relation of S1,S2;
redefine func [^R,S^] means :: redefines [^ (PCS_0, definition)
:Def3:
for r1 being Element of R1, r2 being Element of R2
for s1 being Element of S1, s2 being Element of S2 holds
[[r1,s1],[r2,s2]] in it iff [r1,r2] in R or [s1,s2] in S;
compatibility
proof
let f be Relation of [:R1,S1:],[:R2,S2:];
thus f = [^R,S^] implies for r1 being Element of R1, r2 being Element of R2
for s1 being Element of S1, s2 being Element of S2 holds
[[r1,s1],[r2,s2]] in f iff [r1,r2] in R or [s1,s2] in S
proof
assume
A1: f = [^R,S^];
let r1 be Element of R1, r2 be Element of R2;
let s1 be Element of S1, s2 be Element of S2;
hereby
assume [[r1,s1],[r2,s2]] in f;
then consider r19, s19, r29, s29 being set such that
A2: [r1,s1] = [r19,s19] and
A3: [r2,s2] = [r29,s29] and
r19 in R1 and s19 in S1
and r29 in R2
and s29 in S2 and
A4: [r19,r29] in R or [s19,s29] in S by A1,Def2;
A5: r1 = r19 by A2,XTUPLE_0:1;
s1 = s19 by A2,XTUPLE_0:1;
hence [r1,r2] in R or [s1,s2] in S by A3,A4,A5,XTUPLE_0:1;
end;
thus thesis by A1,Def2;
end;
assume
A6: for r1 being Element of R1, r2 being Element of R2
for s1 being Element of S1, s2 being Element of S2 holds
[[r1,s1],[r2,s2]] in f iff [r1,r2] in R or [s1,s2] in S;
for x, y being object holds [x,y] in f iff [x,y] in [^R,S^]
proof
let x, y be object;
thus [x,y] in f implies [x,y] in [^R,S^]
proof
assume
A7: [x,y] in f;
then x in dom f by XTUPLE_0:def 12;
then consider x1, x2 being object such that
A8: x1 in R1 and
A9: x2 in S1 and
A10: x = [x1,x2] by ZFMISC_1:def 2;
y in rng f by A7,XTUPLE_0:def 13;
then consider y1, y2 being object such that
A11: y1 in R2 and
A12: y2 in S2 and
A13: y = [y1,y2] by ZFMISC_1:def 2;
[x1,y1] in R or [x2,y2] in S by A6,A7,A8,A9,A10,A11,A12,A13;
hence thesis by A8,A9,A10,A11,A12,A13,Def2;
end;
assume [x,y] in [^R,S^];
then 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) by Def2;
hence thesis by A6;
end;
hence thesis;
end;
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;
coherence
proof
let x,y be object;
thus [x,y] in dom [^R,S^] implies [x,y] in [:R1,S1:];
assume
A1: [x,y] in [:R1,S1:];
then
A2: x in R1 by ZFMISC_1:87;
A3: y in S1 by A1,ZFMISC_1:87;
dom R = R1 by PARTFUN1:def 2;
then consider a being object such that
A4: [x,a] in R by A2,XTUPLE_0:def 12;
dom S = S1 by PARTFUN1:def 2;
then consider b being object such that
A5: [y,b] in S by A3,XTUPLE_0:def 12;
A6: a in R1 by A4,ZFMISC_1:87;
b in S1 by A5,ZFMISC_1:87;
then [[x,y],[a,b]] in [^R,S^] by A2,A3,A4,A6,Def2;
hence thesis by XTUPLE_0:def 12;
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
proof
let x be object;
assume
A1: x in field [^R,S^];
A2: R is_reflexive_in field R by RELAT_2:def 9;
A3: S is_reflexive_in field S by RELAT_2:def 9;
per cases by A1,XBOOLE_0:def 3;
suppose x in dom [^R,S^];
then consider y being object such that
A4: [x,y] in [^R,S^] by XTUPLE_0:def 12;
consider p, q, s, t being set such that
A5: x = [p,q] and y = [s,t] and
A6: p in R1 and
A7: q in S1 and s in R1
and t in S1 and
A8: [p,s] in R or [q,t] in S by A4,Def2;
per cases by A8;
suppose [p,s] in R;
then p in field R by RELAT_1:15;
then [p,p] in R by A2;
hence thesis by A5,A6,A7,Def2;
end;
suppose [q,t] in S;
then q in field S by RELAT_1:15;
then [q,q] in S by A3;
hence thesis by A5,A6,A7,Def2;
end;
end;
suppose x in rng [^R,S^];
then consider y being object such that
A9: [y,x] in [^R,S^] by XTUPLE_0:def 13;
consider p, q, s, t being set such that
y = [p,q] and
A10: x = [s,t] and
p in R1 and q in S1 and
A11: s in R1 and
A12: t in S1 and
A13: [p,s] in R or [q,t] in S by A9,Def2;
per cases by A13;
suppose [p,s] in R;
then s in field R by RELAT_1:15;
then [s,s] in R by A2;
hence thesis by A10,A11,A12,Def2;
end;
suppose [q,t] in S;
then t in field S by RELAT_1:15;
then [t,t] in S by A3;
hence thesis by A10,A11,A12,Def2;
end;
end;
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
proof
let x be object;
assume x in field [^R,S^];
then consider x1, x2 being object such that
A1: x1 in R1 and
A2: x2 in S1 and
A3: x = [x1,x2] by ZFMISC_1:def 2;
S1 = field S by ORDERS_1:12;
then S is_reflexive_in S1 by RELAT_2:def 9;
then [x2,x2] in S by A2;
hence thesis by A1,A2,A3,Def3;
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
proof
let x be object;
assume x in field [^R,S^];
then consider x1, x2 being object such that
A1: x1 in R1 and
A2: x2 in S1 and
A3: x = [x1,x2] by ZFMISC_1:def 2;
R1 = field R by ORDERS_1:12;
then R is_reflexive_in R1 by RELAT_2:def 9;
then [x1,x1] in R by A1;
hence thesis by A1,A2,A3,Def3;
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
proof
let x, y be object;
assume that x in field [^R,S^] and y in field [^R,S^];
assume [x,y] in [^R,S^];
then consider p, q, s, t being set such that
A1: x = [p,q] and
A2: y = [s,t] and
A3: p in R1 and
A4: q in S1 and
A5: s in R1 and
A6: t in S1 and
A7: [p,s] in R or [q,t] in S by Def2;
A8: R is_symmetric_in field R by RELAT_2:def 11;
A9: S is_symmetric_in field S by RELAT_2:def 11;
per cases by A7;
suppose
A10: [p,s] in R;
then
A11: p in field R by RELAT_1:15;
s in field R by A10,RELAT_1:15;
then [s,p] in R by A8,A10,A11;
hence thesis by A1,A2,A3,A4,A5,A6,Def2;
end;
suppose
A12: [q,t] in S;
then
A13: q in field S by RELAT_1:15;
t in field S by A12,RELAT_1:15;
then [t,q] in S by A9,A12,A13;
hence thesis by A1,A2,A3,A4,A5,A6,Def2;
end;
end;
end;
begin :: Relational Structures
registration
cluster empty -> total for RelStr;
coherence;
end;
definition
let R be Relation;
attr R is transitive-yielding means
:Def4:
for S being RelStr st S in rng R holds S is transitive;
end;
registration
cluster Poset-yielding -> transitive-yielding for Relation;
coherence
by YELLOW16:def 5;
end;
registration
cluster Poset-yielding for Function;
existence
proof
set f = the Poset-yielding ManySortedSet of 0;
take f;
thus thesis;
end;
end;
registration
let I be set;
cluster Poset-yielding for ManySortedSet of I;
existence
proof
set f = the Poset-yielding ManySortedSet of I;
take f;
thus thesis;
end;
end;
definition
let I be set, C be RelStr-yielding ManySortedSet of I;
func pcs-InternalRels C -> ManySortedSet of I means
:Def5:
for i being set st i in I
ex P being RelStr st P = C.i & it.i = the InternalRel of P;
existence
proof
defpred P[object,object] means
ex R being RelStr st R = C.$1 & $2 = the InternalRel of R;
A1: for i being object st i in I ex j being object st P[i,j]
proof
let i be object;
assume
A2: i in I;
then reconsider I as non empty set;
reconsider B = C as RelStr-yielding ManySortedSet of I;
reconsider i9 = i as Element of I by A2;
take the InternalRel of B.i9, B.i9;
thus thesis;
end;
consider M being Function such that
A3: dom M = I and
A4: for i being object st i in I holds P[i,M.i] from CLASSES1:sch 1(A1);
reconsider M as ManySortedSet of I by A3,PARTFUN1:def 2,RELAT_1:def 18;
take M;
thus thesis by A4;
end;
uniqueness
proof
let X, Y be ManySortedSet of I such that
A5: for j being set st j in I
ex R being RelStr st R = C.j & X.j = the InternalRel of R and
A6: for j being set st j in I
ex R being RelStr st R = C.j & Y.j = the InternalRel of R;
for i being object st i in I holds X.i = Y.i
proof
let i be object;
assume
A7: i in I;
then
A8: ex R being RelStr st R = C.i & X.i = the InternalRel of R by A5;
ex R being RelStr st R = C.i & Y.i = the InternalRel of R by A6,A7;
hence thesis by A8;
end;
hence thesis by PBOOLE:3;
end;
end;
definition
let I be non empty set, C be RelStr-yielding ManySortedSet of I;
redefine func pcs-InternalRels C means :: redefines pcs-InternalRels (PCS_0, definition)
:Def6:
for i being Element of I holds it.i = the InternalRel of C.i;
compatibility
proof
let X be ManySortedSet of I;
thus X = pcs-InternalRels C implies
for i being Element of I holds X.i = the InternalRel of C.i
proof
assume
A1: X = pcs-InternalRels C;
let i be Element of I;
ex P being RelStr st P = C.i & X.i = the InternalRel of P by A1,Def5;
hence thesis;
end;
assume
A2: for i being Element of I holds X.i = the InternalRel of C.i;
for i being set st i in I
ex P being RelStr st P = C.i & X.i = the InternalRel of P
proof
let i be set;
assume i in I;
then reconsider i as Element of I;
take C.i;
thus thesis by A2;
end;
hence thesis by Def5;
end;
end;
registration
let I be set, C be RelStr-yielding ManySortedSet of I;
cluster pcs-InternalRels C -> Relation-yielding;
coherence
proof
set IR = pcs-InternalRels C;
let i be object;
assume i in dom IR;
then ex P being RelStr st P = C.i & IR.i = the InternalRel of P by Def5;
hence thesis;
end;
end;
registration
let I be non empty set;
let C be transitive-yielding RelStr-yielding ManySortedSet of I;
let i be Element of I;
cluster C.i -> transitive for RelStr;
coherence
proof
dom C = I by PARTFUN1:def 2;
then C.i in rng C by FUNCT_1:3;
hence thesis by Def4;
end;
end;
begin :: Tolerance Structures
definition
struct (1-sorted) TolStr (# carrier -> set,
ToleranceRel -> Relation of the carrier #);
end;
definition
let P be TolStr;
let p, q be Element of P;
pred p (--) q means
:Def7:
[p,q] in the ToleranceRel of P;
end;
definition
let P be TolStr;
attr P is pcs-tol-total means
:Def8:
the ToleranceRel of P is total;
attr P is pcs-tol-reflexive means
:Def9:
the ToleranceRel of P is_reflexive_in the carrier of P;
attr P is pcs-tol-irreflexive means
:Def10:
the ToleranceRel of P is_irreflexive_in the carrier of P;
attr P is pcs-tol-symmetric means
:Def11:
the ToleranceRel of P is_symmetric_in the carrier of P;
end;
definition
func emptyTolStr -> TolStr equals
TolStr (# {}, {}({},{}) #);
coherence;
end;
registration
cluster emptyTolStr -> empty strict;
coherence;
end;
theorem
for P being TolStr st P is empty holds the TolStr of P = emptyTolStr
proof
let P be TolStr;
assume P is empty;
then the carrier of P = {};
hence thesis;
end;
registration
cluster pcs-tol-reflexive -> pcs-tol-total for TolStr;
coherence
proof
let P be TolStr;
assume P is pcs-tol-reflexive;
then the ToleranceRel of P is_reflexive_in the carrier of P;
hence the ToleranceRel of P is total by ORDERS_1:13;
end;
end;
registration
cluster empty -> pcs-tol-reflexive pcs-tol-irreflexive pcs-tol-symmetric
for TolStr;
coherence
proof
let P be TolStr;
assume
A1: P is empty;
thus the ToleranceRel of P is_reflexive_in the carrier of P
by A1;
thus the ToleranceRel of P is_irreflexive_in the carrier of P
by A1;
thus the ToleranceRel of P is_symmetric_in the carrier of P
by A1;
end;
end;
registration
cluster empty strict for TolStr;
existence
proof
take emptyTolStr;
thus thesis;
end;
end;
registration
let P be pcs-tol-total TolStr;
cluster the ToleranceRel of P -> total;
coherence by Def8;
end;
registration
let P be pcs-tol-reflexive TolStr;
cluster the ToleranceRel of P -> reflexive;
coherence
proof
set TR = the ToleranceRel of P;
A1: field TR = the carrier of P by ORDERS_1:12;
TR is_reflexive_in the carrier of P by Def9;
hence thesis by A1;
end;
end;
registration
let P be pcs-tol-irreflexive TolStr;
cluster the ToleranceRel of P -> irreflexive;
coherence
proof
set TR = the ToleranceRel of P;
A1: TR is_irreflexive_in the carrier of P by Def10;
let x be object;
assume x in field TR;
assume
A2: [x,x] in TR;
then x in dom TR by XTUPLE_0:def 12;
hence thesis by A1,A2;
end;
end;
registration
let P be pcs-tol-symmetric TolStr;
cluster the ToleranceRel of P -> symmetric;
coherence
proof
set TR = the ToleranceRel of P;
A1: TR is_symmetric_in the carrier of P by Def11;
let x, y be object;
assume that x in field TR and y in field TR;
assume
A2: [x,y] in TR;
then
A3: x in dom TR by XTUPLE_0:def 12;
y in rng TR by A2,XTUPLE_0:def 13;
hence thesis by A1,A2,A3;
end;
end;
registration
let L be pcs-tol-total TolStr;
cluster the TolStr of L -> pcs-tol-total;
coherence;
end;
definition
let P be pcs-tol-symmetric TolStr;
let p, q be Element of P;
redefine pred p (--) q; :: redefines (--) (PCS_0, definition)
symmetry
proof
let x, y be Element of P;
assume
A1: [x,y] in the ToleranceRel of P;
then
A2: x in the carrier of P by ZFMISC_1:87;
the ToleranceRel of P is_symmetric_in the carrier of P by Def11;
hence [y,x] in the ToleranceRel of P by A1,A2;
end;
end;
registration
let D be set;
cluster TolStr(#D,nabla D#) -> pcs-tol-reflexive pcs-tol-symmetric;
coherence
proof
set P = TolStr(#D,nabla D#);
set TR = the ToleranceRel of P;
A1: field TR = the carrier of P by ORDERS_1:12;
hence TR is_reflexive_in the carrier of P by RELAT_2:def 9;
thus TR is_symmetric_in the carrier of P by A1,RELAT_2:def 11;
end;
end;
registration
let D be set;
cluster TolStr(#D,{}(D,D)#) -> pcs-tol-irreflexive pcs-tol-symmetric;
coherence
proof
set P = TolStr(#D,{}(D,D)#);
thus the ToleranceRel of P is_irreflexive_in the carrier of P;
let x be object;
thus thesis;
end;
end;
registration
cluster strict non empty pcs-tol-reflexive pcs-tol-symmetric for TolStr;
existence
proof
take P = TolStr(#{{}},nabla {{}}#);
thus P is strict;
thus the carrier of P is non empty;
thus thesis;
end;
end;
registration
cluster strict non empty pcs-tol-irreflexive pcs-tol-symmetric for TolStr;
existence
proof
take P = TolStr(#{{}},{}({{}},{{}})#);
thus P is strict;
thus the carrier of P is non empty;
thus thesis;
end;
end;
definition
let R be Relation;
attr R is TolStr-yielding means
for P being set st P in rng R holds P is TolStr;
end;
definition
let f be Function;
redefine attr f is TolStr-yielding means :: redefines TolStr-yielding (PCS_0, definition)
:Def14:
for x being set st x in dom f holds f.x is TolStr;
compatibility
proof
thus f is TolStr-yielding implies
for x being set st x in dom f holds f.x is TolStr by FUNCT_1:3;
assume
A1: for x being set st x in dom f holds f.x is TolStr;
let P be set;
assume P in rng f;
then ex x being object st x in dom f & f.x = P by FUNCT_1:def 3;
hence thesis by A1;
end;
end;
definition
let I be set, f be ManySortedSet of I;
A1: dom f = I by PARTFUN1:def 2;
redefine attr f is TolStr-yielding means :: redefines TolStr-yielding (PCS_0, redefinition) → TolStr-yielding (PCS_0, definition)
for x being set st x in I holds f.x is TolStr;
compatibility by A1;
end;
definition
let R be Relation;
attr R is pcs-tol-reflexive-yielding means
:Def16:
for S being TolStr st S in rng R holds S is pcs-tol-reflexive;
attr R is pcs-tol-irreflexive-yielding means
:Def17:
for S being TolStr st S in rng R holds S is pcs-tol-irreflexive;
attr R is pcs-tol-symmetric-yielding means
:Def18:
for S being TolStr st S in rng R holds S is pcs-tol-symmetric;
end;
registration
cluster empty -> pcs-tol-reflexive-yielding pcs-tol-irreflexive-yielding
pcs-tol-symmetric-yielding for Relation;
coherence;
end;
registration
let I be set, P be TolStr;
cluster I --> P -> TolStr-yielding for ManySortedSet of I;
coherence
by FUNCOP_1:7;
end;
registration
let I be set, P be pcs-tol-reflexive TolStr;
cluster I --> P -> pcs-tol-reflexive-yielding for ManySortedSet of I;
coherence
proof
set f = I --> P;
f is pcs-tol-reflexive-yielding
proof
let S be TolStr;
assume S in rng f;
hence thesis by TARSKI:def 1;
end;
hence thesis;
end;
end;
registration
let I be set, P be pcs-tol-irreflexive TolStr;
cluster I --> P -> pcs-tol-irreflexive-yielding for ManySortedSet of I;
coherence
proof
set f = I --> P;
f is pcs-tol-irreflexive-yielding
proof
let S be TolStr;
assume S in rng f;
hence thesis by TARSKI:def 1;
end;
hence thesis;
end;
end;
registration
let I be set, P be pcs-tol-symmetric TolStr;
cluster I --> P -> pcs-tol-symmetric-yielding for ManySortedSet of I;
coherence
proof
set f = I --> P;
f is pcs-tol-symmetric-yielding
proof
let S be TolStr;
assume S in rng f;
hence thesis by TARSKI:def 1;
end;
hence thesis;
end;
end;
registration
cluster TolStr-yielding -> 1-sorted-yielding for Function;
coherence
proof
let f be Function;
assume
A1: f is TolStr-yielding;
let x be object;
thus thesis by A1;
end;
end;
registration
let I be set;
cluster pcs-tol-reflexive-yielding pcs-tol-symmetric-yielding TolStr-yielding
for ManySortedSet of I;
existence
proof
take I --> TolStr(#0,nabla 0#);
thus thesis;
end;
end;
registration
let I be set;
cluster pcs-tol-irreflexive-yielding pcs-tol-symmetric-yielding
TolStr-yielding for ManySortedSet of I;
existence
proof
take I --> TolStr(#0,{}(0,0)#);
thus thesis;
end;
end;
registration
let I be set;
cluster TolStr-yielding for ManySortedSet of I;
existence
proof
set R = the TolStr;
take I --> R;
thus thesis;
end;
end;
definition
let I be non empty set, C be TolStr-yielding ManySortedSet of I,
i be Element of I;
redefine func C.i -> TolStr; :: redefines . (FUNCT_1, definition)
coherence
proof
dom C = I by PARTFUN1:def 2;
hence thesis by Def14;
end;
end;
definition
let I be set, C be TolStr-yielding ManySortedSet of I;
func pcs-ToleranceRels C -> ManySortedSet of I means
:Def19:
for i being set st i in I
ex P being TolStr st P = C.i & it.i = the ToleranceRel of P;
existence
proof
defpred P[object,object] means
ex R being TolStr st R = C.$1 & $2 = the ToleranceRel of R;
A1: for i being object st i in I ex j being object st P[i,j]
proof
let i be object;
assume
A2: i in I;
then reconsider I as non empty set;
reconsider B = C as TolStr-yielding ManySortedSet of I;
reconsider i9 = i as Element of I by A2;
take the ToleranceRel of B.i9, B.i9;
thus thesis;
end;
consider M being Function such that
A3: dom M = I and
A4: for i being object st i in I holds P[i,M.i] from CLASSES1:sch 1(A1);
reconsider M as ManySortedSet of I by A3,PARTFUN1:def 2,RELAT_1:def 18;
take M;
thus thesis by A4;
end;
uniqueness
proof
let X, Y be ManySortedSet of I such that
A5: for j being set st j in I
ex R being TolStr st R = C.j & X.j = the ToleranceRel of R and
A6: for j being set st j in I
ex R being TolStr st R = C.j & Y.j = the ToleranceRel of R;
for i being object st i in I holds X.i = Y.i
proof
let i be object;
assume
A7: i in I;
then
A8: ex R being TolStr st R = C.i & X.i = the ToleranceRel of R by A5;
ex R being TolStr st R = C.i & Y.i = the ToleranceRel of R by A6,A7;
hence thesis by A8;
end;
hence thesis by PBOOLE:3;
end;
end;
definition
let I be non empty set, C be TolStr-yielding ManySortedSet of I;
redefine func pcs-ToleranceRels C means :: redefines pcs-ToleranceRels (PCS_0, definition)
:Def20:
for i being Element of I holds it.i = the ToleranceRel of C.i;
compatibility
proof
let X be ManySortedSet of I;
thus X = pcs-ToleranceRels C implies
for i being Element of I holds X.i = the ToleranceRel of C.i
proof
assume
A1: X = pcs-ToleranceRels C;
let i be Element of I;
ex P being TolStr st P = C.i & X.i = the ToleranceRel of P by A1,Def19;
hence thesis;
end;
assume
A2: for i being Element of I holds X.i = the ToleranceRel of C.i;
for i being set st i in I
ex P being TolStr st P = C.i & X.i = the ToleranceRel of P
proof
let i be set;
assume i in I;
then reconsider i as Element of I;
take C.i;
thus thesis by A2;
end;
hence thesis by Def19;
end;
end;
registration
let I be set, C be TolStr-yielding ManySortedSet of I;
cluster pcs-ToleranceRels C -> Relation-yielding;
coherence
proof
set TR = pcs-ToleranceRels C;
let i be object;
assume i in dom TR;
then ex P being TolStr st P = C.i & TR.i = the ToleranceRel of P by Def19;
hence thesis;
end;
end;
registration
let I be non empty set;
let C be pcs-tol-reflexive-yielding TolStr-yielding ManySortedSet of I;
let i be Element of I;
cluster C.i -> pcs-tol-reflexive for TolStr;
coherence
proof
dom C = I by PARTFUN1:def 2;
then C.i in rng C by FUNCT_1:3;
hence thesis by Def16;
end;
end;
registration
let I be non empty set;
let C be pcs-tol-irreflexive-yielding TolStr-yielding ManySortedSet of I;
let i be Element of I;
cluster C.i -> pcs-tol-irreflexive for TolStr;
coherence
proof
dom C = I by PARTFUN1:def 2;
then C.i in rng C by FUNCT_1:3;
hence thesis by Def17;
end;
end;
registration
let I be non empty set;
let C be pcs-tol-symmetric-yielding TolStr-yielding ManySortedSet of I;
let i be Element of I;
cluster C.i -> pcs-tol-symmetric for TolStr;
coherence
proof
dom C = I by PARTFUN1:def 2;
then C.i in rng C by FUNCT_1:3;
hence thesis by Def18;
end;
end;
theorem Th3:
for P, Q being TolStr st the TolStr of P = the TolStr of Q &
P is pcs-tol-reflexive holds Q is pcs-tol-reflexive;
theorem Th4:
for P, Q being TolStr st the TolStr of P = the TolStr of Q &
P is pcs-tol-irreflexive holds Q is pcs-tol-irreflexive;
theorem Th5:
for P, Q being TolStr st the TolStr of P = the TolStr of Q &
P is pcs-tol-symmetric holds Q is pcs-tol-symmetric;
definition
let P, Q be TolStr;
func [^P,Q^] -> TolStr equals
TolStr (# [: the carrier of P, the carrier of Q :],
[^ the ToleranceRel of P, the ToleranceRel of Q ^] #);
coherence;
end;
notation
let P, Q be TolStr, p be Element of P, q be Element of Q;
synonym [^p,q^] for [p,q];
end;
definition
let P, Q be non empty TolStr, p be Element of P, q be Element of Q;
redefine func [^p,q^] -> Element of [^P,Q^]; :: redefines [^ (PCS_0, synonym) → [ (TARSKI, definition)
coherence
proof
[p,q] is Element of [^P,Q^];
hence thesis;
end;
end;
notation
let P, Q be TolStr, 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, p be Element of [^P,Q^];
redefine func p^`1 -> Element of P; :: redefines ^`1 (PCS_0, synonym) → `1 (XTUPLE_0, definition)
coherence by MCART_1:10;
redefine func p^`2 -> Element of Q; :: redefines ^`2 (PCS_0, synonym) → `2 (XTUPLE_0, definition)
coherence by MCART_1:10;
end;
theorem Th6:
for S1, S2 being non empty TolStr
for a, c being Element of S1, b, d being Element of S2 holds
[^a,b^] (--) [^c,d^] iff a (--) c or b (--) d
by Def3;
theorem
for S1, S2 being non empty TolStr, x, y being Element of [^S1,S2^] holds
x (--) y iff x^`1 (--) y^`1 or x^`2 (--) y^`2
proof
let S1, S2 be non empty TolStr, x, y be Element of [^S1,S2^];
A1: ex a, b being object st a in the carrier of S1 & b in the carrier of S2 &
x = [a,b] by ZFMISC_1:def 2;
A2: ex c, d being object st c in the carrier of S1 & d in the carrier of S2 &
y = [c,d] by ZFMISC_1:def 2;
A3: x = [x^`1,x^`2] by A1;
y = [y^`1,y^`2] by A2;
hence thesis by A3,Th6;
end;
registration
let P be TolStr, Q be pcs-tol-reflexive TolStr;
cluster [^P,Q^] -> pcs-tol-reflexive;
coherence
proof
let x be object;
assume x in the carrier of [^P,Q^];
then consider x1, x2 being object such that
A1: x1 in the carrier of P and
A2: x2 in the carrier of Q and
A3: x = [x1,x2] by ZFMISC_1:def 2;
reconsider D2 = the carrier of Q as non empty set by A2;
reconsider TQ = the ToleranceRel of Q as Relation of D2;
D2 = field TQ by ORDERS_1:12;
then TQ is_reflexive_in D2 by RELAT_2:def 9;
then [x2,x2] in TQ by A2;
hence thesis by A1,A2,A3,Def3;
end;
end;
registration
let P be pcs-tol-reflexive TolStr, Q be TolStr;
cluster [^P,Q^] -> pcs-tol-reflexive;
coherence
proof
let x be object;
assume x in the carrier of [^P,Q^];
then consider x1, x2 being object such that
A1: x1 in the carrier of P and
A2: x2 in the carrier of Q and
A3: x = [x1,x2] by ZFMISC_1:def 2;
reconsider D1 = the carrier of P as non empty set by A1;
reconsider TP = the ToleranceRel of P as Relation of D1;
D1 = field TP by ORDERS_1:12;
then TP is_reflexive_in D1 by RELAT_2:def 9;
then [x1,x1] in TP by A1;
hence thesis by A1,A2,A3,Def3;
end;
end;
registration
let P, Q be pcs-tol-symmetric TolStr;
cluster [^P,Q^] -> pcs-tol-symmetric;
coherence
proof
set R = [^P,Q^];
set TR = the ToleranceRel of R;
A1: TR is_symmetric_in field TR by RELAT_2:def 11;
let x, y be object;
assume that x in the carrier of R and y in the carrier of R;
assume
A2: [x,y] in TR;
then
A3: x in field TR by RELAT_1:15;
y in field TR by A2,RELAT_1:15;
hence thesis by A1,A2,A3;
end;
end;
begin :: PCS's
definition
struct (RelStr,TolStr) pcs-Str (# carrier -> set,
InternalRel -> (Relation of the carrier),
ToleranceRel -> Relation of the carrier #);
end;
definition
let P be pcs-Str;
attr P is pcs-compatible means
:Def22:
for p, p9, q, q9 being Element of P st
p (--) q & p9 <= p & q9 <= q holds p9 (--) q9;
end;
definition
let P be pcs-Str;
attr P is pcs-like means
P is reflexive transitive pcs-tol-reflexive pcs-tol-symmetric pcs-compatible;
attr P is anti-pcs-like means
P is reflexive transitive pcs-tol-irreflexive pcs-tol-symmetric
pcs-compatible;
end;
registration
cluster pcs-like -> reflexive transitive pcs-tol-reflexive pcs-tol-symmetric
pcs-compatible for pcs-Str;
coherence;
cluster reflexive transitive pcs-tol-reflexive pcs-tol-symmetric
pcs-compatible -> pcs-like for pcs-Str;
coherence;
cluster anti-pcs-like -> reflexive transitive pcs-tol-irreflexive
pcs-tol-symmetric pcs-compatible for pcs-Str;
coherence;
cluster reflexive transitive pcs-tol-irreflexive pcs-tol-symmetric
pcs-compatible -> anti-pcs-like for pcs-Str;
coherence;
end;
definition
let D be set;
func pcs-total D -> pcs-Str equals
pcs-Str (# D,nabla D,nabla D #);
coherence;
end;
registration
let D be set;
cluster pcs-total D -> strict;
coherence;
end;
registration
let D be non empty set;
cluster pcs-total D -> non empty;
coherence;
end;
registration
let D be set;
cluster pcs-total D -> reflexive transitive
pcs-tol-reflexive pcs-tol-symmetric;
coherence
proof
set P = pcs-total D;
set IR = the InternalRel of P;
set TR = the ToleranceRel of P;
A1: field IR = the carrier of P by ORDERS_1:12;
hence IR is_reflexive_in the carrier of P by RELAT_2:def 9;
thus IR is_transitive_in the carrier of P by A1,RELAT_2:def 16;
thus TR is_reflexive_in the carrier of P by A1,RELAT_2:def 9;
thus TR is_symmetric_in the carrier of P by A1,RELAT_2:def 11;
end;
end;
registration
let D be set;
cluster pcs-total D -> pcs-like;
coherence
proof
set P = pcs-total D;
thus P is reflexive transitive;
thus P is pcs-tol-reflexive pcs-tol-symmetric;
let p, p9, q, q9 be Element of P such that p (--) q;
assume that
A1: p9 <= p and q9 <= q;
[p9,p] in [:D,D:] by A1;
then p9 in the carrier of P by ZFMISC_1:87;
hence [p9,q9] in the ToleranceRel of P by ZFMISC_1:87;
end;
end;
registration
let D be set;
cluster pcs-Str(#D,nabla D,{}(D,D)#) -> anti-pcs-like;
coherence
proof
set P = pcs-Str(#D,nabla D,{}(D,D)#);
A1: the RelStr of P = the RelStr of RelStr(#D,nabla D#);
hence P is reflexive by WAYBEL_8:12;
thus P is transitive by A1,WAYBEL_8:13;
A2: the TolStr of P = the TolStr of TolStr(#D,{}(D,D)#);
hence P is pcs-tol-irreflexive by Th4;
thus P is pcs-tol-symmetric by A2,Th5;
let p be Element of P;
thus thesis;
end;
end;
registration
cluster strict non empty pcs-like for pcs-Str;
existence
proof
take P = pcs-total {{}};
thus P is strict;
thus the carrier of P is non empty;
thus thesis;
end;
cluster strict non empty anti-pcs-like for pcs-Str;
existence
proof
take P = pcs-Str(#{{}},nabla {{}},{}({{}},{{}})#);
thus P is strict;
thus the carrier of P is non empty;
thus thesis;
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-total 0;
coherence;
end;
registration
cluster pcs-empty -> strict empty pcs-like;
coherence;
end;
definition
let p be set;
func pcs-singleton p -> pcs-Str equals
pcs-total {p};
coherence;
end;
registration
let p be set;
cluster pcs-singleton p -> strict non empty pcs-like;
coherence;
end;
definition
let R be Relation;
attr R is pcs-Str-yielding means
for P being set st P in rng R holds P is pcs-Str;
attr R is pcs-yielding means
for P being set st P in rng R holds P is pcs;
end;
definition
let f be Function;
redefine attr f is pcs-Str-yielding means :: redefines pcs-Str-yielding (PCS_0, definition)
for x being set st x in dom f holds f.x is pcs-Str;
compatibility
proof
thus f is pcs-Str-yielding implies
for x being set st x in dom f holds f.x is pcs-Str by FUNCT_1:3;
assume
A1: for x being set st x in dom f holds f.x is pcs-Str;
let P be set;
assume P in rng f;
then ex x being object st x in dom f & f.x = P by FUNCT_1:def 3;
hence thesis by A1;
end;
redefine attr f is pcs-yielding means :: redefines pcs-yielding (PCS_0, definition)
for x being set st x in dom f holds f.x is pcs;
compatibility
proof
thus f is pcs-yielding implies
for x being set st x in dom f holds f.x is pcs by FUNCT_1:3;
assume
A2: for x being set st x in dom f holds f.x is pcs;
let P be set;
assume P in rng f;
then ex x being object st x in dom f & f.x = P by FUNCT_1:def 3;
hence thesis by A2;
end;
end;
definition
let I be set, f be ManySortedSet of I;
A1: dom f = I by PARTFUN1:def 2;
redefine attr f is pcs-Str-yielding means :: redefines pcs-Str-yielding (PCS_0, redefinition) → pcs-Str-yielding (PCS_0, definition)
:Def32:
for x being set st x in I holds f.x is pcs-Str;
compatibility by A1;
redefine attr f is pcs-yielding means :: redefines pcs-yielding (PCS_0, redefinition) → pcs-yielding (PCS_0, definition)
:Def33:
for x being set st x in I holds f.x is pcs;
compatibility by A1;
end;
registration
cluster pcs-Str-yielding -> TolStr-yielding RelStr-yielding for Relation;
coherence
proof
let f be Relation;
assume
A1: f is pcs-Str-yielding;
thus f is TolStr-yielding
by A1;
let y be set;
thus thesis by A1;
end;
cluster pcs-yielding -> pcs-Str-yielding for Relation;
coherence;
cluster pcs-yielding -> reflexive-yielding transitive-yielding
pcs-tol-reflexive-yielding pcs-tol-symmetric-yielding for Relation;
coherence;
end;
registration
let I be set, P be pcs;
cluster I --> P -> pcs-yielding for ManySortedSet of I;
coherence
by FUNCOP_1:7;
end;
registration
let I be set;
cluster pcs-yielding for ManySortedSet of I;
existence
proof
take I --> pcs-empty;
thus thesis;
end;
end;
definition
let I be non empty set, C be pcs-Str-yielding ManySortedSet of I,
i be Element of I;
redefine func C.i -> pcs-Str; :: redefines . (FUNCT_1, definition)
coherence by Def32;
end;
definition
let I be non empty set, C be pcs-yielding ManySortedSet of I,
i be Element of I;
redefine func C.i -> pcs; :: redefines . (FUNCT_1, definition)
coherence by Def33;
end;
:: Union of PCS's
definition
let P, Q be pcs-Str;
pred P c= Q means
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;
end;
theorem
for P, Q being RelStr
for p, q being Element of P, 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
for P, Q being TolStr
for p, q being Element of P, 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:
for P, Q being pcs-Str st P in rng C & Q in rng C holds P c= Q or Q c= P;
end;
registration
let I be set, P be pcs-Str;
cluster I --> P -> pcs-chain-like for ManySortedSet of I;
coherence
proof
set f = I --> P;
f is pcs-chain-like
proof
let R, S be pcs-Str;
assume that
A1: R in rng f and
A2: S in rng f;
P = R & P = S or rng f = {} by A1,A2,TARSKI:def 1;
hence thesis by A1;
end;
hence thesis;
end;
end;
registration
cluster pcs-chain-like pcs-yielding for Function;
existence
proof
set P = the pcs;
take 0 --> P;
thus thesis;
end;
end;
registration
let I be set;
cluster pcs-chain-like pcs-yielding for ManySortedSet of I;
existence
proof
set P = the pcs;
take I --> P;
thus thesis;
end;
end;
definition
let I be set;
mode pcs-Chain of I is pcs-chain-like pcs-yielding ManySortedSet of I;
end;
definition
let I be set, C be pcs-Str-yielding ManySortedSet of I;
func pcs-union C -> strict pcs-Str means
:Def36:
the carrier of it = Union Carrier C &
the InternalRel of it = Union pcs-InternalRels C &
the ToleranceRel of it = Union pcs-ToleranceRels C;
existence
proof
set CA = Carrier C;
set IRA = pcs-InternalRels C;
set TRA = pcs-ToleranceRels C;
set D = Union CA;
set IR = Union IRA;
set TR = Union TRA;
A1: dom CA = I by PARTFUN1:def 2;
IR c= [:D,D:]
proof
let x be object;
assume x in IR;
then consider P being set such that
A2: x in P and
A3: P in rng IRA by TARSKI:def 4;
consider i being object such that
A4: i in dom IRA and
A5: IRA.i = P by A3,FUNCT_1:def 3;
consider R being RelStr such that
A6: R = C.i and
A7: IRA.i = the InternalRel of R by A4,Def5;
consider x1, x2 being object such that
A8: x = [x1,x2] and
A9: x1 in the carrier of R and
A10: x2 in the carrier of R by A2,A5,A7,RELSET_1:2;
ex S being 1-sorted st S = C.i & CA.i = the carrier of S
by A4,PRALG_1:def 15;
then
A11: the carrier of R in rng CA by A1,A4,A6,FUNCT_1:def 3;
then
A12: x1 in union rng CA by A9,TARSKI:def 4;
x2 in union rng CA by A10,A11,TARSKI:def 4;
hence thesis by A8,A12,ZFMISC_1:87;
end;
then reconsider IR as Relation of D;
TR c= [:D,D:]
proof
let x be object;
assume x in TR;
then consider P being set such that
A13: x in P and
A14: P in rng TRA by TARSKI:def 4;
consider i being object such that
A15: i in dom TRA and
A16: TRA.i = P by A14,FUNCT_1:def 3;
consider R being TolStr such that
A17: R = C.i and
A18: TRA.i = the ToleranceRel of R by A15,Def19;
consider x1, x2 being object such that
A19: x = [x1,x2] and
A20: x1 in the carrier of R and
A21: x2 in the carrier of R by A13,A16,A18,RELSET_1:2;
ex S being 1-sorted st S = C.i & CA.i = the carrier of S
by A15,PRALG_1:def 15;
then
A22: the carrier of R in rng CA by A1,A15,A17,FUNCT_1:def 3;
then
A23: x1 in union rng CA by A20,TARSKI:def 4;
x2 in union rng CA by A21,A22,TARSKI:def 4;
hence thesis by A19,A23,ZFMISC_1:87;
end;
then reconsider TR as Relation of D;
take pcs-Str(#D,IR,TR#);
thus thesis;
end;
uniqueness;
end;
theorem Th10:
for I being set, C being pcs-Str-yielding ManySortedSet of I
for p, q being Element of pcs-union C holds p <= q iff
ex i being object, P being pcs-Str, p9, q9 being Element of P st
i in I & P = C.i & p9 = p & q9 = q & p9 <= q9
proof
let I be set, C be pcs-Str-yielding ManySortedSet of I;
set R = pcs-union C;
let p, q be Element of R;
A1: dom pcs-InternalRels C = I by PARTFUN1:def 2;
thus p <= q implies
ex i being object, P being pcs-Str, p9, q9 being Element of P st
i in I & P = C.i & p9 = p & q9 = q & p9 <= q9
proof
assume p <= q;
then [p,q] in the InternalRel of R;
then [p,q] in Union pcs-InternalRels C by Def36;
then consider Z being set such that
A2: [p,q] in Z and
A3: Z in rng pcs-InternalRels C by TARSKI:def 4;
consider i being object such that
A4: i in dom pcs-InternalRels C and
A5: (pcs-InternalRels C).i = Z by A3,FUNCT_1:def 3;
reconsider I1 = I as non empty set by A4;
reconsider A1 = C as pcs-Str-yielding ManySortedSet of I1;
reconsider i1 = i as Element of I1 by A4;
reconsider P = A1.i1 as pcs-Str;
take i, P;
Z = the InternalRel of A1.i1 by A5,Def6;
then reconsider p9 = p, q9 = q as Element of P by A2,ZFMISC_1:87;
take p9, q9;
thus i in I by A4;
thus P = C.i & p9 = p & q9 = q;
thus [p9,q9] in the InternalRel of P by A2,A5,Def6;
end;
given i being object, P being pcs-Str, p9, q9 being Element of P such that
A6: i in I and
A7: P = C.i and
A8: p9 = p and
A9: q9 = q and
A10: p9 <= q9;
A11: [p9,q9] in the InternalRel of P by A10;
reconsider I1 = I as non empty set by A6;
reconsider i1 = i as Element of I1 by A6;
reconsider A1 = C as pcs-Str-yielding ManySortedSet of I1;
(pcs-InternalRels A1).i1 = the InternalRel of A1.i1 by Def6;
then the InternalRel of A1.i1 in rng pcs-InternalRels C by A1,FUNCT_1:3;
then [p,q] in Union pcs-InternalRels C by A7,A8,A9,A11,TARSKI:def 4;
hence [p,q] in the InternalRel of R by Def36;
end;
theorem
for I being non empty set, C being pcs-Str-yielding ManySortedSet of I
for p, q being Element of pcs-union C holds p <= q iff
ex i being Element of I, p9, q9 being Element of C.i st
p9 = p & q9 = q & p9 <= q9
proof
let I be non empty set, C be pcs-Str-yielding ManySortedSet of I;
let p, q be Element of pcs-union C;
thus
p <= q implies ex i being Element of I, p9, q9 being Element of C.i st
p9 = p & q9 = q & p9 <= q9
proof
assume p <= q;
then ex i being object, P being pcs-Str, p9, q9 being Element of P st
i in I & P = C.i & p9 = p & q9 = q & p9 <= q9 by Th10;
hence thesis;
end;
thus thesis by Th10;
end;
theorem Th12:
for I being set, C being pcs-Str-yielding ManySortedSet of I
for p, q being Element of pcs-union C holds p (--) q iff
ex i being object, P being pcs-Str, p9, q9 being Element of P st
i in I & P = C.i & p9 = p & q9 = q & p9 (--) q9
proof
let I be set, C be pcs-Str-yielding ManySortedSet of I;
set R = pcs-union C;
let p, q be Element of R;
A1: dom pcs-ToleranceRels C = I by PARTFUN1:def 2;
thus p (--) q implies
ex i being object, P being pcs-Str, p9, q9 being Element of P st
i in I & P = C.i & p9 = p & q9 = q & p9 (--) q9
proof
assume p (--) q;
then [p,q] in the ToleranceRel of R;
then [p,q] in Union pcs-ToleranceRels C by Def36;
then consider Z being set such that
A2: [p,q] in Z and
A3: Z in rng pcs-ToleranceRels C by TARSKI:def 4;
consider i being object such that
A4: i in dom pcs-ToleranceRels C and
A5: (pcs-ToleranceRels C).i = Z by A3,FUNCT_1:def 3;
reconsider I1 = I as non empty set by A4;
reconsider A1 = C as pcs-Str-yielding ManySortedSet of I1;
reconsider i1 = i as Element of I1 by A4;
reconsider P = A1.i1 as pcs-Str;
take i, P;
Z = the ToleranceRel of A1.i1 by A5,Def20;
then reconsider p9 = p, q9 = q as Element of P by A2,ZFMISC_1:87;
take p9, q9;
thus i in I by A4;
thus P = C.i & p9 = p & q9 = q;
thus [p9,q9] in the ToleranceRel of P by A2,A5,Def20;
end;
given i being object, P being pcs-Str, p9, q9 being Element of P such that
A6: i in I and
A7: P = C.i and
A8: p9 = p and
A9: q9 = q and
A10: p9 (--) q9;
A11: [p9,q9] in the ToleranceRel of P by A10;
reconsider I1 = I as non empty set by A6;
reconsider i1 = i as Element of I1 by A6;
reconsider A1 = C as pcs-Str-yielding ManySortedSet of I1;
(pcs-ToleranceRels A1).i1 = the ToleranceRel of A1.i1 by Def20;
then the ToleranceRel of A1.i1 in rng pcs-ToleranceRels C by A1,FUNCT_1:3;
then [p,q] in Union pcs-ToleranceRels C by A7,A8,A9,A11,TARSKI:def 4;
hence [p,q] in the ToleranceRel of R by Def36;
end;
theorem
for I being non empty set, C being pcs-Str-yielding ManySortedSet of I
for p, q being Element of pcs-union C holds p (--) q iff
ex i being Element of I, p9, q9 being Element of C.i st
p9 = p & q9 = q & p9 (--) q9
proof
let I be non empty set, C be pcs-Str-yielding ManySortedSet of I;
let p, q be Element of pcs-union C;
thus p (--) q implies ex i being Element of I, p9, q9 being Element of C.i st
p9 = p & q9 = q & p9 (--) q9
proof
assume p (--) q;
then ex i being object, P being pcs-Str, p9, q9 being Element of P st
i in I & P = C.i & p9 = p & q9 = q & p9 (--) q9 by Th12;
hence thesis;
end;
thus thesis by Th12;
end;
registration
let I be set, C be reflexive-yielding pcs-Str-yielding ManySortedSet of I;
cluster pcs-union C -> reflexive;
coherence
proof
set P = pcs-union C;
set IR = the InternalRel of P;
set CP = the carrier of P;
set CA = Carrier C;
A1: CP = Union CA by Def36;
A2: IR = Union pcs-InternalRels C by Def36;
A3: dom pcs-InternalRels C = I by PARTFUN1:def 2;
let x be object;
assume x in CP;
then consider P being set such that
A4: x in P and
A5: P in rng CA by A1,TARSKI:def 4;
consider i being object such that
A6: i in dom CA and
A7: CA.i = P by A5,FUNCT_1:def 3;
A8: ex R being 1-sorted st ( R = C.i)&( CA.i = the carrier of R)
by A6,PRALG_1:def 15;
reconsider I as non empty set by A6;
reconsider i as Element of I by A6;
reconsider C as reflexive-yielding pcs-Str-yielding ManySortedSet of I;
A9: (pcs-InternalRels C).i = the InternalRel of C.i by Def6;
the InternalRel of C.i is_reflexive_in the carrier of C.i
by ORDERS_2:def 2;
then
A10: [x,x] in the InternalRel of C.i by A4,A7,A8;
the InternalRel of C.i in rng pcs-InternalRels C by A3,A9,FUNCT_1:3;
hence thesis by A2,A10,TARSKI:def 4;
end;
end;
registration
let I be set,
C be pcs-tol-reflexive-yielding pcs-Str-yielding ManySortedSet of I;
cluster pcs-union C -> pcs-tol-reflexive;
coherence
proof
set P = pcs-union C;
set TR = the ToleranceRel of P;
set CP = the carrier of P;
set CA = Carrier C;
A1: CP = Union CA by Def36;
A2: TR = Union pcs-ToleranceRels C by Def36;
A3: dom pcs-ToleranceRels C = I by PARTFUN1:def 2;
let x be object;
assume x in CP;
then consider P being set such that
A4: x in P and
A5: P in rng CA by A1,TARSKI:def 4;
consider i being object such that
A6: i in dom CA and
A7: CA.i = P by A5,FUNCT_1:def 3;
A8: ex R being 1-sorted st ( R = C.i)&( CA.i = the carrier of R)
by A6,PRALG_1:def 15;
reconsider I as non empty set by A6;
reconsider i as Element of I by A6;
reconsider C as pcs-tol-reflexive-yielding pcs-Str-yielding
ManySortedSet of I;
A9: (pcs-ToleranceRels C).i = the ToleranceRel of C.i by Def20;
the ToleranceRel of C.i is_reflexive_in the carrier of C.i by Def9;
then
A10: [x,x] in the ToleranceRel of C.i by A4,A7,A8;
the ToleranceRel of C.i in rng pcs-ToleranceRels C by A3,A9,FUNCT_1:3;
hence thesis by A2,A10,TARSKI:def 4;
end;
end;
registration
let I be set,
C be pcs-tol-symmetric-yielding pcs-Str-yielding ManySortedSet of I;
cluster pcs-union C -> pcs-tol-symmetric;
coherence
proof
set P = pcs-union C;
set TR = the ToleranceRel of P;
set CP = the carrier of P;
A1: TR = Union pcs-ToleranceRels C by Def36;
let x, y be object;
assume that x in CP and y in CP;
assume [x,y] in TR;
then consider P being set such that
A2: [x,y] in P and
A3: P in rng pcs-ToleranceRels C by A1,TARSKI:def 4;
consider i being object such that
A4: i in dom pcs-ToleranceRels C and
A5: (pcs-ToleranceRels C).i = P by A3,FUNCT_1:def 3;
reconsider I as non empty set by A4;
reconsider C as pcs-tol-symmetric-yielding pcs-Str-yielding
ManySortedSet of I;
reconsider i as Element of I by A4;
A6: (pcs-ToleranceRels C).i = the ToleranceRel of C.i by Def20;
then
A7: x in the carrier of C.i by A2,A5,ZFMISC_1:87;
A8: y in the carrier of C.i by A2,A5,A6,ZFMISC_1:87;
the ToleranceRel of C.i is_symmetric_in the carrier of C.i by Def11;
then
A9: [y,x] in the ToleranceRel of C.i by A2,A5,A6,A7,A8;
the ToleranceRel of C.i in rng pcs-ToleranceRels C by A4,A6,FUNCT_1:3;
hence thesis by A1,A9,TARSKI:def 4;
end;
end;
registration
let I be set, C be pcs-Chain of I;
cluster pcs-union C -> transitive pcs-compatible;
coherence
proof
set P = pcs-union C;
set IR = the InternalRel of P;
set TR = the ToleranceRel of P;
set CA = the carrier of P;
A1: IR = Union pcs-InternalRels C by Def36;
A2: TR = Union pcs-ToleranceRels C by Def36;
A3: dom C = I by PARTFUN1:def 2;
thus P is transitive
proof
let x, y, z be object;
assume that x in CA and y in CA
and z in CA;
assume [x,y] in IR;
then consider Z1 being set such that
A4: [x,y] in Z1 and
A5: Z1 in rng pcs-InternalRels C by A1,TARSKI:def 4;
consider i being object such that
A6: i in dom pcs-InternalRels C and
A7: (pcs-InternalRels C).i = Z1 by A5,FUNCT_1:def 3;
assume [y,z] in IR;
then consider Z2 being set such that
A8: [y,z] in Z2 and
A9: Z2 in rng pcs-InternalRels C by A1,TARSKI:def 4;
consider j being object such that
A10: j in dom pcs-InternalRels C and
A11: (pcs-InternalRels C).j = Z2 by A9,FUNCT_1:def 3;
reconsider I as non empty set by A6;
reconsider C as pcs-Chain of I;
reconsider i, j as Element of I by A6,A10;
A12: (pcs-InternalRels C).i = the InternalRel of C.i by Def6;
then
A13: x in the carrier of C.i by A4,A7,ZFMISC_1:87;
A14: y in the carrier of C.i by A4,A7,A12,ZFMISC_1:87;
A15: (pcs-InternalRels C).j = the InternalRel of C.j by Def6;
A16: C.i in rng C by A3,FUNCT_1:3;
A17: C.j in rng C by A3,FUNCT_1:3;
A18: the InternalRel of C.i is_transitive_in the carrier of C.i
by ORDERS_2:def 3;
A19: the InternalRel of C.j is_transitive_in the carrier of C.j
by ORDERS_2:def 3;
per cases by A16,A17,Def35;
suppose C.i c= C.j;
then
A20: the InternalRel of C.i c= the InternalRel of C.j;
then
A21: [x,y] in the InternalRel of C.j by A4,A7,A12;
then
A22: x in the carrier of C.j by ZFMISC_1:87;
A23: y in the carrier of C.j by A21,ZFMISC_1:87;
z in the carrier of C.j by A8,A11,A15,ZFMISC_1:87;
then
A24: [x,z] in the InternalRel of C.j by A4,A7,A8,A11,A12,A15,A19,A20,A22,A23
;
the InternalRel of C.j c= IR by A1,A9,A11,A15,ZFMISC_1:74;
hence thesis by A24;
end;
suppose C.j c= C.i;
then
A25: the InternalRel of C.j c= the InternalRel of C.i;
then [y,z] in the InternalRel of C.i by A8,A11,A15;
then z in the carrier of C.i by ZFMISC_1:87;
then
A26: [x,z] in the InternalRel of C.i by A4,A7,A8,A11,A12,A13,A14,A15,A18,A25
;
the InternalRel of C.i c= IR by A1,A5,A7,A12,ZFMISC_1:74;
hence thesis by A26;
end;
end;
let p, p9, q, q9 be Element of P such that
A27: p (--) q and
A28: p9 <= p and
A29: q9 <= q;
[p9,p] in IR by A28;
then consider Z1 being set such that
A30: [p9,p] in Z1 and
A31: Z1 in rng pcs-InternalRels C by A1,TARSKI:def 4;
consider i being object such that
A32: i in dom pcs-InternalRels C and
A33: (pcs-InternalRels C).i = Z1 by A31,FUNCT_1:def 3;
reconsider I as non empty set by A32;
reconsider C as pcs-Chain of I;
reconsider i as Element of I by A32;
A34: (pcs-ToleranceRels C).i = the ToleranceRel of C.i by Def20;
A35: (pcs-InternalRels C).i = the InternalRel of C.i by Def6;
then reconsider pi1 = p, p9i = p9 as Element of C.i
by A30,A33,ZFMISC_1:87;
[q9,q] in IR by A29;
then consider Z2 being set such that
A36: [q9,q] in Z2 and
A37: Z2 in rng pcs-InternalRels C by A1,TARSKI:def 4;
consider j being object such that
A38: j in dom pcs-InternalRels C and
A39: (pcs-InternalRels C).j = Z2 by A37,FUNCT_1:def 3;
reconsider j as Element of I by A38;
A40: (pcs-ToleranceRels C).j = the ToleranceRel of C.j by Def20;
A41: (pcs-InternalRels C).j = the InternalRel of C.j by Def6;
then
A42: q9 in the carrier of C.j by A36,A39,ZFMISC_1:87;
A43: q in the carrier of C.j by A36,A39,A41,ZFMISC_1:87;
reconsider qj = q as Element of C.j by A36,A39,A41,ZFMISC_1:87;
[p,q] in TR by A27;
then consider Z3 being set such that
A44: [p,q] in Z3 and
A45: Z3 in rng pcs-ToleranceRels C by A2,TARSKI:def 4;
consider k being object such that
A46: k in dom pcs-ToleranceRels C and
A47: (pcs-ToleranceRels C).k = Z3 by A45,FUNCT_1:def 3;
reconsider k as Element of I by A46;
A48: (pcs-ToleranceRels C).k = the ToleranceRel of C.k by Def20;
then reconsider pk = p, qk = q as Element of C.k by A44,A47,ZFMISC_1:87;
A49: C.i in rng C by A3,FUNCT_1:3;
A50: C.j in rng C by A3,FUNCT_1:3;
A51: C.k in rng C by A3,FUNCT_1:3;
A52: dom pcs-ToleranceRels C = I by PARTFUN1:def 2;
then
A53: the ToleranceRel of C.i c= TR by A2,A34,FUNCT_1:3,ZFMISC_1:74;
A54: the ToleranceRel of C.j c= TR by A2,A40,A52,FUNCT_1:3,ZFMISC_1:74;
A55: the ToleranceRel of C.k c= TR by A2,A45,A47,A48,ZFMISC_1:74;
per cases by A49,A50,A51,Def35;
suppose that
A56: C.i c= C.j and
A57: C.j c= C.k;
A58: the InternalRel of C.j c= the InternalRel of C.k by A57;
the InternalRel of C.i c= the InternalRel of C.j by A56;
then
A59: [p9,p] in the InternalRel of C.j by A30,A33,A35;
then [p9,p] in the InternalRel of C.k by A58;
then reconsider p9k = p9 as Element of C.k by ZFMISC_1:87;
[q9,q] in the InternalRel of C.k by A36,A39,A41,A58;
then reconsider q9k = q9 as Element of C.k by ZFMISC_1:87;
A60: p9k <= pk by A58,A59;
A61: q9k <= qk by A36,A39,A41,A58;
pk (--) qk by A44,A47,A48;
then p9k (--) q9k by A60,A61,Def22;
then [p9k,q9k] in the ToleranceRel of C.k;
hence [p9,q9] in TR by A55;
end;
suppose that
A62: C.j c= C.i and
A63: C.i c= C.k;
A64: the InternalRel of C.i c= the InternalRel of C.k by A63;
A65: the InternalRel of C.j c= the InternalRel of C.i by A62;
[p9,p] in the InternalRel of C.k by A30,A33,A35,A64;
then reconsider p9k = p9 as Element of C.k by ZFMISC_1:87;
A66: [q9,q] in the InternalRel of C.i by A36,A39,A41,A65;
then [q9,q] in the InternalRel of C.k by A64;
then reconsider q9k = q9 as Element of C.k by ZFMISC_1:87;
A67: p9k <= pk by A30,A33,A35,A64;
A68: q9k <= qk by A64,A66;
pk (--) qk by A44,A47,A48;
then p9k (--) q9k by A67,A68,Def22;
then [p9k,q9k] in the ToleranceRel of C.k;
hence [p9,q9] in TR by A55;
end;
suppose that
A69: C.i c= C.k and
A70: C.k c= C.j;
A71: the InternalRel of C.k c= the InternalRel of C.j by A70;
A72: the ToleranceRel of C.k c= the ToleranceRel of C.j by A70;
the InternalRel of C.i c= the InternalRel of C.k by A69;
then
A73: [p9,p] in the InternalRel of C.k by A30,A33,A35;
then
A74: [p9,p] in the InternalRel of C.j by A71;
then reconsider p9j = p9 as Element of C.j by ZFMISC_1:87;
reconsider q9j = q9 as Element of C.j by A36,A39,A41,ZFMISC_1:87;
reconsider pj = p as Element of C.j by A74,ZFMISC_1:87;
A75: p9j <= pj by A71,A73;
A76: q9j <= qj by A36,A39,A41;
pj (--) qj by A44,A47,A48,A72;
then p9j (--) q9j by A75,A76,Def22;
then [p9j,q9j] in the ToleranceRel of C.j;
hence [p9,q9] in TR by A54;
end;
suppose that
A77: C.k c= C.i and
A78: C.i c= C.j;
A79: the InternalRel of C.i c= the InternalRel of C.j by A78;
A80: the ToleranceRel of C.i c= the ToleranceRel of C.j by A78;
A81: the ToleranceRel of C.k c= the ToleranceRel of C.i by A77;
A82: [p9,p] in the InternalRel of C.j by A30,A33,A35,A79;
then reconsider p9j = p9 as Element of C.j by ZFMISC_1:87;
reconsider q9j = q9 as Element of C.j by A36,A39,A41,ZFMISC_1:87;
reconsider pj = p as Element of C.j by A82,ZFMISC_1:87;
q in the carrier of C.k by A44,A47,A48,ZFMISC_1:87;
then reconsider qi = q as Element of C.i by A77;
A83: p9j <= pj by A30,A33,A35,A79;
A84: q9j <= qj by A36,A39,A41;
pi1 (--) qi by A44,A47,A48,A81;
then pj (--) qj by A80;
then p9j (--) q9j by A83,A84,Def22;
then [p9j,q9j] in the ToleranceRel of C.j;
hence [p9,q9] in TR by A54;
end;
suppose that
A85: C.k c= C.j and
A86: C.j c= C.i;
A87: the ToleranceRel of C.j c= the ToleranceRel of C.i by A86;
A88: the ToleranceRel of C.k c= the ToleranceRel of C.j by A85;
A89: the InternalRel of C.j c= the InternalRel of C.i by A86;
reconsider q9i = q9 as Element of C.i by A42,A86;
reconsider qi = q as Element of C.i by A43,A86;
p in the carrier of C.k by A44,A47,A48,ZFMISC_1:87;
then reconsider pj = p as Element of C.j by A85;
A90: p9i <= pi1 by A30,A33,A35;
A91: q9i <= qi by A36,A39,A41,A89;
pj (--) qj by A44,A47,A48,A88;
then pi1 (--) qi by A87;
then p9i (--) q9i by A90,A91,Def22;
then [p9i,q9i] in the ToleranceRel of C.i;
hence [p9,q9] in TR by A53;
end;
suppose that
A92: C.j c= C.k and
A93: C.k c= C.i;
A94: the ToleranceRel of C.k c= the ToleranceRel of C.i by A93;
A95: the InternalRel of C.k c= the InternalRel of C.i by A93;
A96: the InternalRel of C.j c= the InternalRel of C.k by A92;
reconsider q9k = q9 as Element of C.k by A42,A92;
A97: the carrier of C.j c= the carrier of C.k by A92;
then reconsider q9i = q9 as Element of C.i by A42,A93,Lm2;
reconsider qi = q as Element of C.i by A43,A93,A97,Lm2;
A98: q9k <= qk by A36,A39,A41,A96;
A99: p9i <= pi1 by A30,A33,A35;
A100: q9i <= qi by A95,A98;
pi1 (--) qi by A44,A47,A48,A94;
then p9i (--) q9i by A99,A100,Def22;
then [p9i,q9i] in the ToleranceRel of C.i;
hence [p9,q9] in TR by A53;
end;
end;
end;
:: Direct Sum of PCS's
definition let p,q be set;
func <%p,q%> -> ManySortedSet of {0,1} equals
<%p,q%>;
coherence by CARD_1:50;
end;
registration
let P, Q be 1-sorted;
cluster <%P,Q%> -> 1-sorted-yielding;
coherence;
end;
Lm3:
now
let a,b be object;
<%a,b%> = (0,1) --> (a,b) by AFINSQ_1:76;
hence rng <%a,b%> = {a,b} by FUNCT_4:64;
end;
registration
let P, Q be RelStr;
cluster <%P,Q%> -> RelStr-yielding;
coherence
proof
let x be set;
assume x in rng <%P,Q%>;
then x in {P,Q} by Lm3;
hence thesis by TARSKI:def 2;
end;
end;
registration
let P, Q be TolStr;
cluster <%P,Q%> -> TolStr-yielding;
coherence
proof
let x be set;
assume x in {0,1};
then x = 0 or x = 1 by TARSKI:def 2;
hence thesis;
end;
end;
registration
let P, Q be pcs-Str;
cluster <%P,Q%> -> pcs-Str-yielding;
coherence
proof
let x be set;
assume x in {0,1};
then x = 0 or x = 1 by TARSKI:def 2;
hence thesis;
end;
end;
registration
let P, Q be reflexive pcs-Str;
cluster <%P,Q%> -> reflexive-yielding;
coherence
proof
let x be RelStr;
assume x in rng <%P,Q%>;
then x in {P,Q} by Lm3;
hence thesis by TARSKI:def 2;
end;
end;
registration
let P, Q be transitive pcs-Str;
cluster <%P,Q%> -> transitive-yielding;
coherence
proof
let x be RelStr;
assume x in rng <%P,Q%>;
then x in {P,Q} by Lm3;
hence thesis by TARSKI:def 2;
end;
end;
registration
let P, Q be pcs-tol-reflexive pcs-Str;
cluster <%P,Q%> -> pcs-tol-reflexive-yielding;
coherence
proof
let x be TolStr;
assume x in rng <%P,Q%>;
then x in {P,Q} by Lm3;
hence thesis by TARSKI:def 2;
end;
end;
registration
let P, Q be pcs-tol-symmetric pcs-Str;
cluster <%P,Q%> -> pcs-tol-symmetric-yielding;
coherence
proof
let x be TolStr;
assume x in rng <%P,Q%>;
then x in {P,Q} by Lm3;
hence thesis by TARSKI:def 2;
end;
end;
registration
let P, Q be pcs;
cluster <%P,Q%> -> pcs-yielding;
coherence
proof
let x be set;
assume x in {0,1};
then x = 0 or x = 1 by TARSKI:def 2;
hence thesis;
end;
end;
definition
::$CD
let P, Q be pcs-Str;
func pcs-sum(P,Q) -> pcs-Str equals
pcs-union <%P,Q%>;
coherence;
end;
deffunc pcsSUM(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:
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
let P, Q be pcs-Str;
set S = pcsSUM(P,Q);
set f = <%P,Q%>;
A1: dom Carrier f = {0,1} by PARTFUN1:def 2;
A2: dom pcs-InternalRels f = {0,1} by PARTFUN1:def 2;
A3: dom pcs-ToleranceRels f = {0,1} by PARTFUN1:def 2;
A4: the carrier of S = Union Carrier f
proof
thus the carrier of S c= Union Carrier f
proof
let x be object;
assume x in the carrier of S;
then
A5: x in the carrier of P or x in the carrier of Q by XBOOLE_0:def 3;
A6: (Carrier f).z = the carrier of f.z by Def1;
A7: (Carrier f).j = the carrier of f.j by Def1;
A8: the carrier of P in rng Carrier f by A1,A6,FUNCT_1:3;
the carrier of Q in rng Carrier f by A1,A7,FUNCT_1:3;
hence thesis by A5,A8,TARSKI:def 4;
end;
let x be object;
assume x in Union Carrier f;
then consider Z being set such that
A9: x in Z and
A10: Z in rng Carrier f by TARSKI:def 4;
consider i being object such that
A11: i in dom Carrier f and
A12: Carrier f.i = Z by A10,FUNCT_1:def 3;
i = 0 or i = 1 by A11,TARSKI:def 2;
then Z = the carrier of f.z or Z = the carrier of f.j by A12,Def1;
hence thesis by A9,XBOOLE_0:def 3;
end;
A13: the InternalRel of S = Union pcs-InternalRels f
proof
thus the InternalRel of S c= Union pcs-InternalRels f
proof
let x be object;
assume x in the InternalRel of S;
then
A14: x in the InternalRel of P or x in the InternalRel of Q by XBOOLE_0:def 3;
A15: (pcs-InternalRels f).z = the InternalRel of f.z by Def6;
A16: (pcs-InternalRels f).j = the InternalRel of f.j by Def6;
A17: the InternalRel of P in rng pcs-InternalRels f by A2,A15,FUNCT_1:3;
the InternalRel of Q in rng pcs-InternalRels f by A2,A16,FUNCT_1:3;
hence thesis by A14,A17,TARSKI:def 4;
end;
let x be object;
assume x in Union pcs-InternalRels f;
then consider Z being set such that
A18: x in Z and
A19: Z in rng pcs-InternalRels f by TARSKI:def 4;
consider i being object such that
A20: i in dom pcs-InternalRels f and
A21: (pcs-InternalRels f).i = Z by A19,FUNCT_1:def 3;
i = 0 or i = 1 by A20,TARSKI:def 2;
then Z = the InternalRel of f.z or Z = the InternalRel of f.j by A21,Def6;
hence thesis by A18,XBOOLE_0:def 3;
end;
the ToleranceRel of S = Union pcs-ToleranceRels f
proof
thus the ToleranceRel of S c= Union pcs-ToleranceRels f
proof
let x be object;
assume x in the ToleranceRel of S;
then
A22: x in the ToleranceRel of P or x in the ToleranceRel of Q
by XBOOLE_0:def 3;
A23: (pcs-ToleranceRels f).z = the ToleranceRel of f.z by Def20;
A24: (pcs-ToleranceRels f).j = the ToleranceRel of f.j by Def20;
A25: the ToleranceRel of P in rng pcs-ToleranceRels f by A3,A23,FUNCT_1:3;
the ToleranceRel of Q in rng pcs-ToleranceRels f by A3,A24,FUNCT_1:3;
hence thesis by A22,A25,TARSKI:def 4;
end;
let x be object;
assume x in Union pcs-ToleranceRels f;
then consider Z being set such that
A26: x in Z and
A27: Z in rng pcs-ToleranceRels f by TARSKI:def 4;
consider i being object such that
A28: i in dom pcs-ToleranceRels f and
A29: (pcs-ToleranceRels f).i = Z by A27,FUNCT_1:def 3;
i = 0 or i = 1 by A28,TARSKI:def 2;
then Z = the ToleranceRel of f.z or
Z = the ToleranceRel of f.j by A29,Def20;
hence thesis by A26,XBOOLE_0:def 3;
end;
hence thesis by A4,A13,Def36;
end;
theorem Th15:
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
let P, Q be pcs-Str;
A1: the carrier of pcs-sum(P,Q) = (the carrier of P) \/ the carrier of Q by
Th14;
the InternalRel of pcs-sum(P,Q) = (the InternalRel of P) \/ the
InternalRel of Q by Th14;
hence thesis by A1,Th14;
end;
theorem
for P, Q being pcs-Str, 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
let P, Q be pcs-Str;
set R = pcs-sum(P,Q);
let p, q be Element of R;
A1: the InternalRel of R =
(the InternalRel of P) \/ the InternalRel of Q by Th14;
thus p <= q implies
(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
assume
A2: [p,q] in the InternalRel of R;
per cases by A1,A2,XBOOLE_0:def 3;
suppose
A3: [p,q] in the InternalRel of P;
then reconsider p9 = p, q9 = q as Element of P by ZFMISC_1:87;
p9 <= q9 by A3;
hence thesis;
end;
suppose
A4: [p,q] in the InternalRel of Q;
then reconsider p9 = p, q9 = q as Element of Q by ZFMISC_1:87;
p9 <= q9 by A4;
hence thesis;
end;
end;
assume
A5: (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;
per cases by A5;
suppose ex p9, q9 being Element of P st p9 = p & q9 = q & p9 <= q9;
then consider p9, q9 being Element of P such that
A6: p9 = p and
A7: q9 = q and
A8: p9 <= q9;
[p9,q9] in the InternalRel of P by A8;
hence [p,q] in the InternalRel of R by A1,A6,A7,XBOOLE_0:def 3;
end;
suppose ex p9, q9 being Element of Q st p9 = p & q9 = q & p9 <= q9;
then consider p9, q9 being Element of Q such that
A9: p9 = p and
A10: q9 = q and
A11: p9 <= q9;
[p9,q9] in the InternalRel of Q by A11;
hence [p,q] in the InternalRel of R by A1,A9,A10,XBOOLE_0:def 3;
end;
end;
theorem
for P, Q being pcs-Str, 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
let P, Q be pcs-Str;
set R = pcs-sum(P,Q);
let p, q be Element of R;
A1: the ToleranceRel of R =
(the ToleranceRel of P) \/ the ToleranceRel of Q by Th14;
thus p (--) q implies
(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
assume
A2: [p,q] in the ToleranceRel of R;
per cases by A1,A2,XBOOLE_0:def 3;
suppose
A3: [p,q] in the ToleranceRel of P;
then reconsider p9 = p, q9 = q as Element of P by ZFMISC_1:87;
p9 (--) q9 by A3;
hence thesis;
end;
suppose
A4: [p,q] in the ToleranceRel of Q;
then reconsider p9 = p, q9 = q as Element of Q by ZFMISC_1:87;
p9 (--) q9 by A4;
hence thesis;
end;
end;
assume
A5: (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;
per cases by A5;
suppose ex p9, q9 being Element of P st p9 = p & q9 = q & p9 (--) q9;
then consider p9, q9 being Element of P such that
A6: p9 = p and
A7: q9 = q and
A8: p9 (--) q9;
[p9,q9] in the ToleranceRel of P by A8;
hence [p,q] in the ToleranceRel of R by A1,A6,A7,XBOOLE_0:def 3;
end;
suppose ex p9, q9 being Element of Q st p9 = p & q9 = q & p9 (--) q9;
then consider p9, q9 being Element of Q such that
A9: p9 = p and
A10: q9 = q and
A11: p9 (--) q9;
[p9,q9] in the ToleranceRel of Q by A11;
hence [p,q] in the ToleranceRel of R by A1,A9,A10,XBOOLE_0:def 3;
end;
end;
registration
let P, Q be reflexive pcs-Str;
cluster pcs-sum(P,Q) -> reflexive;
coherence;
end;
registration
let P, Q be pcs-tol-reflexive pcs-Str;
cluster pcs-sum(P,Q) -> pcs-tol-reflexive;
coherence;
end;
registration
let P, Q be pcs-tol-symmetric pcs-Str;
cluster pcs-sum(P,Q) -> pcs-tol-symmetric;
coherence;
end;
theorem Th18:
for P, Q being pcs holds
P misses Q implies the InternalRel of pcs-sum(P,Q) is transitive
proof
let P, Q be pcs;
assume
A1: the carrier of P misses the carrier of Q;
pcs-sum(P,Q) = pcsSUM(P,Q) by Th15;
hence thesis by A1,Th1;
end;
theorem Th19:
for P, Q being pcs holds P misses Q implies pcs-sum(P,Q) is pcs-compatible
proof
let P, Q be pcs;
set D1 = the carrier of P;
set D2 = the carrier of Q;
set R1 = the InternalRel of P;
set R2 = the InternalRel of Q;
set T1 = the ToleranceRel of P;
set T2 = the ToleranceRel of Q;
set R = R1 \/ R2;
set T = T1 \/ T2;
assume
A1: D1 misses D2;
let p, p9, q, q9 be Element of pcs-sum(P,Q) such that
A2: p (--) q and
A3: p9 <= p and
A4: q9 <= q;
A5: pcs-sum(P,Q) = pcsSUM(P,Q) by Th15;
then
A6: [p,q] in T by A2;
per cases by A6,XBOOLE_0:def 3;
suppose
A7: [p,q] in T1;
then
A8: p in D1 by ZFMISC_1:87;
A9: q in D1 by A7,ZFMISC_1:87;
reconsider p1 = p, q1 = q as Element of P by A7,ZFMISC_1:87;
A10: p1 (--) q1 by A7;
A11: [p9,p] in R by A3,A5;
A12: [q9,q] in R by A4,A5;
then reconsider p91 = p9, q91 = q9 as Element of P by A1,A8,A9,A11,Lm1;
A13: [p9,p] in R1 by A1,A8,A11,Lm1;
A14: [q9,q] in R1 by A1,A9,A12,Lm1;
A15: p91 <= p1 by A13;
q91 <= q1 by A14;
then p91 (--) q91 by A10,A15,Def22;
then [p91,q91] in T1;
then [p91,q91] in T by XBOOLE_0:def 3;
hence p9 (--) q9 by A5;
end;
suppose
A16: [p,q] in T2;
then
A17: p in D2 by ZFMISC_1:87;
A18: q in D2 by A16,ZFMISC_1:87;
reconsider p1 = p, q1 = q as Element of Q by A16,ZFMISC_1:87;
A19: p1 (--) q1 by A16;
A20: [p9,p] in R by A3,A5;
A21: [q9,q] in R by A4,A5;
then reconsider p91 = p9, q91 = q9 as Element of Q by A1,A17,A18,A20,Lm1;
A22: [p9,p] in R2 by A1,A17,A20,Lm1;
A23: [q9,q] in R2 by A1,A18,A21,Lm1;
A24: p91 <= p1 by A22;
q91 <= q1 by A23;
then p91 (--) q91 by A19,A24,Def22;
then [p91,q91] in T2;
then [p91,q91] in T by XBOOLE_0:def 3;
hence p9 (--) q9 by A5;
end;
end;
theorem
for P, Q being pcs holds P misses Q implies pcs-sum(P,Q) is pcs
proof
let P, Q be pcs;
assume
A1: P misses Q;
set R = pcs-sum(P,Q);
A2: field the InternalRel of R = the carrier of R by ORDERS_1:12;
the InternalRel of R is transitive by A1,Th18;
then the InternalRel of R is_transitive_in the carrier of R
by A2;
then
A3: R is transitive;
R is pcs-compatible by A1,Th19;
hence thesis by A3;
end;
:: Extension
definition
let P be pcs-Str, a be set;
func pcs-extension(P,a) -> strict pcs-Str means
:Def39:
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
proof
set D = {a} \/ the carrier of P;
set IR = [:{a},D:] \/ the InternalRel of P;
set TR = [:D,{a}:] \/ [:{a},D:] \/ the ToleranceRel of P;
A1: {a} c= D by XBOOLE_1:7;
then
A2: [:{a},D:] c= [:D,D:] by ZFMISC_1:95;
the carrier of P c= D by XBOOLE_1:7;
then
A3: [:the carrier of P,the carrier of P:] c= [:D,D:] by ZFMISC_1:96;
then the InternalRel of P c= [:D,D:];
then reconsider IR as Relation of D by A2,XBOOLE_1:8;
[:D,{a}:] c= [:D,D:] by A1,ZFMISC_1:95;
then
A4: [:D,{a}:] \/ [:{a},D:] c= [:D,D:] by A2,XBOOLE_1:8;
the ToleranceRel of P c= [:D,D:] by A3;
then reconsider TR as Relation of D by A4,XBOOLE_1:8;
take pcs-Str(#D,IR,TR#);
thus thesis;
end;
uniqueness;
end;
registration
let P be pcs-Str, a be set;
cluster pcs-extension(P,a) -> non empty;
coherence
proof
the carrier of pcs-extension(P,a) = {a} \/ the carrier of P by Def39;
hence the carrier of pcs-extension(P,a) is non empty;
end;
end;
theorem Th21:
for P being pcs-Str, 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
let P be pcs-Str, a be set;
set R = pcs-extension(P,a);
A1: the carrier of R = {a} \/ the carrier of P by Def39;
A2: the InternalRel of R = [:{a},the carrier of R:] \/ the InternalRel of P
by Def39;
the ToleranceRel of R = [:{a},the carrier of R:] \/ [:the carrier of R,{
a}:] \/ the ToleranceRel of P by Def39;
hence thesis by A1,A2,XBOOLE_1:7;
end;
theorem
for P being pcs-Str, a being set,
p, q being Element of pcs-extension(P,a) st p = a holds p <= q
proof
let P be pcs-Str, a be set;
set R = pcs-extension(P,a);
let p, q be Element of R such that
A1: p = a;
A2: the InternalRel of R =
[:{a},the carrier of R:] \/ the InternalRel of P by Def39;
[a,q] in [:{a},the carrier of R:] by ZFMISC_1:105;
hence [p,q] in the InternalRel of R by A1,A2,XBOOLE_0:def 3;
end;
theorem Th23:
for P being pcs-Str, a being set, p, q being Element of P,
p1, q1 being Element of pcs-extension(P,a) st p = p1 & q = q1 &
p <= q holds p1 <= q1
proof
let P be pcs-Str, a be set, p, q be Element of P,
p1, q1 be Element of pcs-extension(P,a) such that
A1: p = p1 and
A2: q = q1 and
A3: [p,q] in the InternalRel of P;
the InternalRel of P c= the InternalRel of pcs-extension(P,a) by Th21;
hence [p1,q1] in the InternalRel of pcs-extension(P,a) by A1,A2,A3;
end;
theorem Th24:
for P being pcs-Str, a being set, p being Element of P,
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
let P be pcs-Str, a be set, p be Element of P,
p1, q1 be Element of pcs-extension(P,a) such that
A1: p = p1 and
A2: p <> a and
A3: p1 <= q1 and
A4: not a in the carrier of P;
set R = pcs-extension(P,a);
A5: the InternalRel of R = [:{a},the carrier of R:] \/ the InternalRel of P
by Def39;
[p1,q1] in the InternalRel of R by A3;
then [p1,q1] in [:{a},the carrier of R:] or [p1,q1] in the InternalRel of P
by A5,XBOOLE_0:def 3;
hence thesis by A1,A2,A4,ZFMISC_1:87,105;
end;
theorem Th25:
for P being pcs-Str, a being set,
p being Element of pcs-extension(P,a) st p <> a holds p in the carrier of P
proof
let P be pcs-Str, a be set, p be Element of pcs-extension(P,a) such that
A1: p <> a;
the carrier of pcs-extension(P,a) = {a} \/ the carrier of P by Def39;
then p in {a} or p in the carrier of P by XBOOLE_0:def 3;
hence thesis by A1,TARSKI:def 1;
end;
theorem Th26:
for P being pcs-Str, a being set, p, q being Element of P,
p1, q1 being Element of pcs-extension(P,a) st p = p1 & q = q1 &
p <> a & p1 <= q1 holds p <= q
proof
let P be pcs-Str, a be set, p, q be Element of P,
p1, q1 be Element of pcs-extension(P,a) such that
A1: p = p1 and
A2: q = q1 and
A3: p <> a and
A4: p1 <= q1;
set R = pcs-extension(P,a);
A5: the InternalRel of R = [:{a},the carrier of R:] \/ the InternalRel of P
by Def39;
[p1,q1] in the InternalRel of R by A4;
then [p1,q1] in [:{a},the carrier of R:] or [p1,q1] in the InternalRel of P
by A5,XBOOLE_0:def 3;
hence [p,q] in the InternalRel of P by A1,A2,A3,ZFMISC_1:105;
end;
theorem Th27:
for P being pcs-Str, a being set,
p, q being Element of pcs-extension(P,a) st p = a holds p (--) q & q (--) p
proof
let P be pcs-Str, a be set;
set R = pcs-extension(P,a);
let p, q be Element of R such that
A1: p = a;
the ToleranceRel of R = [:{a},the carrier of R:] \/
[:the carrier of R,{a}:] \/ the ToleranceRel of P by Def39;
then
A2: the ToleranceRel of R = [:{a},the carrier of R:] \/
([:the carrier of R,{a}:] \/ the ToleranceRel of P) by XBOOLE_1:4;
A3: [a,q] in [:{a},the carrier of R:] by ZFMISC_1:105;
[q,a] in [:the carrier of R,{a}:] by ZFMISC_1:106;
then [q,a] in [:the carrier of R,{a}:] \/ the ToleranceRel of P
by XBOOLE_0:def 3;
hence [p,q] in the ToleranceRel of R & [q,p] in the ToleranceRel of R
by A1,A2,A3,XBOOLE_0:def 3;
end;
theorem Th28:
for P being pcs-Str, a being set, p, q being Element of P,
p1, q1 being Element of pcs-extension(P,a) st p = p1 & q = q1 &
p (--) q holds p1 (--) q1
proof
let P be pcs-Str, a be set, p, q be Element of P,
p1, q1 be Element of pcs-extension(P,a) such that
A1: p = p1 and
A2: q = q1 and
A3: [p,q] in the ToleranceRel of P;
the ToleranceRel of P c= the ToleranceRel of pcs-extension(P,a) by Th21;
hence [p1,q1] in the ToleranceRel of pcs-extension(P,a) by A1,A2,A3;
end;
theorem Th29:
for P being pcs-Str, a being set, p, q being Element of P,
p1, q1 being Element of pcs-extension(P,a) st p = p1 & q = q1 &
p <> a & q <> a & p1 (--) q1 holds p (--) q
proof
let P be pcs-Str, a be set, p, q be Element of P,
p1, q1 be Element of pcs-extension(P,a) such that
A1: p = p1 and
A2: q = q1 and
A3: p <> a and
A4: q <> a and
A5: p1 (--) q1;
set R = pcs-extension(P,a);
A6: the ToleranceRel of R = [:{a},the carrier of R:] \/
[:the carrier of R,{a}:] \/ the ToleranceRel of P by Def39;
[p1,q1] in the ToleranceRel of R by A5;
then [p1,q1] in [:{a},the carrier of R:] \/ [:the carrier of R,{a}:] or
[p1,q1] in the ToleranceRel of P by A6,XBOOLE_0:def 3;
then [p1,q1] in [:{a},the carrier of R:] or
[p1,q1] in [:the carrier of R,{a}:] or
[p1,q1] in the ToleranceRel of P by XBOOLE_0:def 3;
hence [p,q] in the ToleranceRel of P by A1,A2,A3,A4,ZFMISC_1:105,106;
end;
registration
let P be reflexive pcs-Str, a be set;
cluster pcs-extension(P,a) -> reflexive;
coherence
proof
set R = pcs-extension(P,a);
A1: the carrier of R = {a} \/ the carrier of P by Def39;
A2: the InternalRel of R = [:{a},the carrier of R:] \/ the InternalRel of P
by Def39;
let p be object;
assume
A3: p in the carrier of R;
per cases by A1,A3,XBOOLE_0:def 3;
suppose p in {a};
then p = a by TARSKI:def 1;
then [p,p] in [:{a},the carrier of R:] by A3,ZFMISC_1:105;
hence thesis by A2,XBOOLE_0:def 3;
end;
suppose
A4: p in the carrier of P;
the InternalRel of P is_reflexive_in the carrier of P by ORDERS_2:def 2;
then [p,p] in the InternalRel of P by A4;
hence thesis by A2,XBOOLE_0:def 3;
end;
end;
end;
theorem Th30:
for P being transitive pcs-Str, a being set st not a in the carrier of P
holds pcs-extension(P,a) is transitive
proof
let P be transitive pcs-Str, a be set such that
A1: not a in the carrier of P;
set R = pcs-extension(P,a);
A2: the InternalRel of R = [:{a},the carrier of R:] \/ the InternalRel of P
by Def39;
let x, y, z be object;
assume that
A3: x in the carrier of R and
A4: y in the carrier of R and
A5: z in the carrier of R and
A6: [x,y] in the InternalRel of R and
A7: [y,z] in the InternalRel of R;
A8: [a,z] in [:{a},the carrier of R:] by A5,ZFMISC_1:105;
reconsider x, y, z as Element of R by A3,A4,A5;
A9: x <= y by A6;
A10: y <= z by A7;
per cases;
suppose x = a;
hence thesis by A2,A8,XBOOLE_0:def 3;
end;
suppose
A11: x <> a;
then reconsider x0 = x as Element of P by Th25;
A12: x0 <> a by A11;
then reconsider y0 = y as Element of P by A1,A9,Th24;
y0 <> a by A1,A9,A12,Th24;
then reconsider z0 = z as Element of P by A1,A10,Th24;
A13: y <> a by A1,A9,A12,Th24;
A14: x0 <= y0 by A9,A11,Th26;
y0 <= z0 by A10,A13,Th26;
then x0 <= z0 by A14,YELLOW_0:def 2;
then x <= z by Th23;
hence thesis;
end;
end;
registration
let P be pcs-tol-reflexive pcs-Str, a be set;
cluster pcs-extension(P,a) -> pcs-tol-reflexive;
coherence
proof
set R = pcs-extension(P,a);
A1: the carrier of R = {a} \/ the carrier of P by Def39;
A2: the ToleranceRel of R = [:{a},the carrier of R:] \/
[:the carrier of R,{a}:] \/ the ToleranceRel of P by Def39;
then
A3: the ToleranceRel of R = [:{a},the carrier of R:] \/
([:the carrier of R,{a}:] \/ the ToleranceRel of P) by XBOOLE_1:4;
let p be object;
assume
A4: p in the carrier of R;
per cases by A1,A4,XBOOLE_0:def 3;
suppose p in {a};
then p = a by TARSKI:def 1;
then [p,p] in [:{a},the carrier of R:] by A4,ZFMISC_1:105;
hence thesis by A3,XBOOLE_0:def 3;
end;
suppose
A5: p in the carrier of P;
the ToleranceRel of P is_reflexive_in the carrier of P by Def9;
then [p,p] in the ToleranceRel of P by A5;
hence thesis by A2,XBOOLE_0:def 3;
end;
end;
end;
registration
let P be pcs-tol-symmetric pcs-Str, a be set;
cluster pcs-extension(P,a) -> pcs-tol-symmetric;
coherence
proof
set R = pcs-extension(P,a);
A1: the ToleranceRel of R = [:{a},the carrier of R:] \/
[:the carrier of R,{a}:] \/ the ToleranceRel of P by Def39;
let p, q be object;
assume that p in the carrier of R and q in the carrier of R and
A2: [p,q] in the ToleranceRel of R;
A3: the ToleranceRel of P is_symmetric_in the carrier of P by Def11;
per cases by A1,A2,XBOOLE_0:def 3;
suppose
A4: [p,q] in [:{a},the carrier of R:] \/ [:the carrier of R,{a}:];
per cases by A4,XBOOLE_0:def 3;
suppose
A5: [p,q] in [:{a},the carrier of R:];
then
A6: p = a by ZFMISC_1:105;
q in the carrier of R by A5,ZFMISC_1:105;
then [q,p] in [:the carrier of R,{a}:] by A6,ZFMISC_1:106;
then [q,p] in [:{a},the carrier of R:] \/ [:the carrier of R,{a}:]
by XBOOLE_0:def 3;
hence thesis by A1,XBOOLE_0:def 3;
end;
suppose
A7: [p,q] in [:the carrier of R,{a}:];
then
A8: q = a by ZFMISC_1:106;
p in the carrier of R by A7,ZFMISC_1:106;
then [q,p] in [:{a},the carrier of R:] by A8,ZFMISC_1:105;
then [q,p] in [:{a},the carrier of R:] \/ [:the carrier of R,{a}:]
by XBOOLE_0:def 3;
hence thesis by A1,XBOOLE_0:def 3;
end;
end;
suppose
A9: [p,q] in the ToleranceRel of P;
then
A10: p in the carrier of P by ZFMISC_1:87;
q in the carrier of P by A9,ZFMISC_1:87;
then [q,p] in the ToleranceRel of P by A3,A9,A10;
hence thesis by A1,XBOOLE_0:def 3;
end;
end;
end;
theorem Th31:
for P being pcs-compatible pcs-Str, a being set st not a in the carrier of P
holds pcs-extension(P,a) is pcs-compatible
proof
let P be pcs-compatible pcs-Str, a be set such that
A1: not a in the carrier of P;
set R = pcs-extension(P,a);
let p, p9, q, q9 be Element of R such that
A2: p (--) q and
A3: p9 <= p and
A4: q9 <= q;
per cases;
suppose p9 = a or q9 = a;
hence thesis by Th27;
end;
suppose that
A5: p9 <> a and
A6: q9 <> a;
reconsider p90 = p9, q90 = q9 as Element of P by A5,A6,Th25;
A7: p90 <> a by A5;
A8: q90 <> a by A6;
A9: p <> a by A1,A3,A7,Th24;
A10: q <> a by A1,A4,A8,Th24;
reconsider p0 = p, q0 = q as Element of P by A1,A3,A4,A7,A8,Th24;
A11: p0 (--) q0 by A2,A9,A10,Th29;
A12: p90 <= p0 by A3,A5,Th26;
q90 <= q0 by A4,A6,Th26;
then p90 (--) q90 by A11,A12,Def22;
hence thesis by Th28;
end;
end;
theorem
for P being pcs, a being set st not a in the carrier of P
holds pcs-extension(P,a) is pcs
proof
let P be pcs, a be set such that
A1: not a in the carrier of P;
set R = pcs-extension(P,a);
R is reflexive transitive pcs-tol-reflexive pcs-tol-symmetric
pcs-compatible by A1,Th30,Th31;
hence thesis;
end;
:: Reverse
definition
let P be pcs-Str;
func pcs-reverse(P) -> strict pcs-Str means
:Def40:
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
proof
reconsider TR = (the ToleranceRel of P)` as Relation of the carrier of P;
take pcs-Str(#the carrier of P,(the InternalRel of P)~,TR#);
thus thesis;
end;
uniqueness;
end;
registration
let P be non empty pcs-Str;
cluster pcs-reverse(P) -> non empty;
coherence
proof
the carrier of pcs-reverse(P) = the carrier of P by Def40;
hence the carrier of pcs-reverse(P) is non empty;
end;
end;
theorem Th33:
for P being pcs-Str, 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
let P be pcs-Str, p, q be Element of P;
set R = pcs-reverse(P);
let p9, q9 be Element of R such that
A1: p = p9 and
A2: q = q9;
A3: the InternalRel of R = (the InternalRel of P)~ by Def40;
thus p <= q implies q9 <= p9
by A1,A2,A3,RELAT_1:def 7;
assume [q9,p9] in the InternalRel of R;
hence [p,q] in the InternalRel of P by A1,A2,A3,RELAT_1:def 7;
end;
theorem Th34:
for P being pcs-Str, p, q being Element of P
for p9, q9 being Element of pcs-reverse(P) st p = p9 & q = q9 holds
p (--) q implies not p9 (--) q9
proof
let P be pcs-Str, p, q be Element of P;
set R = pcs-reverse(P);
let p9, q9 be Element of R such that
A1: p = p9 and
A2: q = q9;
A3: the ToleranceRel of R = (the ToleranceRel of P)` by Def40;
assume [p,q] in the ToleranceRel of P;
hence not [p9,q9] in the ToleranceRel of R by A1,A2,A3,XBOOLE_0:def 5;
end;
theorem Th35:
for P being non empty pcs-Str, p, q being Element of P
for p9, q9 being Element of pcs-reverse(P) st p = p9 & q = q9 holds
not p9 (--) q9 implies p (--) q
proof
let P be non empty pcs-Str, p, q be Element of P;
set R = pcs-reverse(P);
let p9, q9 be Element of R such that
A1: p = p9 and
A2: q = q9;
A3: the ToleranceRel of R = (the ToleranceRel of P)` by Def40;
assume
A4: not [p9,q9] in the ToleranceRel of R;
[p,q] in [:the carrier of P,the carrier of P:] by ZFMISC_1:87;
hence [p,q] in the ToleranceRel of P by A1,A2,A3,A4,XBOOLE_0:def 5;
end;
registration
let P be reflexive pcs-Str;
cluster pcs-reverse(P) -> reflexive;
coherence
proof
set R = pcs-reverse(P);
A1: the carrier of R = the carrier of P by Def40;
A2: the InternalRel of R = (the InternalRel of P)~ by Def40;
the InternalRel of P is_reflexive_in the carrier of P by ORDERS_2:def 2;
hence the InternalRel of R is_reflexive_in the carrier of R
by A1,A2,ORDERS_1:79;
end;
end;
registration
let P be transitive pcs-Str;
cluster pcs-reverse(P) -> transitive;
coherence
proof
set R = pcs-reverse(P);
A1: the carrier of R = the carrier of P by Def40;
A2: the InternalRel of R = (the InternalRel of P)~ by Def40;
the InternalRel of P is_transitive_in the carrier of P by ORDERS_2:def 3;
hence the InternalRel of R is_transitive_in the carrier of R
by A1,A2,ORDERS_1:80;
end;
end;
registration
let P be pcs-tol-reflexive pcs-Str;
cluster pcs-reverse(P) -> pcs-tol-irreflexive;
coherence
proof
set R = pcs-reverse(P);
A1: the carrier of R = the carrier of P by Def40;
A2: the ToleranceRel of R = (the ToleranceRel of P)` by Def40;
A3: the ToleranceRel of P is_reflexive_in the carrier of P by Def9;
let x be object;
assume x in the carrier of R;
then [x,x] in the ToleranceRel of P by A1,A3;
hence thesis by A2,XBOOLE_0:def 5;
end;
end;
registration
let P be pcs-tol-irreflexive pcs-Str;
cluster pcs-reverse(P) -> pcs-tol-reflexive;
coherence
proof
set R = pcs-reverse(P);
A1: the carrier of R = the carrier of P by Def40;
A2: the ToleranceRel of R = (the ToleranceRel of P)` by Def40;
A3: the ToleranceRel of P is_irreflexive_in the carrier of P by Def10;
let x be object;
assume
A4: x in the carrier of R;
then
A5: not [x,x] in the ToleranceRel of P by A1,A3;
[x,x] in [:the carrier of R,the carrier of R:] by A4,ZFMISC_1:87;
hence thesis by A1,A2,A5,XBOOLE_0:def 5;
end;
end;
registration
let P be pcs-tol-symmetric pcs-Str;
cluster pcs-reverse(P) -> pcs-tol-symmetric;
coherence
proof
set R = pcs-reverse(P);
A1: the carrier of R = the carrier of P by Def40;
A2: the ToleranceRel of R = (the ToleranceRel of P)` by Def40;
A3: the ToleranceRel of P is_symmetric_in the carrier of P by Def11;
let x, y be object;
assume that
A4: x in the carrier of R and
A5: y in the carrier of R;
assume [x,y] in the ToleranceRel of R;
then not [x,y] in the ToleranceRel of P by A2,XBOOLE_0:def 5;
then
A6: not [y,x] in the ToleranceRel of P by A1,A3,A4,A5;
[y,x] in [:the carrier of P,the carrier of P:] by A1,A4,A5,ZFMISC_1:87;
hence thesis by A2,A6,XBOOLE_0:def 5;
end;
end;
registration
let P be pcs-compatible pcs-Str;
cluster pcs-reverse(P) -> pcs-compatible;
coherence
proof
set R = pcs-reverse(P);
A1: the carrier of R = the carrier of P by Def40;
A2: the InternalRel of R = (the InternalRel of P)~ by Def40;
A3: the ToleranceRel of R = (the ToleranceRel of P)` by Def40;
let p, p9, q, q9 be Element of R such that
A4: [p,q] in the ToleranceRel of R and
A5: [p9,p] in the InternalRel of R and
A6: [q9,q] in the InternalRel of R;
A7: p9 in the carrier of R by A5,ZFMISC_1:87;
reconsider p90 = p9, q90 = q9, p0 = p, q0 = q as Element of P by Def40;
not [p0,q0] in the ToleranceRel of P by A3,A4,XBOOLE_0:def 5;
then
A8: not p0 (--) q0;
A9: [p0,p90] in the InternalRel of P by A2,A5,RELAT_1:def 7;
A10: [q0,q90] in the InternalRel of P by A2,A6,RELAT_1:def 7;
A11: p0 <= p90 by A9;
q0 <= q90 by A10;
then not p90 (--) q90 by A8,A11,Def22;
then
A12: not [p90,q90] in the ToleranceRel of P;
[p9,q9] in [:the carrier of P,the carrier of P:] by A1,A7,ZFMISC_1:87;
hence [p9,q9] in the ToleranceRel of R by A3,A12,XBOOLE_0:def 5;
end;
end;
:: Times
definition
let P, Q be pcs-Str;
func P pcs-times Q -> pcs-Str equals
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;
end;
registration
let P, Q be pcs-Str;
cluster P pcs-times Q -> strict;
coherence;
end;
registration
let P, Q be non empty pcs-Str;
cluster P pcs-times Q -> non empty;
coherence;
end;
theorem
for P, Q being pcs-Str, p, q being Element of P pcs-times Q
for p1, p2 being Element of P, q1, q2 being Element of Q st
p = [p1,q1] & q = [p2,q2] holds p <= q iff p1 <= p2 & q1 <= q2
proof
let P, Q be pcs-Str, p, q be Element of P pcs-times Q;
let p1, p2 be Element of P, q1, q2 be Element of Q such that
A1: p = [p1,q1] and
A2: q = [p2,q2];
thus p <= q implies p1 <= p2 & q1 <= q2
proof
assume p <= q;
then [p,q] in [" the InternalRel of P, the InternalRel of Q "];
then consider a, b, s, t being object such that
A3: p = [a,b] and
A4: q = [s,t] and
A5: [a,s] in the InternalRel of P and
A6: [b,t] in the InternalRel of Q by YELLOW_3:def 1;
A7: a = p1 by A1,A3,XTUPLE_0:1;
A8: b = q1 by A1,A3,XTUPLE_0:1;
thus [p1,p2] in the InternalRel of P by A2,A4,A5,A7,XTUPLE_0:1;
thus [q1,q2] in the InternalRel of Q by A2,A4,A6,A8,XTUPLE_0:1;
end;
assume that
A9: p1 <= p2 and
A10: q1 <= q2;
A11: [p1,p2] in the InternalRel of P by A9;
[q1,q2] in the InternalRel of Q by A10;
hence [p,q] in the InternalRel of P pcs-times Q by A1,A2,A11,YELLOW_3:def 1;
end;
theorem
for P, Q being pcs-Str, p, q being Element of P pcs-times Q
for p1, p2 being Element of P, q1, q2 being Element of Q st
p = [p1,q1] & q = [p2,q2] holds p (--) q implies p1 (--) p2 or q1 (--) q2
proof
let P, Q be pcs-Str, p, q be Element of P pcs-times Q;
let p1, p2 be Element of P, q1, q2 be Element of Q such that
A1: p = [p1,q1] and
A2: q = [p2,q2];
assume p (--) q;
then [p,q] in [^ the ToleranceRel of P, the ToleranceRel of Q ^];
then consider a, b, c, d being set such that
A3: p = [a,b] and
A4: q = [c,d] and a in the carrier of P
and b in the carrier of Q
and c in the carrier of P
and d in the carrier of Q and
A5: [a,c] in the ToleranceRel of P or [b,d] in the ToleranceRel of Q by Def2;
A6: a = p1 by A1,A3,XTUPLE_0:1;
A7: b = q1 by A1,A3,XTUPLE_0:1;
A8: c = p2 by A2,A4,XTUPLE_0:1;
d = q2 by A2,A4,XTUPLE_0:1;
hence thesis by A5,A6,A7,A8;
end;
theorem Th38:
for P, Q being non empty pcs-Str, p, q being Element of P pcs-times Q
for p1, p2 being Element of P, q1, q2 being Element of Q st
p = [p1,q1] & q = [p2,q2] holds p1 (--) p2 or q1 (--) q2 implies p (--) q
by Def2;
registration
let P, Q be reflexive pcs-Str;
cluster P pcs-times Q -> reflexive;
coherence
proof
the RelStr of P pcs-times Q = [:P,Q:] by YELLOW_3:def 2;
hence thesis by WAYBEL_8:12;
end;
end;
registration
let P, Q be transitive pcs-Str;
cluster P pcs-times Q -> transitive;
coherence
proof
the RelStr of P pcs-times Q = [:P,Q:] by YELLOW_3:def 2;
hence thesis by WAYBEL_8:13;
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
proof
the TolStr of P pcs-times Q = [^P,Q^];
hence thesis by Th3;
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
proof
the TolStr of P pcs-times Q = [^P,Q^];
hence thesis by Th3;
end;
end;
registration
let P, Q be pcs-tol-symmetric pcs-Str;
cluster P pcs-times Q -> pcs-tol-symmetric;
coherence
proof
the TolStr of P pcs-times Q = [^P,Q^];
hence thesis by Th5;
end;
end;
registration
let P, Q be pcs-compatible pcs-Str;
cluster P pcs-times Q -> pcs-compatible;
coherence
proof
set R = P pcs-times Q;
set TR = the ToleranceRel of R;
set D1 = the carrier of P;
set D2 = the carrier of Q;
let p, p9, q, q9 be Element of R such that
A1: p (--) q and
A2: p9 <= p and
A3: q9 <= q;
A4: [p,q] in TR by A1;
then consider a, b, c, d being set such that
A5: p = [a,b] and
A6: q = [c,d] and
A7: a in D1 and
A8: b in D2 and
A9: c in D1 and
A10: d in D2 and
[a,c] in the ToleranceRel of P or [b,d] in the ToleranceRel of Q by Def2;
A11: [p9,p] in the InternalRel of R by A2;
then p9 in the carrier of R by ZFMISC_1:87;
then consider e, f being object such that
A12: e in D1 and
A13: f in D2 and
A14: p9 = [e,f] by ZFMISC_1:def 2;
A15: [q9,q] in the InternalRel of R by A3;
then q9 in the carrier of R by ZFMISC_1:87;
then consider g, h being object such that
A16: g in D1 and
A17: h in D2 and
A18: q9 = [g,h] by ZFMISC_1:def 2;
reconsider P, Q as non empty pcs-compatible pcs-Str by A7,A8;
reconsider a, c, e, g as Element of P by A7,A9,A12,A16;
reconsider b, d, f, h as Element of Q by A8,A10,A13,A17;
[^a,b^] (--) [^c,d^] by A4,A5,A6;
then
A19: a (--) c or b (--) d by Th6;
A20: the RelStr of P pcs-times Q = [:P,Q:] by YELLOW_3:def 2;
then
A21: [e,f] <= [a,b] by A5,A11,A14;
then
A22: e <= a by YELLOW_3:11;
A23: f <= b by A21,YELLOW_3:11;
A24: [g,h] <= [c,d] by A6,A15,A18,A20;
then
A25: g <= c by YELLOW_3:11;
h <= d by A24,YELLOW_3:11;
then e (--) g or f (--) h by A19,A22,A23,A25,Def22;
then
A26: [e,g] in the ToleranceRel of P or [f,h] in the ToleranceRel of Q;
A27: p9 = [e,f] by A14;
q9 = [g,h] by A18;
hence [p9,q9] in TR by A26,A27,Def3;
end;
end;
definition
let P, Q be pcs-Str;
func P --> Q -> pcs-Str equals
(pcs-reverse P) pcs-times Q;
coherence;
end;
registration
let P, Q be pcs-Str;
cluster P --> Q -> strict;
coherence;
end;
registration
let P, Q be non empty pcs-Str;
cluster P --> Q -> non empty;
coherence;
end;
theorem
for P, Q being pcs-Str, p, q being Element of P --> Q
for p1, p2 being Element of P, q1, q2 being Element of Q st
p = [p1,q1] & q = [p2,q2] holds p <= q iff p2 <= p1 & q1 <= q2
proof
let P, Q be pcs-Str, p, q be Element of P --> Q;
let p1, p2 be Element of P, q1, q2 be Element of Q such that
A1: p = [p1,q1] and
A2: q = [p2,q2];
reconsider r1 = p1, r2 = p2 as Element of pcs-reverse P by Def40;
thus p <= q implies p2 <= p1 & q1 <= q2
proof
assume p <= q;
then [p,q] in ["the InternalRel of pcs-reverse P, the InternalRel of Q"];
then consider a, b, s, t being object such that
A3: p = [a,b] and
A4: q = [s,t] and
A5: [a,s] in the InternalRel of pcs-reverse P and
A6: [b,t] in the InternalRel of Q by YELLOW_3:def 1;
A7: a = p1 by A1,A3,XTUPLE_0:1;
A8: b = q1 by A1,A3,XTUPLE_0:1;
s = p2 by A2,A4,XTUPLE_0:1;
then r1 <= r2 by A5,A7;
hence p2 <= p1 by Th33;
thus [q1,q2] in the InternalRel of Q by A2,A4,A6,A8,XTUPLE_0:1;
end;
assume that
A9: p2 <= p1 and
A10: q1 <= q2;
r1 <= r2 by A9,Th33;
then
A11: [r1,r2] in the InternalRel of pcs-reverse P;
[q1,q2] in the InternalRel of Q by A10;
hence [p,q] in the InternalRel of P --> Q by A1,A2,A11,YELLOW_3:def 1;
end;
theorem
for P, Q being pcs-Str, p, q being Element of P --> Q
for p1, p2 being Element of P, q1, q2 being Element of Q st
p = [p1,q1] & q = [p2,q2] holds p (--) q implies not p1 (--) p2 or q1 (--) q2
proof
let P, Q be pcs-Str, p, q be Element of P --> Q;
let p1, p2 be Element of P, q1, q2 be Element of Q such that
A1: p = [p1,q1] and
A2: q = [p2,q2];
reconsider r1 = p1, r2 = p2 as Element of pcs-reverse P by Def40;
assume [p,q] in the ToleranceRel of P --> Q;
then consider a, b, s, t being set such that
A3: p = [a,b] and
A4: q = [s,t] and
a in the carrier of pcs-reverse P and b in the carrier of Q
and s in the carrier of pcs-reverse P
and t in the carrier of Q and
A5: [a,s] in the ToleranceRel of pcs-reverse P or
[b,t] in the ToleranceRel of Q by Def2;
A6: a = p1 by A1,A3,XTUPLE_0:1;
A7: b = q1 by A1,A3,XTUPLE_0:1;
A8: s = p2 by A2,A4,XTUPLE_0:1;
t = q2 by A2,A4,XTUPLE_0:1;
then r1 (--) r2 or q1 (--) q2 by A5,A6,A7,A8;
hence thesis by Th34;
end;
theorem
for P, Q being non empty pcs-Str, p, q being Element of P --> Q
for p1, p2 being Element of P, q1, q2 being Element of Q st
p = [p1,q1] & q = [p2,q2] holds not p1 (--) p2 or q1 (--) q2 implies p (--) q
proof
let P, Q be non empty pcs-Str, p, q be Element of P --> Q;
let p1, p2 be Element of P, q1, q2 be Element of Q such that
A1: p = [p1,q1] and
A2: q = [p2,q2];
reconsider r1 = p1, r2 = p2 as Element of pcs-reverse P by Def40;
reconsider w1 = [r1,q1], w2 = [r2,q2] as
Element of (pcs-reverse P) pcs-times Q by A1,A2;
assume not p1 (--) p2 or q1 (--) q2;
then r1 (--) r2 or q1 (--) q2 by Th35;
then w1 (--) w2 by Th38;
hence thesis by A1,A2;
end;
registration
let P, Q be reflexive pcs-Str;
cluster P --> Q -> reflexive;
coherence;
end;
registration
let P, Q be transitive pcs-Str;
cluster P --> Q -> transitive;
coherence;
end;
registration
let P be pcs-Str, Q be pcs-tol-reflexive pcs-Str;
cluster P --> Q -> pcs-tol-reflexive;
coherence;
end;
registration
let P be pcs-tol-irreflexive pcs-Str, Q be pcs-Str;
cluster P --> Q -> pcs-tol-reflexive;
coherence;
end;
registration
let P, Q be pcs-tol-symmetric pcs-Str;
cluster P --> Q -> pcs-tol-symmetric;
coherence;
end;
registration
let P, Q be pcs-compatible pcs-Str;
cluster P --> Q -> pcs-compatible;
coherence;
end;
registration
let P, Q be pcs;
cluster P --> Q -> pcs-like;
coherence;
end;
:: Self-coherence
definition
let P be TolStr, S be Subset of P;
attr S is pcs-self-coherent means
for x, y being Element of P st x in S & y in S holds x (--) y;
end;
registration
let P be TolStr;
cluster empty -> pcs-self-coherent for Subset of P;
coherence;
end;
definition
let P be TolStr, F be Subset-Family of P;
attr F is pcs-self-coherent-membered means
:Def44:
for S being Subset of P st S in F holds S is pcs-self-coherent;
end;
registration
let P be TolStr;
cluster non empty pcs-self-coherent-membered for Subset-Family of P;
existence
proof
reconsider F = {{}} as Subset-Family of P by SETFAM_1:46;
take F;
thus F is non empty;
let S be Subset of P;
assume S in F;
then S = {}P by TARSKI:def 1;
hence thesis;
end;
end;
definition
let P be RelStr, D be set;
defpred P[set,set] means $1 in D & $2 in D &
for a being set st a in $1 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:
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 ex b being set st b in B &
[a,b] in the InternalRel of P;
existence
proof
consider R being Relation of D such that
A1: for x, y being set holds [x,y] in R iff x in D & y in D & P[x,y]
from RELSET_1:sch 5;
take R;
thus thesis by A1;
end;
uniqueness
proof
let R1, R2 be Relation of D such that
A2: for A, B being set holds [A,B] in R1 iff A in D & B in D &
for a being set st a in A ex b being set st b in B &
[a,b] in the InternalRel of P and
A3: for A, B being set holds [A,B] in R2 iff A in D & B in D &
for a being set st a in A ex b being set st b in B &
[a,b] in the InternalRel of P;
let x,y be object;
reconsider a=x, b=y as set by TARSKI:1;
A4: [a,b] in R1 iff P[a,b] by A2;
[a,b] in R2 iff P[a,b] by A3;
hence [x,y] in R1 iff [x,y] in R2 by A4;
end;
end;
definition
let P be TolStr, D be set;
defpred Q[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:
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
proof
consider R being Relation of D such that
A1: for x, y being set holds [x,y] in R iff x in D & y in D & Q[x,y]
from RELSET_1:sch 5;
take R;
thus thesis by A1;
end;
uniqueness
proof
let R1, R2 be Relation of D such that
A2: for A, B being set holds [A,B] in R1 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
and
A3: for A, B being set holds [A,B] in R2 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;
let x,y be object;
reconsider a=x, b=y as set by TARSKI:1;
A4: [a,b] in R1 iff Q[a,b] by A2;
[a,b] in R2 iff Q[a,b] by A3;
hence [x,y] in R1 iff [x,y] in R2 by A4;
end;
end;
theorem
for P being RelStr, 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 ex b being Element of P st b in B & a <= b
proof
let P be RelStr, D be Subset-Family of P;
let A, B be set;
thus [A,B] in pcs-general-power-IR(P,D) implies A in D & B in D &
for a being Element of P st a in A ex b being Element of P st b in B &
a <= b
proof
assume
A1: [A,B] in pcs-general-power-IR(P,D);
hence
A2: A in D & B in D by Def45;
let a be Element of P;
assume a in A;
then consider b being set such that
A3: b in B and
A4: [a,b] in the InternalRel of P by A1,Def45;
reconsider b as Element of P by A2,A3;
take b;
thus thesis by A3,A4;
end;
assume that
A5: A in D and
A6: B in D and
A7: for a being Element of P st a in A ex b being Element of P st b in B &
a <= b;
for a being set st a in A ex b being set st b in B &
[a,b] in the InternalRel of P
proof
let a be set;
assume
A8: a in A;
then reconsider a as Element of P by A5;
consider b being Element of P such that
A9: b in B and
A10: a <= b by A7,A8;
take b;
thus thesis by A9,A10;
end;
hence thesis by A5,A6,Def45;
end;
theorem
for P being TolStr, 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
let P be TolStr, D be Subset-Family of P;
let A, B be set;
thus [A,B] in pcs-general-power-TR(P,D) implies A in D & B in D &
for a, b being Element of P st a in A & b in B holds a (--) b
by Def46;
assume that
A1: A in D and
A2: B in D and
A3: for a, b being Element of P st a in A & b in B holds a (--) b;
for a, b being set st a in A & b in B holds [a,b] in the ToleranceRel of P
by A1,A2,A3,Def7;
hence thesis by A1,A2,Def46;
end;
definition
let P be pcs-Str, D be set;
func pcs-general-power(P,D) -> pcs-Str equals
pcs-Str (# D, pcs-general-power-IR(P,D), pcs-general-power-TR(P,D) #);
coherence;
end;
notation
let P be pcs-Str, D be Subset-Family of P;
synonym pcs-general-power(D) for pcs-general-power(P,D);
end;
registration
let P be pcs-Str, D be non empty set;
cluster pcs-general-power(P,D) -> non empty;
coherence;
end;
theorem Th44:
for P being pcs-Str, D be set
for p, q being Element of pcs-general-power(P,D) holds p <= q
implies for p9 being Element of P st p9 in p
ex q9 being Element of P st q9 in q & p9 <= q9
proof
let P be pcs-Str, D be set;
set R = pcs-general-power(P,D);
let p, q be Element of R;
assume
A1: [p,q] in the InternalRel of R;
let p9 be Element of P;
assume p9 in p;
then consider b being set such that
A2: b in q and
A3: [p9,b] in the InternalRel of P by A1,Def45;
reconsider b as Element of P by A3,ZFMISC_1:87;
take b;
thus b in q & [p9,b] in the InternalRel of P by A2,A3;
end;
theorem
for P being pcs-Str, 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
ex q9 being Element of P st q9 in q & p9 <= q9 holds p <= q
proof
let P be pcs-Str, D be non empty Subset-Family of P;
set R = pcs-general-power(D);
let p, q be Element of R;
assume
A1: for p9 being Element of P st p9 in p
ex q9 being Element of P st q9 in q & p9 <= q9;
A2: p in D;
for a being set st a in p ex b being set st b in q &
[a,b] in the InternalRel of P
proof
let a be set;
assume
A3: a in p;
then reconsider a as Element of P by A2;
consider q9 being Element of P such that
A4: q9 in q and
A5: a <= q9 by A1,A3;
take q9;
thus thesis by A4,A5;
end;
hence [p,q] in the InternalRel of R by Def45;
end;
theorem Th46:
for P being pcs-Str, D being set
for p, q being Element of pcs-general-power(P,D) holds p (--) q implies
for p9, q9 being Element of P st p9 in p & q9 in q holds p9 (--) q9
by Def46;
theorem
for P being pcs-Str, 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
let P be pcs-Str, D be non empty Subset-Family of P;
set R = pcs-general-power(D);
let p, q be Element of R;
assume
A1: for p9, q9 being Element of P st p9 in p & q9 in q holds p9 (--) q9;
A2: p in D;
A3: q in D;
for a,b being set st a in p & b in q
holds [a,b] in the ToleranceRel of P by A1,A2,A3,Def7;
hence [p,q] in the ToleranceRel of R by Def46;
end;
registration
let P be pcs-Str, D be set;
cluster pcs-general-power(P,D) -> strict;
coherence;
end;
registration
let P be reflexive pcs-Str, D be Subset-Family of P;
cluster pcs-general-power(D) -> reflexive;
coherence
proof
set R = pcs-general-power(D);
let x be object;
assume
A1: x in the carrier of R;
reconsider x as set by TARSKI:1;
for a being set st a in x ex b being set st b in x &
[a,b] in the InternalRel of P
proof
let a be set such that
A2: a in x;
take a;
thus a in x by A2;
field the InternalRel of P = the carrier of P by ORDERS_1:12;
then the InternalRel of P is_reflexive_in the carrier of P by
RELAT_2:def 9;
hence thesis by A1,A2;
end;
hence thesis by A1,Def45;
end;
end;
registration
let P be transitive pcs-Str, D be set;
cluster pcs-general-power(P,D) -> transitive;
coherence
proof
set R = pcs-general-power(P,D);
set IR = the InternalRel of R;
let x, y, z be object;
assume that
A1: x in the carrier of R and y in the carrier of R and
A2: z in the carrier of R and
A3: [x,y] in IR and
A4: [y,z] in IR;
reconsider x,y,z as set by TARSKI:1;
for a being set st a in x ex b being set st b in z &
[a,b] in the InternalRel of P
proof
let a be set;
assume a in x;
then consider b being set such that
A5: b in y and
A6: [a,b] in the InternalRel of P by A3,Def45;
consider c being set such that
A7: c in z and
A8: [b,c] in the InternalRel of P by A4,A5,Def45;
take c;
thus c in z by A7;
A9: the
InternalRel of P is_transitive_in the carrier of P by ORDERS_2:def 3;
A10: a in the carrier of P by A6,ZFMISC_1:87;
A11: b in the carrier of P by A6,ZFMISC_1:87;
c in the carrier of P by A8,ZFMISC_1:87;
hence thesis by A6,A8,A9,A10,A11;
end;
hence thesis by A1,A2,Def45;
end;
end;
registration
let P be pcs-tol-reflexive pcs-Str,
D be pcs-self-coherent-membered Subset-Family of P;
cluster pcs-general-power(D) -> pcs-tol-reflexive;
coherence
proof
let x be object;
assume
A1: x in the carrier of pcs-general-power(D);
then reconsider x as Subset of P;
A2: x is pcs-self-coherent by A1,Def44;
for a,b being set st a in x & b in x
holds [a,b] in the ToleranceRel of P by A2,Def7;
hence thesis by A1,Def46;
end;
end;
registration
let P be pcs-tol-symmetric pcs-Str, D be Subset-Family of P;
cluster pcs-general-power(D) -> pcs-tol-symmetric;
coherence
proof
set R = pcs-general-power(D);
let x, y be object;
assume
A1: x in the carrier of R;
assume
A2: y in the carrier of R;
assume
A3: [x,y] in the ToleranceRel of R;
reconsider x,y as set by TARSKI:1;
now
let a, b be set such that
A4: a in y and
A5: b in x;
reconsider a1 = a, b1 = b as Element of P by A1,A2,A4,A5;
[b,a] in the ToleranceRel of P by A3,A4,A5,Def46;
then b1 (--) a1;
hence [a,b] in the ToleranceRel of P by Def7;
end;
hence thesis by A1,A2,Def46;
end;
end;
registration
let P be pcs-compatible pcs-Str, D be Subset-Family of P;
cluster pcs-general-power(D) -> pcs-compatible;
coherence
proof
set R = pcs-general-power(D);
let p, p9, q, q9 being Element of R such that
A1: p (--) q and
A2: p9 <= p and
A3: q9 <= q;
A4: [p9,p] in the InternalRel of R by A2;
A5: [q9,q] in the InternalRel of R by A3;
A6: p9 in the carrier of R by A4,ZFMISC_1:87;
A7: q9 in the carrier of R by A5,ZFMISC_1:87;
now
let a, b be set such that
A8: a in p9 and
A9: b in q9;
reconsider a1 = a, b1 = b as Element of P by A6,A7,A8,A9;
consider p1 being Element of P such that
A10: p1 in p and
A11: a1 <= p1 by A2,A8,Th44;
consider q1 being Element of P such that
A12: q1 in q and
A13: b1 <= q1 by A3,A9,Th44;
p1 (--) q1 by A1,A10,A12,Th46;
then a1 (--) b1 by A11,A13,Def22;
hence [a,b] in the ToleranceRel of P;
end;
hence [p9,q9] in the ToleranceRel of R by A6,Def46;
end;
end;
definition
let P be pcs-Str;
func pcs-coherent-power(P) -> set equals
{X where X is Subset of P: X is pcs-self-coherent};
coherence;
end;
registration
let P be pcs-Str;
cluster pcs-self-coherent for Subset of P;
existence
proof
take {}P;
thus thesis;
end;
end;
theorem Th48:
for P being pcs-Str, X being set holds X in pcs-coherent-power(P)
implies X is pcs-self-coherent Subset of P
proof
let P be pcs-Str, X be set;
assume X in pcs-coherent-power(P);
then ex Y being Subset of P st X = Y & Y is pcs-self-coherent;
hence thesis;
end;
registration
let P be pcs-Str;
cluster pcs-coherent-power(P) -> non empty;
coherence
proof
{}P in pcs-coherent-power(P);
hence thesis;
end;
end;
definition
let P be pcs-Str;
redefine func pcs-coherent-power(P) -> Subset-Family of P; :: redefines pcs-coherent-power (PCS_0, definition)
coherence
proof
pcs-coherent-power(P) c= bool the carrier of P
proof
let X be object;
assume X in pcs-coherent-power(P);
then X is Subset of P by Th48;
hence thesis;
end;
hence thesis;
end;
end;
registration
let P be pcs-Str;
cluster pcs-coherent-power(P) -> pcs-self-coherent-membered
for Subset-Family of P;
coherence
by Th48;
end;
definition
let P be pcs-Str;
func pcs-power(P) -> pcs-Str equals
pcs-general-power(pcs-coherent-power(P));
coherence;
end;
registration
let P be pcs-Str;
cluster pcs-power(P) -> strict;
coherence;
end;
registration
let P be pcs-Str;
cluster pcs-power(P) -> non empty;
coherence;
end;
registration
let P be reflexive pcs-Str;
cluster pcs-power(P) -> reflexive;
coherence;
end;
registration
let P be transitive pcs-Str;
cluster pcs-power(P) -> transitive;
coherence;
end;
registration
let P be pcs-tol-reflexive pcs-Str;
cluster pcs-power(P) -> pcs-tol-reflexive;
coherence;
end;
registration
let P be pcs-tol-symmetric pcs-Str;
cluster pcs-power(P) -> pcs-tol-symmetric;
coherence;
end;
registration
let P be pcs-compatible pcs-Str;
cluster pcs-power(P) -> pcs-compatible;
coherence;
end;
registration
let P be pcs;
cluster pcs-power(P) -> pcs-like;
coherence;
end;