:: The Operation of Addition of Relational Structures :: by Katarzyna Romanowicz and Adam Grabowski :: :: Received May 24, 2004 :: Copyright (c) 2004-2012 Association of Mizar Users begin theorem :: LATSUM_1:1 for x, y, A, B being set st x in A \/ B & y in A \/ B & not ( x in A \ B & y in A \ B ) & not ( x in B & y in B ) & not ( x in A \ B & y in B ) holds ( x in B & y in A \ B ) proofend; definition let R, S be RelStr ; predR tolerates S means :Def1: :: LATSUM_1:def 1 for x, y being set st x in the carrier of R /\ the carrier of S & y in the carrier of R /\ the carrier of S holds ( [x,y] in the InternalRel of R iff [x,y] in the InternalRel of S ); end; :: deftheorem Def1 defines tolerates LATSUM_1:def_1_:_ for R, S being RelStr holds ( R tolerates S iff for x, y being set st x in the carrier of R /\ the carrier of S & y in the carrier of R /\ the carrier of S holds ( [x,y] in the InternalRel of R iff [x,y] in the InternalRel of S ) ); begin definition let R, S be RelStr ; funcR [*] S -> strict RelStr means :Def2: :: LATSUM_1:def 2 ( the carrier of it = the carrier of R \/ the carrier of S & the InternalRel of it = ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) ); existence ex b1 being strict RelStr st ( the carrier of b1 = the carrier of R \/ the carrier of S & the InternalRel of b1 = ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) ) proofend; uniqueness for b1, b2 being strict RelStr st the carrier of b1 = the carrier of R \/ the carrier of S & the InternalRel of b1 = ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) & the carrier of b2 = the carrier of R \/ the carrier of S & the InternalRel of b2 = ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) holds b1 = b2 ; end; :: deftheorem Def2 defines [*] LATSUM_1:def_2_:_ for R, S being RelStr for b3 being strict RelStr holds ( b3 = R [*] S iff ( the carrier of b3 = the carrier of R \/ the carrier of S & the InternalRel of b3 = ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) ) ); registration let R be RelStr ; let S be non empty RelStr ; clusterR [*] S -> non empty strict ; coherence not R [*] S is empty proofend; end; registration let R be non empty RelStr ; let S be RelStr ; clusterR [*] S -> non empty strict ; coherence not R [*] S is empty proofend; end; theorem Th2: :: LATSUM_1:2 for R, S being RelStr holds ( the InternalRel of R c= the InternalRel of (R [*] S) & the InternalRel of S c= the InternalRel of (R [*] S) ) proofend; theorem Th3: :: LATSUM_1:3 for R, S being RelStr st R is reflexive & S is reflexive holds R [*] S is reflexive proofend; begin theorem Th4: :: LATSUM_1:4 for R, S being RelStr for a, b being set st [a,b] in the InternalRel of (R [*] S) & a in the carrier of R & b in the carrier of R & R tolerates S & R is transitive holds [a,b] in the InternalRel of R proofend; theorem Th5: :: LATSUM_1:5 for R, S being RelStr for a, b being set st [a,b] in the InternalRel of (R [*] S) & a in the carrier of S & b in the carrier of S & R tolerates S & S is transitive holds [a,b] in the InternalRel of S proofend; theorem Th6: :: LATSUM_1:6 for R, S being RelStr for a, b being set holds ( ( [a,b] in the InternalRel of R implies [a,b] in the InternalRel of (R [*] S) ) & ( [a,b] in the InternalRel of S implies [a,b] in the InternalRel of (R [*] S) ) ) proofend; theorem :: LATSUM_1:7 for R, S being non empty RelStr for x being Element of (R [*] S) holds ( x in the carrier of R or x in the carrier of S \ the carrier of R ) proofend; theorem Th8: :: LATSUM_1:8 for R, S being non empty RelStr for x, y being Element of R for a, b being Element of (R [*] S) st x = a & y = b & R tolerates S & R is transitive holds ( x <= y iff a <= b ) proofend; theorem Th9: :: LATSUM_1:9 for R, S being non empty RelStr for a, b being Element of (R [*] S) for c, d being Element of S st a = c & b = d & R tolerates S & S is transitive holds ( a <= b iff c <= d ) proofend; theorem Th10: :: LATSUM_1:10 for R, S being non empty reflexive transitive antisymmetric with_suprema RelStr for x being set st x in the carrier of R holds x is Element of (R [*] S) proofend; theorem :: LATSUM_1:11 for R, S being non empty reflexive transitive antisymmetric with_suprema RelStr for x being set st x in the carrier of S holds x is Element of (R [*] S) proofend; theorem Th12: :: LATSUM_1:12 for R, S being non empty RelStr for x being set st x in the carrier of R /\ the carrier of S holds x is Element of R proofend; theorem Th13: :: LATSUM_1:13 for R, S being non empty RelStr for x being set st x in the carrier of R /\ the carrier of S holds x is Element of S proofend; theorem :: LATSUM_1:14 for R, S being non empty reflexive transitive antisymmetric with_suprema RelStr for x, y being Element of (R [*] S) st x in the carrier of R & y in the carrier of S & R tolerates S holds ( x <= y iff ex a being Element of (R [*] S) st ( a in the carrier of R /\ the carrier of S & x <= a & a <= y ) ) proofend; theorem Th15: :: LATSUM_1:15 for R, S being non empty RelStr for a, b being Element of R for c, d being Element of S st a = c & b = d & R tolerates S & R is transitive & S is transitive holds ( a <= b iff c <= d ) proofend; theorem Th16: :: LATSUM_1:16 for R being non empty reflexive transitive antisymmetric with_suprema RelStr for D being directed lower Subset of R for x, y being Element of R st x in D & y in D holds x "\/" y in D proofend; theorem Th17: :: LATSUM_1:17 for R, S being RelStr for a, b being set st the carrier of R /\ the carrier of S is upper Subset of R & [a,b] in the InternalRel of (R [*] S) & a in the carrier of S holds b in the carrier of S proofend; theorem Th18: :: LATSUM_1:18 for R, S being RelStr for a, b being Element of (R [*] S) st the carrier of R /\ the carrier of S is upper Subset of R & a <= b & a in the carrier of S holds b in the carrier of S proofend; theorem :: LATSUM_1:19 for R, S being non empty reflexive transitive antisymmetric with_suprema RelStr for x, y being Element of R for a, b being Element of S st the carrier of R /\ the carrier of S is directed lower Subset of S & the carrier of R /\ the carrier of S is upper Subset of R & R tolerates S & x = a & y = b holds x "\/" y = a "\/" b proofend; theorem :: LATSUM_1:20 for R, S being non empty reflexive transitive antisymmetric with_suprema lower-bounded RelStr st the carrier of R /\ the carrier of S is non empty directed lower Subset of S holds Bottom S in the carrier of R proofend; theorem Th21: :: LATSUM_1:21 for R, S being RelStr for a, b being set st the carrier of R /\ the carrier of S is lower Subset of S & [a,b] in the InternalRel of (R [*] S) & b in the carrier of R holds a in the carrier of R proofend; theorem :: LATSUM_1:22 for x, y being set for R, S being RelStr st [x,y] in the InternalRel of (R [*] S) & the carrier of R /\ the carrier of S is upper Subset of R & not ( x in the carrier of R & y in the carrier of R ) & not ( x in the carrier of S & y in the carrier of S ) holds ( x in the carrier of R \ the carrier of S & y in the carrier of S \ the carrier of R ) proofend; theorem :: LATSUM_1:23 for R, S being RelStr for a, b being Element of (R [*] S) st the carrier of R /\ the carrier of S is lower Subset of S & a <= b & b in the carrier of R holds a in the carrier of R proofend; theorem :: LATSUM_1:24 for R, S being RelStr st R tolerates S & the carrier of R /\ the carrier of S is upper Subset of R & the carrier of R /\ the carrier of S is lower Subset of S & R is transitive & R is antisymmetric & S is transitive & S is antisymmetric holds R [*] S is antisymmetric proofend; theorem :: LATSUM_1:25 for R, S being RelStr st the carrier of R /\ the carrier of S is upper Subset of R & the carrier of R /\ the carrier of S is lower Subset of S & R tolerates S & R is transitive & S is transitive holds R [*] S is transitive proofend;