:: The Properties of Product of Relational Structures
:: by Artur Korni{\l}owicz
::
:: Received March 27, 1998
:: Copyright (c) 1998-2021 Association of Mizar Users

registration

let S, T be non empty upper-bounded RelStr ;

cluster [:S,T:] -> upper-bounded ;

coherence
[:S,T:] is upper-bounded

proof end;

end;

registration

let S, T be non empty lower-bounded RelStr ;

cluster [:S,T:] -> lower-bounded ;

coherence
[:S,T:] is lower-bounded

proof end;

end;

theorem :: YELLOW10:1

for S, T being non empty RelStr st [:S,T:] is upper-bounded holds
( S is upper-bounded & T is upper-bounded )

proof end;

theorem :: YELLOW10:2

for S, T being non empty RelStr st [:S,T:] is lower-bounded holds
( S is lower-bounded & T is lower-bounded )

proof end;

theorem Th3: :: YELLOW10:3

for S, T being non empty antisymmetric upper-bounded RelStr holds Top [:S,T:] = [(Top S),(Top T)]

proof end;

theorem Th4: :: YELLOW10:4

for S, T being non empty antisymmetric lower-bounded RelStr holds Bottom [:S,T:] = [(Bottom S),(Bottom T)]

proof end;

theorem Th5: :: YELLOW10:5

for S, T being non empty antisymmetric lower-bounded RelStr
for D being Subset of [:S,T:] st ( [:S,T:] is complete or ex_sup_of D,[:S,T:] ) holds
sup D = [(sup (proj1 D)),(sup (proj2 D))]

proof end;

theorem :: YELLOW10:6

for S, T being non empty antisymmetric upper-bounded RelStr
for D being Subset of [:S,T:] st ( [:S,T:] is complete or ex_inf_of D,[:S,T:] ) holds
inf D = [(inf (proj1 D)),(inf (proj2 D))]

proof end;

theorem :: YELLOW10:7

for S, T being non empty RelStr
for x, y being Element of [:S,T:] holds
( x is_<=_than {y} iff ( x `1 is_<=_than {(y `1)} & x `2 is_<=_than {(y `2)} ) )

proof end;

theorem :: YELLOW10:8

for S, T being non empty RelStr
for x, y, z being Element of [:S,T:] holds
( x is_<=_than {y,z} iff ( x `1 is_<=_than {(y `1),(z `1)} & x `2 is_<=_than {(y `2),(z `2)} ) )

proof end;

theorem :: YELLOW10:9

for S, T being non empty RelStr
for x, y being Element of [:S,T:] holds
( x is_>=_than {y} iff ( x `1 is_>=_than {(y `1)} & x `2 is_>=_than {(y `2)} ) )

proof end;

theorem :: YELLOW10:10

for S, T being non empty RelStr
for x, y, z being Element of [:S,T:] holds
( x is_>=_than {y,z} iff ( x `1 is_>=_than {(y `1),(z `1)} & x `2 is_>=_than {(y `2),(z `2)} ) )

proof end;

theorem :: YELLOW10:11

for S, T being non empty antisymmetric RelStr
for x, y being Element of [:S,T:] holds
( ex_inf_of {x,y},[:S,T:] iff ( ex_inf_of {(x `1),(y `1)},S & ex_inf_of {(x `2),(y `2)},T ) )

proof end;

theorem :: YELLOW10:12

for S, T being non empty antisymmetric RelStr
for x, y being Element of [:S,T:] holds
( ex_sup_of {x,y},[:S,T:] iff ( ex_sup_of {(x `1),(y `1)},S & ex_sup_of {(x `2),(y `2)},T ) )

proof end;

theorem Th13: :: YELLOW10:13

for S, T being antisymmetric with_infima RelStr
for x, y being Element of [:S,T:] holds
( (x "/\" y) `1 = (x `1) "/\" (y `1) & (x "/\" y) `2 = (x `2) "/\" (y `2) )

proof end;

theorem Th14: :: YELLOW10:14

for S, T being antisymmetric with_suprema RelStr
for x, y being Element of [:S,T:] holds
( (x "\/" y) `1 = (x `1) "\/" (y `1) & (x "\/" y) `2 = (x `2) "\/" (y `2) )

proof end;

theorem Th15: :: YELLOW10:15

for S, T being antisymmetric with_infima RelStr
for x1, y1 being Element of S
for x2, y2 being Element of T holds [(x1 "/\" y1),(x2 "/\" y2)] = [x1,x2] "/\" [y1,y2]

proof end;

theorem Th16: :: YELLOW10:16

for S, T being antisymmetric with_suprema RelStr
for x1, y1 being Element of S
for x2, y2 being Element of T holds [(x1 "\/" y1),(x2 "\/" y2)] = [x1,x2] "\/" [y1,y2]

proof end;

definition

let S be antisymmetric with_suprema with_infima RelStr ;
let x, y be Element of S;
:: original: is_a_complement_of
redefine pred y is_a_complement_of x;
symmetry
for y, x being Element of S st R55(S,b₂,b₁) holds
R55(S,b₁,b₂)

proof end;

end;

theorem Th17: :: YELLOW10:17

for S, T being antisymmetric bounded with_suprema with_infima RelStr
for x, y being Element of [:S,T:] holds
( x is_a_complement_of y iff ( x `1 is_a_complement_of y `1 & x `2 is_a_complement_of y `2 ) )

proof end;

theorem Th18: :: YELLOW10:18

for S, T being non empty reflexive antisymmetric up-complete RelStr
for a, c being Element of S
for b, d being Element of T st [a,b] << [c,d] holds
( a << c & b << d )

proof end;

theorem Th19: :: YELLOW10:19

for S, T being non empty up-complete Poset
for a, c being Element of S
for b, d being Element of T holds
( [a,b] << [c,d] iff ( a << c & b << d ) )

proof end;

theorem Th20: :: YELLOW10:20

for S, T being non empty reflexive antisymmetric up-complete RelStr
for x, y being Element of [:S,T:] st x << y holds
( x `1 << y `1 & x `2 << y `2 )

proof end;

theorem Th21: :: YELLOW10:21

for S, T being non empty up-complete Poset
for x, y being Element of [:S,T:] holds
( x << y iff ( x `1 << y `1 & x `2 << y `2 ) )

proof end;

theorem Th22: :: YELLOW10:22

for S, T being non empty reflexive antisymmetric up-complete RelStr
for x being Element of [:S,T:] st x is compact holds
( x `1 is compact & x `2 is compact )

proof end;

theorem Th23: :: YELLOW10:23

for S, T being non empty up-complete Poset
for x being Element of [:S,T:] st x `1 is compact & x `2 is compact holds
x is compact

proof end;

theorem Th24: :: YELLOW10:24

for S, T being antisymmetric with_infima RelStr
for X, Y being Subset of [:S,T:] holds
( proj1 (X "/\" Y) = (proj1 X) "/\" (proj1 Y) & proj2 (X "/\" Y) = (proj2 X) "/\" (proj2 Y) )

proof end;

theorem :: YELLOW10:25

for S, T being antisymmetric with_suprema RelStr
for X, Y being Subset of [:S,T:] holds
( proj1 (X "\/" Y) = (proj1 X) "\/" (proj1 Y) & proj2 (X "\/" Y) = (proj2 X) "\/" (proj2 Y) )

proof end;

theorem :: YELLOW10:26

for S, T being RelStr
for X being Subset of [:S,T:] holds downarrow X c= [:(downarrow (proj1 X)),(downarrow (proj2 X)):]

proof end;

theorem :: YELLOW10:27

for S, T being RelStr
for X being Subset of S
for Y being Subset of T holds [:(downarrow X),(downarrow Y):] = downarrow [:X,Y:]

proof end;

theorem Th28: :: YELLOW10:28

for S, T being RelStr
for X being Subset of [:S,T:] holds
( proj1 (downarrow X) c= downarrow (proj1 X) & proj2 (downarrow X) c= downarrow (proj2 X) )

proof end;

theorem :: YELLOW10:29

for S being RelStr
for T being reflexive RelStr
for X being Subset of [:S,T:] holds proj1 (downarrow X) = downarrow (proj1 X)

proof end;

theorem :: YELLOW10:30

for S being reflexive RelStr
for T being RelStr
for X being Subset of [:S,T:] holds proj2 (downarrow X) = downarrow (proj2 X)

proof end;

theorem :: YELLOW10:31

for S, T being RelStr
for X being Subset of [:S,T:] holds uparrow X c= [:(uparrow (proj1 X)),(uparrow (proj2 X)):]

proof end;

theorem :: YELLOW10:32

for S, T being RelStr
for X being Subset of S
for Y being Subset of T holds [:(uparrow X),(uparrow Y):] = uparrow [:X,Y:]

proof end;

theorem Th33: :: YELLOW10:33

for S, T being RelStr
for X being Subset of [:S,T:] holds
( proj1 (uparrow X) c= uparrow (proj1 X) & proj2 (uparrow X) c= uparrow (proj2 X) )

proof end;

theorem :: YELLOW10:34

for S being RelStr
for T being reflexive RelStr
for X being Subset of [:S,T:] holds proj1 (uparrow X) = uparrow (proj1 X)

proof end;

theorem :: YELLOW10:35

for S being reflexive RelStr
for T being RelStr
for X being Subset of [:S,T:] holds proj2 (uparrow X) = uparrow (proj2 X)

proof end;

theorem :: YELLOW10:36

for S, T being non empty RelStr
for s being Element of S
for t being Element of T holds [:(downarrow s),(downarrow t):] = downarrow [s,t]

proof end;

theorem Th37: :: YELLOW10:37

for S, T being non empty RelStr
for x being Element of [:S,T:] holds
( proj1 (downarrow x) c= downarrow (x `1) & proj2 (downarrow x) c= downarrow (x `2) )

proof end;

theorem :: YELLOW10:38

for S being non empty RelStr
for T being non empty reflexive RelStr
for x being Element of [:S,T:] holds proj1 (downarrow x) = downarrow (x `1)

proof end;

theorem :: YELLOW10:39

for S being non empty reflexive RelStr
for T being non empty RelStr
for x being Element of [:S,T:] holds proj2 (downarrow x) = downarrow (x `2)

proof end;

theorem :: YELLOW10:40

for S, T being non empty RelStr
for s being Element of S
for t being Element of T holds [:(uparrow s),(uparrow t):] = uparrow [s,t]

proof end;

theorem Th41: :: YELLOW10:41

for S, T being non empty RelStr
for x being Element of [:S,T:] holds
( proj1 (uparrow x) c= uparrow (x `1) & proj2 (uparrow x) c= uparrow (x `2) )

proof end;

theorem :: YELLOW10:42

for S being non empty RelStr
for T being non empty reflexive RelStr
for x being Element of [:S,T:] holds proj1 (uparrow x) = uparrow (x `1)

proof end;

theorem :: YELLOW10:43

for S being non empty reflexive RelStr
for T being non empty RelStr
for x being Element of [:S,T:] holds proj2 (uparrow x) = uparrow (x `2)

proof end;

theorem Th44: :: YELLOW10:44

for S, T being non empty up-complete Poset
for s being Element of S
for t being Element of T holds [:(waybelow s),(waybelow t):] = waybelow [s,t]

proof end;

theorem Th45: :: YELLOW10:45

for S, T being non empty reflexive antisymmetric up-complete RelStr
for x being Element of [:S,T:] holds
( proj1 (waybelow x) c= waybelow (x `1) & proj2 (waybelow x) c= waybelow (x `2) )

proof end;

theorem Th46: :: YELLOW10:46

for S being non empty up-complete Poset
for T being non empty lower-bounded up-complete Poset
for x being Element of [:S,T:] holds proj1 (waybelow x) = waybelow (x `1)

proof end;

theorem Th47: :: YELLOW10:47

for S being non empty lower-bounded up-complete Poset
for T being non empty up-complete Poset
for x being Element of [:S,T:] holds proj2 (waybelow x) = waybelow (x `2)

proof end;

theorem :: YELLOW10:48

for S, T being non empty up-complete Poset
for s being Element of S
for t being Element of T holds [:(wayabove s),(wayabove t):] = wayabove [s,t]

proof end;

theorem :: YELLOW10:49

for S, T being non empty reflexive antisymmetric up-complete RelStr
for x being Element of [:S,T:] holds
( proj1 (wayabove x) c= wayabove (x `1) & proj2 (wayabove x) c= wayabove (x `2) )

proof end;

theorem Th50: :: YELLOW10:50

for S, T being non empty up-complete Poset
for s being Element of S
for t being Element of T holds [:(compactbelow s),(compactbelow t):] = compactbelow [s,t]

proof end;

theorem Th51: :: YELLOW10:51

for S, T being non empty reflexive antisymmetric up-complete RelStr
for x being Element of [:S,T:] holds
( proj1 (compactbelow x) c= compactbelow (x `1) & proj2 (compactbelow x) c= compactbelow (x `2) )

proof end;

theorem Th52: :: YELLOW10:52

for S being non empty up-complete Poset
for T being non empty lower-bounded up-complete Poset
for x being Element of [:S,T:] holds proj1 (compactbelow x) = compactbelow (x `1)

proof end;

theorem Th53: :: YELLOW10:53

for S being non empty lower-bounded up-complete Poset
for T being non empty up-complete Poset
for x being Element of [:S,T:] holds proj2 (compactbelow x) = compactbelow (x `2)

proof end;

registration

let S be non empty reflexive RelStr ;

cluster empty -> Open for M3( bool the carrier of S);

coherence
for b₁ being Subset of S st b₁ is empty holds
b₁ is Open

proof end;

end;

theorem :: YELLOW10:54

for S, T being non empty reflexive antisymmetric up-complete RelStr
for X being Subset of [:S,T:] st X is Open holds
( proj1 X is Open & proj2 X is Open )

proof end;

theorem :: YELLOW10:55

for S, T being non empty up-complete Poset
for X being Subset of S
for Y being Subset of T st X is Open & Y is Open holds
[:X,Y:] is Open

proof end;

theorem :: YELLOW10:56

for S, T being non empty reflexive antisymmetric up-complete RelStr
for X being Subset of [:S,T:] st X is inaccessible holds
( proj1 X is inaccessible & proj2 X is inaccessible )

proof end;

theorem :: YELLOW10:57

for S, T being non empty reflexive antisymmetric up-complete RelStr
for X being upper Subset of S
for Y being upper Subset of T st X is inaccessible & Y is inaccessible holds
[:X,Y:] is inaccessible

proof end;

theorem :: YELLOW10:58

for S, T being non empty reflexive antisymmetric up-complete RelStr
for X being Subset of S
for Y being Subset of T st [:X,Y:] is directly_closed holds
( ( Y <> {} implies X is directly_closed ) & ( X <> {} implies Y is directly_closed ) )

proof end;

theorem :: YELLOW10:59

for S, T being non empty reflexive antisymmetric up-complete RelStr
for X being Subset of S
for Y being Subset of T st X is directly_closed & Y is directly_closed holds
[:X,Y:] is directly_closed

proof end;

theorem :: YELLOW10:60

for S, T being non empty reflexive antisymmetric up-complete RelStr
for X being Subset of [:S,T:] st X is property(S) holds
( proj1 X is property(S) & proj2 X is property(S) )

proof end;

theorem :: YELLOW10:61

for S, T being non empty up-complete Poset
for X being Subset of S
for Y being Subset of T st X is property(S) & Y is property(S) holds
[:X,Y:] is property(S)

proof end;

theorem Th62: :: YELLOW10:62

for S, T being non empty reflexive RelStr st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) & S is /\-complete holds
T is /\-complete

proof end;

registration

let S be non empty reflexive /\-complete RelStr ;

cluster RelStr(# the carrier of S, the InternalRel of S #) -> /\-complete ;

coherence
RelStr(# the carrier of S, the InternalRel of S #) is /\-complete by Th62;

end;

registration

let S, T be non empty reflexive /\-complete RelStr ;

cluster [:S,T:] -> /\-complete ;

coherence
[:S,T:] is /\-complete

proof end;

end;

theorem :: YELLOW10:63

for S, T being non empty reflexive RelStr st [:S,T:] is /\-complete holds
( S is /\-complete & T is /\-complete )

proof end;

registration

let S, T be non empty antisymmetric bounded complemented with_suprema with_infima RelStr ;

cluster [:S,T:] -> complemented ;

coherence
[:S,T:] is complemented

proof end;

end;

theorem :: YELLOW10:64

for S, T being antisymmetric bounded with_suprema with_infima RelStr st [:S,T:] is complemented holds
( S is complemented & T is complemented )

proof end;

registration

let S, T be non empty antisymmetric distributive with_suprema with_infima RelStr ;

cluster [:S,T:] -> distributive ;

coherence
[:S,T:] is distributive

proof end;

end;

theorem :: YELLOW10:65

for S being antisymmetric with_suprema with_infima RelStr
for T being reflexive antisymmetric with_suprema with_infima RelStr st [:S,T:] is distributive holds
S is distributive

proof end;

theorem :: YELLOW10:66

for S being reflexive antisymmetric with_suprema with_infima RelStr
for T being antisymmetric with_suprema with_infima RelStr st [:S,T:] is distributive holds
T is distributive

proof end;

registration

let S, T be meet-continuous Semilattice;

cluster [:S,T:] -> satisfying_MC ;

coherence
[:S,T:] is satisfying_MC

proof end;

end;

theorem :: YELLOW10:67

for S, T being Semilattice st [:S,T:] is meet-continuous holds
( S is meet-continuous & T is meet-continuous )

proof end;

registration

let S, T be non empty up-complete /\-complete satisfying_axiom_of_approximation Poset;

cluster [:S,T:] -> satisfying_axiom_of_approximation ;

coherence
[:S,T:] is satisfying_axiom_of_approximation

proof end;

end;

registration

let S, T be non empty /\-complete continuous Poset;

cluster [:S,T:] -> continuous ;

coherence
[:S,T:] is continuous ;

end;

theorem :: YELLOW10:68

for S, T being non empty lower-bounded up-complete Poset st [:S,T:] is continuous holds
( S is continuous & T is continuous )

proof end;

registration

let S, T be lower-bounded up-complete satisfying_axiom_K sup-Semilattice;

cluster [:S,T:] -> satisfying_axiom_K ;

coherence
[:S,T:] is satisfying_axiom_K

proof end;

end;

registration

let S, T be lower-bounded complete algebraic sup-Semilattice;

cluster [:S,T:] -> algebraic ;

coherence
[:S,T:] is algebraic ;

end;

theorem Th69: :: YELLOW10:69

for S, T being non empty lower-bounded Poset st [:S,T:] is algebraic holds
( S is algebraic & T is algebraic )

proof end;

registration

let S, T be lower-bounded arithmetic LATTICE;

cluster [:S,T:] -> arithmetic ;

coherence
[:S,T:] is arithmetic

proof end;

end;

theorem :: YELLOW10:70

for S, T being lower-bounded LATTICE st [:S,T:] is arithmetic holds
( S is arithmetic & T is arithmetic )

proof end;