:: Basic Operations on Preordered Coherent Spaces
:: by Klaus E. Grue and Artur Korni{\l}owicz
::
:: Received August 28, 2007
:: Copyright (c) 2007-2017 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;
begin
definition
let R1, R2 be set, R be Relation of R1,R2;
redefine func field R -> Subset of R1 \/ R2;
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;
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;
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;
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;
end;
theorem :: PCS_0:1
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;
definition
let I be non empty set, C be 1-sorted-yielding ManySortedSet of I;
redefine func Carrier C means
:: PCS_0:def 1
for i being Element of I holds it.i = the carrier of C.i;
end;
definition
let R1, R2, S1, S2 be set;
let R be Relation of R1,R2, S be Relation of S1,S2;
func [^R,S^] -> Relation of [:R1,S1:],[:R2,S2:] means
:: PCS_0:def 2
for x, y being object holds [x,y] in it iff
ex r1, s1, r2, s2 being set st x = [r1,s1] & y = [r2,s2] &
r1 in R1 & s1 in S1 & r2 in R2 & s2 in S2 & ([r1,r2] in R or [s1,s2] in S);
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
:: PCS_0:def 3
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;
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;
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;
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;
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;
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;
end;
begin :: Relational Structures
registration
cluster empty -> total for RelStr;
end;
definition
let R be Relation;
attr R is transitive-yielding means
:: PCS_0:def 4
for S being RelStr st S in rng R holds S is transitive;
end;
registration
cluster Poset-yielding -> transitive-yielding for Relation;
end;
registration
cluster Poset-yielding for Function;
end;
registration
let I be set;
cluster Poset-yielding for ManySortedSet of I;
end;
definition
let I be set, C be RelStr-yielding ManySortedSet of I;
func pcs-InternalRels C -> ManySortedSet of I means
:: PCS_0:def 5
for i being set st i in I
ex P being RelStr st P = C.i & it.i = the InternalRel of P;
end;
definition
let I be non empty set, C be RelStr-yielding ManySortedSet of I;
redefine func pcs-InternalRels C means
:: PCS_0:def 6
for i being Element of I holds it.i = the InternalRel of C.i;
end;
registration
let I be set, C be RelStr-yielding ManySortedSet of I;
cluster pcs-InternalRels C -> Relation-yielding;
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;
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
:: PCS_0:def 7
[p,q] in the ToleranceRel of P;
end;
definition
let P be TolStr;
attr P is pcs-tol-total means
:: PCS_0:def 8
the ToleranceRel of P is total;
attr P is pcs-tol-reflexive means
:: PCS_0:def 9
the ToleranceRel of P is_reflexive_in the carrier of P;
attr P is pcs-tol-irreflexive means
:: PCS_0:def 10
the ToleranceRel of P is_irreflexive_in the carrier of P;
attr P is pcs-tol-symmetric means
:: PCS_0:def 11
the ToleranceRel of P is_symmetric_in the carrier of P;
end;
definition
func emptyTolStr -> TolStr equals
:: PCS_0:def 12
TolStr (# {}, {}({},{}) #);
end;
registration
cluster emptyTolStr -> empty strict;
end;
theorem :: PCS_0:2
for P being TolStr st P is empty holds the TolStr of P = emptyTolStr;
registration
cluster pcs-tol-reflexive -> pcs-tol-total for TolStr;
end;
registration
cluster empty -> pcs-tol-reflexive pcs-tol-irreflexive pcs-tol-symmetric
for TolStr;
end;
registration
cluster empty strict for TolStr;
end;
registration
let P be pcs-tol-total TolStr;
cluster the ToleranceRel of P -> total;
end;
registration
let P be pcs-tol-reflexive TolStr;
cluster the ToleranceRel of P -> reflexive;
end;
registration
let P be pcs-tol-irreflexive TolStr;
cluster the ToleranceRel of P -> irreflexive;
end;
registration
let P be pcs-tol-symmetric TolStr;
cluster the ToleranceRel of P -> symmetric;
end;
registration
let L be pcs-tol-total TolStr;
cluster the TolStr of L -> pcs-tol-total;
end;
definition
let P be pcs-tol-symmetric TolStr;
let p, q be Element of P;
redefine pred p (--) q;
symmetry;
end;
registration
let D be set;
cluster TolStr(#D,nabla D#) -> pcs-tol-reflexive pcs-tol-symmetric;
end;
registration
let D be set;
cluster TolStr(#D,{}(D,D)#) -> pcs-tol-irreflexive pcs-tol-symmetric;
end;
registration
cluster strict non empty pcs-tol-reflexive pcs-tol-symmetric for TolStr;
end;
registration
cluster strict non empty pcs-tol-irreflexive pcs-tol-symmetric for TolStr;
end;
definition
let R be Relation;
attr R is TolStr-yielding means
:: PCS_0:def 13
for P being set st P in rng R holds P is TolStr;
end;
definition
let f be Function;
redefine attr f is TolStr-yielding means
:: PCS_0:def 14
for x being set st x in dom f holds f.x is TolStr;
end;
definition
let I be set, f be ManySortedSet of I;
redefine attr f is TolStr-yielding means
:: PCS_0:def 15
for x being set st x in I holds f.x is TolStr;
end;
definition
let R be Relation;
attr R is pcs-tol-reflexive-yielding means
:: PCS_0:def 16
for S being TolStr st S in rng R holds S is pcs-tol-reflexive;
attr R is pcs-tol-irreflexive-yielding means
:: PCS_0:def 17
for S being TolStr st S in rng R holds S is pcs-tol-irreflexive;
attr R is pcs-tol-symmetric-yielding means
:: PCS_0:def 18
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;
end;
registration
let I be set, P be TolStr;
cluster I --> P -> TolStr-yielding for ManySortedSet of I;
end;
registration
let I be set, P be pcs-tol-reflexive TolStr;
cluster I --> P -> pcs-tol-reflexive-yielding for ManySortedSet of I;
end;
registration
let I be set, P be pcs-tol-irreflexive TolStr;
cluster I --> P -> pcs-tol-irreflexive-yielding for ManySortedSet of I;
end;
registration
let I be set, P be pcs-tol-symmetric TolStr;
cluster I --> P -> pcs-tol-symmetric-yielding for ManySortedSet of I;
end;
registration
cluster TolStr-yielding -> 1-sorted-yielding for Function;
end;
registration
let I be set;
cluster pcs-tol-reflexive-yielding pcs-tol-symmetric-yielding TolStr-yielding
for ManySortedSet of I;
end;
registration
let I be set;
cluster pcs-tol-irreflexive-yielding pcs-tol-symmetric-yielding
TolStr-yielding for ManySortedSet of I;
end;
registration
let I be set;
cluster TolStr-yielding for ManySortedSet of I;
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;
end;
definition
let I be set, C be TolStr-yielding ManySortedSet of I;
func pcs-ToleranceRels C -> ManySortedSet of I means
:: PCS_0:def 19
for i being set st i in I
ex P being TolStr st P = C.i & it.i = the ToleranceRel of P;
end;
definition
let I be non empty set, C be TolStr-yielding ManySortedSet of I;
redefine func pcs-ToleranceRels C means
:: PCS_0:def 20
for i being Element of I holds it.i = the ToleranceRel of C.i;
end;
registration
let I be set, C be TolStr-yielding ManySortedSet of I;
cluster pcs-ToleranceRels C -> Relation-yielding;
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;
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;
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;
end;
theorem :: PCS_0:3
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 :: PCS_0:4
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 :: PCS_0:5
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
:: PCS_0:def 21
TolStr (# [: the carrier of P, the carrier of Q :],
[^ the ToleranceRel of P, the ToleranceRel of Q ^] #);
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^];
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;
redefine func p^`2 -> Element of Q;
end;
theorem :: PCS_0:6
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;
theorem :: PCS_0:7
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;
registration
let P be TolStr, Q be pcs-tol-reflexive TolStr;
cluster [^P,Q^] -> pcs-tol-reflexive;
end;
registration
let P be pcs-tol-reflexive TolStr, Q be TolStr;
cluster [^P,Q^] -> pcs-tol-reflexive;
end;
registration
let P, Q be pcs-tol-symmetric TolStr;
cluster [^P,Q^] -> pcs-tol-symmetric;
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
:: PCS_0:def 22
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
:: PCS_0:def 23
P is reflexive transitive pcs-tol-reflexive pcs-tol-symmetric pcs-compatible;
attr P is anti-pcs-like means
:: PCS_0:def 24
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;
cluster reflexive transitive pcs-tol-reflexive pcs-tol-symmetric
pcs-compatible -> pcs-like for pcs-Str;
cluster anti-pcs-like -> reflexive transitive pcs-tol-irreflexive
pcs-tol-symmetric pcs-compatible for pcs-Str;
cluster reflexive transitive pcs-tol-irreflexive pcs-tol-symmetric
pcs-compatible -> anti-pcs-like for pcs-Str;
end;
definition
let D be set;
func pcs-total D -> pcs-Str equals
:: PCS_0:def 25
pcs-Str (# D,nabla D,nabla D #);
end;
registration
let D be set;
cluster pcs-total D -> strict;
end;
registration
let D be non empty set;
cluster pcs-total D -> non empty;
end;
registration
let D be set;
cluster pcs-total D -> reflexive transitive
pcs-tol-reflexive pcs-tol-symmetric;
end;
registration
let D be set;
cluster pcs-total D -> pcs-like;
end;
registration
let D be set;
cluster pcs-Str(#D,nabla D,{}(D,D)#) -> anti-pcs-like;
end;
registration
cluster strict non empty pcs-like for pcs-Str;
cluster strict non empty anti-pcs-like for pcs-Str;
end;
definition
mode pcs is pcs-like pcs-Str;
mode anti-pcs is anti-pcs-like pcs-Str;
end;
definition
func pcs-empty -> pcs-Str equals
:: PCS_0:def 26
pcs-total 0;
end;
registration
cluster pcs-empty -> strict empty pcs-like;
end;
definition
let p be set;
func pcs-singleton p -> pcs-Str equals
:: PCS_0:def 27
pcs-total {p};
end;
registration
let p be set;
cluster pcs-singleton p -> strict non empty pcs-like;
end;
definition
let R be Relation;
attr R is pcs-Str-yielding means
:: PCS_0:def 28
for P being set st P in rng R holds P is pcs-Str;
attr R is pcs-yielding means
:: PCS_0:def 29
for P being set st P in rng R holds P is pcs;
end;
definition
let f be Function;
redefine attr f is pcs-Str-yielding means
:: PCS_0:def 30
for x being set st x in dom f holds f.x is pcs-Str;
redefine attr f is pcs-yielding means
:: PCS_0:def 31
for x being set st x in dom f holds f.x is pcs;
end;
definition
let I be set, f be ManySortedSet of I;
redefine attr f is pcs-Str-yielding means
:: PCS_0:def 32
for x being set st x in I holds f.x is pcs-Str;
redefine attr f is pcs-yielding means
:: PCS_0:def 33
for x being set st x in I holds f.x is pcs;
end;
registration
cluster pcs-Str-yielding -> TolStr-yielding RelStr-yielding for Relation;
cluster pcs-yielding -> pcs-Str-yielding for Relation;
cluster pcs-yielding -> reflexive-yielding transitive-yielding
pcs-tol-reflexive-yielding pcs-tol-symmetric-yielding for Relation;
end;
registration
let I be set, P be pcs;
cluster I --> P -> pcs-yielding for ManySortedSet of I;
end;
registration
let I be set;
cluster pcs-yielding for ManySortedSet of I;
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;
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;
end;
:: Union of PCS's
definition
let P, Q be pcs-Str;
pred P c= Q means
:: PCS_0:def 34
the carrier of P c= the carrier of Q &
the InternalRel of P c= the InternalRel of Q &
the ToleranceRel of P c= the ToleranceRel of Q;
reflexivity;
end;
theorem :: PCS_0:8
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 :: PCS_0:9
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;
definition
let C be Relation;
attr C is pcs-chain-like means
:: PCS_0:def 35
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;
end;
registration
cluster pcs-chain-like pcs-yielding for Function;
end;
registration
let I be set;
cluster pcs-chain-like pcs-yielding for ManySortedSet of I;
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
:: PCS_0:def 36
the carrier of it = Union Carrier C &
the InternalRel of it = Union pcs-InternalRels C &
the ToleranceRel of it = Union pcs-ToleranceRels C;
end;
theorem :: PCS_0:10
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;
theorem :: PCS_0:11
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;
theorem :: PCS_0:12
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;
theorem :: PCS_0:13
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;
registration
let I be set, C be reflexive-yielding pcs-Str-yielding ManySortedSet of I;
cluster pcs-union C -> reflexive;
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;
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;
end;
registration
let I be set, C be pcs-Chain of I;
cluster pcs-union C -> transitive pcs-compatible;
end;
:: Direct Sum of PCS's
definition let p,q be set;
func <%p,q%> -> ManySortedSet of {0,1} equals
:: PCS_0:def 37
<%p,q%>;
end;
registration
let P, Q be 1-sorted;
cluster <%P,Q%> -> 1-sorted-yielding;
end;
registration
let P, Q be RelStr;
cluster <%P,Q%> -> RelStr-yielding;
end;
registration
let P, Q be TolStr;
cluster <%P,Q%> -> TolStr-yielding;
end;
registration
let P, Q be pcs-Str;
cluster <%P,Q%> -> pcs-Str-yielding;
end;
registration
let P, Q be reflexive pcs-Str;
cluster <%P,Q%> -> reflexive-yielding;
end;
registration
let P, Q be transitive pcs-Str;
cluster <%P,Q%> -> transitive-yielding;
end;
registration
let P, Q be pcs-tol-reflexive pcs-Str;
cluster <%P,Q%> -> pcs-tol-reflexive-yielding;
end;
registration
let P, Q be pcs-tol-symmetric pcs-Str;
cluster <%P,Q%> -> pcs-tol-symmetric-yielding;
end;
registration
let P, Q be pcs;
cluster <%P,Q%> -> pcs-yielding;
end;
definition
::$CD
let P, Q be pcs-Str;
func pcs-sum(P,Q) -> pcs-Str equals
:: PCS_0:def 39
pcs-union <%P,Q%>;
end;
theorem :: PCS_0:14
for P, Q being pcs-Str holds
the carrier of pcs-sum(P,Q) = (the carrier of P) \/ the carrier of Q &
the InternalRel of pcs-sum(P,Q) =
(the InternalRel of P) \/ the InternalRel of Q &
the ToleranceRel of pcs-sum(P,Q) =
(the ToleranceRel of P) \/ the ToleranceRel of Q;
theorem :: PCS_0:15
for P, Q being pcs-Str holds pcs-sum(P,Q) = pcs-Str (#
(the carrier of P) \/ the carrier of Q,
(the InternalRel of P) \/ the InternalRel of Q,
(the ToleranceRel of P) \/ the ToleranceRel of Q #);
theorem :: PCS_0:16
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;
theorem :: PCS_0:17
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;
registration
let P, Q be reflexive pcs-Str;
cluster pcs-sum(P,Q) -> reflexive;
end;
registration
let P, Q be pcs-tol-reflexive pcs-Str;
cluster pcs-sum(P,Q) -> pcs-tol-reflexive;
end;
registration
let P, Q be pcs-tol-symmetric pcs-Str;
cluster pcs-sum(P,Q) -> pcs-tol-symmetric;
end;
theorem :: PCS_0:18
for P, Q being pcs holds
P misses Q implies the InternalRel of pcs-sum(P,Q) is transitive;
theorem :: PCS_0:19
for P, Q being pcs holds P misses Q implies pcs-sum(P,Q) is pcs-compatible;
theorem :: PCS_0:20
for P, Q being pcs holds P misses Q implies pcs-sum(P,Q) is pcs;
:: Extension
definition
let P be pcs-Str, a be set;
func pcs-extension(P,a) -> strict pcs-Str means
:: PCS_0:def 40
the carrier of it = {a} \/ the carrier of P & the InternalRel of it =
[:{a},the carrier of it:] \/ the InternalRel of P &
the ToleranceRel of it = [:{a},the carrier of it:] \/
[:the carrier of it,{a}:] \/ the ToleranceRel of P;
end;
registration
let P be pcs-Str, a be set;
cluster pcs-extension(P,a) -> non empty;
end;
theorem :: PCS_0:21
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);
theorem :: PCS_0:22
for P being pcs-Str, a being set,
p, q being Element of pcs-extension(P,a) st p = a holds p <= q;
theorem :: PCS_0:23
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;
theorem :: PCS_0:24
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;
theorem :: PCS_0:25
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;
theorem :: PCS_0:26
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;
theorem :: PCS_0:27
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;
theorem :: PCS_0:28
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;
theorem :: PCS_0:29
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;
registration
let P be reflexive pcs-Str, a be set;
cluster pcs-extension(P,a) -> reflexive;
end;
theorem :: PCS_0:30
for P being transitive pcs-Str, a being set st not a in the carrier of P
holds pcs-extension(P,a) is transitive;
registration
let P be pcs-tol-reflexive pcs-Str, a be set;
cluster pcs-extension(P,a) -> pcs-tol-reflexive;
end;
registration
let P be pcs-tol-symmetric pcs-Str, a be set;
cluster pcs-extension(P,a) -> pcs-tol-symmetric;
end;
theorem :: PCS_0:31
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;
theorem :: PCS_0:32
for P being pcs, a being set st not a in the carrier of P
holds pcs-extension(P,a) is pcs;
:: Reverse
definition
let P be pcs-Str;
func pcs-reverse(P) -> strict pcs-Str means
:: PCS_0:def 41
the carrier of it = the carrier of P &
the InternalRel of it = (the InternalRel of P)~ &
the ToleranceRel of it = (the ToleranceRel of P)`;
end;
registration
let P be non empty pcs-Str;
cluster pcs-reverse(P) -> non empty;
end;
theorem :: PCS_0:33
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;
theorem :: PCS_0:34
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;
theorem :: PCS_0:35
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;
registration
let P be reflexive pcs-Str;
cluster pcs-reverse(P) -> reflexive;
end;
registration
let P be transitive pcs-Str;
cluster pcs-reverse(P) -> transitive;
end;
registration
let P be pcs-tol-reflexive pcs-Str;
cluster pcs-reverse(P) -> pcs-tol-irreflexive;
end;
registration
let P be pcs-tol-irreflexive pcs-Str;
cluster pcs-reverse(P) -> pcs-tol-reflexive;
end;
registration
let P be pcs-tol-symmetric pcs-Str;
cluster pcs-reverse(P) -> pcs-tol-symmetric;
end;
registration
let P be pcs-compatible pcs-Str;
cluster pcs-reverse(P) -> pcs-compatible;
end;
:: Times
definition
let P, Q be pcs-Str;
func P pcs-times Q -> pcs-Str equals
:: PCS_0:def 42
pcs-Str (# [: the carrier of P, the carrier of Q :],
[" the InternalRel of P, the InternalRel of Q "],
[^ the ToleranceRel of P, the ToleranceRel of Q ^] #);
end;
registration
let P, Q be pcs-Str;
cluster P pcs-times Q -> strict;
end;
registration
let P, Q be non empty pcs-Str;
cluster P pcs-times Q -> non empty;
end;
theorem :: PCS_0:36
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;
theorem :: PCS_0:37
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;
theorem :: PCS_0:38
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;
registration
let P, Q be reflexive pcs-Str;
cluster P pcs-times Q -> reflexive;
end;
registration
let P, Q be transitive pcs-Str;
cluster P pcs-times Q -> transitive;
end;
registration
let P be pcs-Str;
let Q be pcs-tol-reflexive pcs-Str;
cluster P pcs-times Q -> pcs-tol-reflexive;
end;
registration
let P be pcs-tol-reflexive pcs-Str;
let Q be pcs-Str;
cluster P pcs-times Q -> pcs-tol-reflexive;
end;
registration
let P, Q be pcs-tol-symmetric pcs-Str;
cluster P pcs-times Q -> pcs-tol-symmetric;
end;
registration
let P, Q be pcs-compatible pcs-Str;
cluster P pcs-times Q -> pcs-compatible;
end;
definition
let P, Q be pcs-Str;
func P --> Q -> pcs-Str equals
:: PCS_0:def 43
(pcs-reverse P) pcs-times Q;
end;
registration
let P, Q be pcs-Str;
cluster P --> Q -> strict;
end;
registration
let P, Q be non empty pcs-Str;
cluster P --> Q -> non empty;
end;
theorem :: PCS_0:39
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;
theorem :: PCS_0:40
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
;
theorem :: PCS_0:41
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
;
registration
let P, Q be reflexive pcs-Str;
cluster P --> Q -> reflexive;
end;
registration
let P, Q be transitive pcs-Str;
cluster P --> Q -> transitive;
end;
registration
let P be pcs-Str, Q be pcs-tol-reflexive pcs-Str;
cluster P --> Q -> pcs-tol-reflexive;
end;
registration
let P be pcs-tol-irreflexive pcs-Str, Q be pcs-Str;
cluster P --> Q -> pcs-tol-reflexive;
end;
registration
let P, Q be pcs-tol-symmetric pcs-Str;
cluster P --> Q -> pcs-tol-symmetric;
end;
registration
let P, Q be pcs-compatible pcs-Str;
cluster P --> Q -> pcs-compatible;
end;
registration
let P, Q be pcs;
cluster P --> Q -> pcs-like;
end;
:: Self-coherence
definition
let P be TolStr, S be Subset of P;
attr S is pcs-self-coherent means
:: PCS_0:def 44
for x, y being Element of P st x in S & y in S holds x (--) y;
end;
registration
let P be TolStr;
cluster empty -> pcs-self-coherent for Subset of P;
end;
definition
let P be TolStr, F be Subset-Family of P;
attr F is pcs-self-coherent-membered means
:: PCS_0:def 45
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;
end;
definition
let P be RelStr, D be set;
func pcs-general-power-IR(P,D) -> Relation of D means
:: PCS_0:def 46
for A, B being set holds [A,B] in it iff A in D & B in D &
for a being set st a in A ex b being set st b in B &
[a,b] in the InternalRel of P;
end;
definition
let P be TolStr, D be set;
func pcs-general-power-TR(P,D) -> Relation of D means
:: PCS_0:def 47
for A, B being set holds [A,B] in it iff A in D & B in D &
for a, b being set st a in A & b in B holds [a,b] in the ToleranceRel of P;
end;
theorem :: PCS_0:42
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
;
theorem :: PCS_0:43
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;
definition
let P be pcs-Str, D be set;
func pcs-general-power(P,D) -> pcs-Str equals
:: PCS_0:def 48
pcs-Str (# D, pcs-general-power-IR(P,D), pcs-general-power-TR(P,D) #);
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;
end;
theorem :: PCS_0:44
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;
theorem :: PCS_0:45
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;
theorem :: PCS_0:46
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;
theorem :: PCS_0:47
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;
registration
let P be pcs-Str, D be set;
cluster pcs-general-power(P,D) -> strict;
end;
registration
let P be reflexive pcs-Str, D be Subset-Family of P;
cluster pcs-general-power(D) -> reflexive;
end;
registration
let P be transitive pcs-Str, D be set;
cluster pcs-general-power(P,D) -> transitive;
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;
end;
registration
let P be pcs-tol-symmetric pcs-Str, D be Subset-Family of P;
cluster pcs-general-power(D) -> pcs-tol-symmetric;
end;
registration
let P be pcs-compatible pcs-Str, D be Subset-Family of P;
cluster pcs-general-power(D) -> pcs-compatible;
end;
definition
let P be pcs-Str;
func pcs-coherent-power(P) -> set equals
:: PCS_0:def 49
{X where X is Subset of P: X is pcs-self-coherent};
end;
registration
let P be pcs-Str;
cluster pcs-self-coherent for Subset of P;
end;
theorem :: PCS_0:48
for P being pcs-Str, X being set holds X in pcs-coherent-power(P)
implies X is pcs-self-coherent Subset of P;
registration
let P be pcs-Str;
cluster pcs-coherent-power(P) -> non empty;
end;
definition
let P be pcs-Str;
redefine func pcs-coherent-power(P) -> Subset-Family of P;
end;
registration
let P be pcs-Str;
cluster pcs-coherent-power(P) -> pcs-self-coherent-membered
for Subset-Family of P;
end;
definition
let P be pcs-Str;
func pcs-power(P) -> pcs-Str equals
:: PCS_0:def 50
pcs-general-power(pcs-coherent-power(P));
end;
registration
let P be pcs-Str;
cluster pcs-power(P) -> strict;
end;
registration
let P be pcs-Str;
cluster pcs-power(P) -> non empty;
end;
registration
let P be reflexive pcs-Str;
cluster pcs-power(P) -> reflexive;
end;
registration
let P be transitive pcs-Str;
cluster pcs-power(P) -> transitive;
end;
registration
let P be pcs-tol-reflexive pcs-Str;
cluster pcs-power(P) -> pcs-tol-reflexive;
end;
registration
let P be pcs-tol-symmetric pcs-Str;
cluster pcs-power(P) -> pcs-tol-symmetric;
end;
registration
let P be pcs-compatible pcs-Str;
cluster pcs-power(P) -> pcs-compatible;
end;
registration
let P be pcs;
cluster pcs-power(P) -> pcs-like;
end;