:: by Katarzyna Romanowicz and Adam Grabowski

::

:: Received May 24, 2004

:: Copyright (c) 2004-2021 Association of Mizar Users

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 )

( x in B & y in A \ B )

proof end;

:: deftheorem 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 ) );

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

definition

let R, S be RelStr ;

ex b_{1} being strict RelStr st

( the carrier of b_{1} = the carrier of R \/ the carrier of S & the InternalRel of b_{1} = ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) )

for b_{1}, b_{2} being strict RelStr st the carrier of b_{1} = the carrier of R \/ the carrier of S & the InternalRel of b_{1} = ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) & the carrier of b_{2} = the carrier of R \/ the carrier of S & the InternalRel of b_{2} = ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) holds

b_{1} = b_{2}
;

end;
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 ( 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) );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def2 defines [*] LATSUM_1:def 2 :

for R, S being RelStr

for b_{3} being strict RelStr holds

( b_{3} = R [*] S iff ( the carrier of b_{3} = the carrier of R \/ the carrier of S & the InternalRel of b_{3} = ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) ) );

for R, S being RelStr

for b

( b

registration
end;

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

( the InternalRel of R c= the InternalRel of (R [*] S) & the InternalRel of S c= the InternalRel of (R [*] S) )

proof end;

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

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

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

for a, b being object 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 )

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 )

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 )

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)

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)

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

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

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

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 )

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

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

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

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

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

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

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 )

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

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

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

R [*] S is transitive

proof end;