:: The Operation of Addition of Relational Structures
:: by Katarzyna Romanowicz and Adam Grabowski
::
:: Received May 24, 2004
:: Copyright (c) 2004-2011 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 )

proof end;

definition

let R, S be RelStr ;
pred R 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 ;
func R [*] 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 b₁ being strict RelStr st
( the carrier of b₁ = the carrier of R \/ the carrier of S & the InternalRel of b₁ = ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) )

proof end;

uniqueness
for b₁, b₂ being strict RelStr st the carrier of b₁ = the carrier of R \/ the carrier of S & the InternalRel of b₁ = ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) & the carrier of b₂ = the carrier of R \/ the carrier of S & the InternalRel of b₂ = ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) holds
b₁ = b₂ ;

end;

:: deftheorem Def2 defines [*] LATSUM_1:def 2 :
for R, S being RelStr
for b₃ being strict RelStr holds
( b₃ = R [*] S iff ( the carrier of b₃ = the carrier of R \/ the carrier of S & the InternalRel of b₃ = ( 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 ;
cluster R [*] S -> non empty strict ;
coherence
not R [*] S is empty

proof end;

end;

registration

let R be non empty RelStr ;
let S be RelStr ;
cluster R [*] S -> non empty strict ;
coherence
not R [*] S is empty

proof end;

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) )

proof end;

theorem Th3: :: LATSUM_1:3

for R, S being RelStr st R is reflexive & S is reflexive holds
R [*] S is reflexive

proof end;

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

proof end;

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

proof end;

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) ) )

proof end;

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 )

proof end;

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 )

proof end;

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 )

proof end;

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)

proof end;

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)

proof end;

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

proof end;

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

proof end;

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 ) )

proof end;

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 )

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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 )

proof end;

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

proof end;

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

proof end;

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

proof end;