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


begin

registration
let S, T be non empty upper-bounded RelStr ;
cluster[:S,T:] ->  upper-bounded ;
coherence
 [:S,T:] is upper-bounded
proofend;
end;

registration
let S, T be non empty lower-bounded RelStr ;
cluster[:S,T:] ->  lower-bounded ;
coherence
 [:S,T:] is lower-bounded
proofend;
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 )
proofend;

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

theorem Th3: :: YELLOW10:3
for S, T being non empty antisymmetric upper-bounded RelStr holds Top [:S,T:] = [(Top S),(Top T)]
proofend;

theorem Th4: :: YELLOW10:4
for S, T being non empty antisymmetric lower-bounded RelStr holds Bottom [:S,T:] = [(Bottom S),(Bottom T)]
proofend;

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

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

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)} &amp; x `2 is_<=_than {(y `2)} ) )
proofend;

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)} &amp; x `2 is_<=_than {(y `2),(z `2)} ) )
proofend;

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)} &amp; x `2 is_>=_than {(y `2)} ) )
proofend;

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)} &amp; x `2 is_>=_than {(y `2),(z `2)} ) )
proofend;

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 &amp; ex_inf_of {(x `2),(y `2)},T ) )
proofend;

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 &amp; ex_sup_of {(x `2),(y `2)},T ) )
proofend;

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) &amp; (x "/\" y) `2 = (x `2) "/\" (y `2) )
proofend;

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) &amp; (x "\/" y) `2 = (x `2) "\/" (y `2) )
proofend;

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]
proofend;

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]
proofend;

definition
let S be antisymmetric with_suprema with_infima RelStr ;
let x, y be Element of S;
:: original:is_a_complement_of
redefine predy is_a_complement_of x;
symmetry
 for y, x being Element of S st R54(S,b2,b1) holds
R54(S,b1,b2)
proofend;
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 &amp; x `2 is_a_complement_of y `2 ) )
proofend;

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 &amp; b << d )
proofend;

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 &amp; b << d ) )
proofend;

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 &amp; x `2 << y `2 )
proofend;

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 &amp; x `2 << y `2 ) )
proofend;

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 &amp; x `2 is compact )
proofend;

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 &amp; x `2 is compact holds
x is compact
proofend;

begin

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) &amp; proj2 (X "/\" Y) = (proj2 X) "/\" (proj2 Y) )
proofend;

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) &amp; proj2 (X "\/" Y) = (proj2 X) "\/" (proj2 Y) )
proofend;

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)):]
proofend;

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:]
proofend;

theorem Th28: :: YELLOW10:28
for S, T being RelStr
for X being Subset of [:S,T:] holds
( proj1 (downarrow X) c= downarrow (proj1 X) &amp; proj2 (downarrow X) c= downarrow (proj2 X) )
proofend;

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

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

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)):]
proofend;

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:]
proofend;

theorem Th33: :: YELLOW10:33
for S, T being RelStr
for X being Subset of [:S,T:] holds
( proj1 (uparrow X) c= uparrow (proj1 X) &amp; proj2 (uparrow X) c= uparrow (proj2 X) )
proofend;

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

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

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]
proofend;

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) &amp; proj2 (downarrow x) c= downarrow (x `2) )
proofend;

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

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

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]
proofend;

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) &amp; proj2 (uparrow x) c= uparrow (x `2) )
proofend;

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

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

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]
proofend;

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) &amp; proj2 (waybelow x) c= waybelow (x `2) )
proofend;

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

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

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]
proofend;

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) &amp; proj2 (wayabove x) c= wayabove (x `2) )
proofend;

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]
proofend;

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) &amp; proj2 (compactbelow x) c= compactbelow (x `2) )
proofend;

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

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

registration
let S be non empty reflexive RelStr ;
cluster empty  ->  Open for M2( bool the carrier of S);
coherence
 for b1 being Subset of S st b1 is empty holds
b1 is Open
proofend;
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 &amp; proj2 X is Open )
proofend;

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 &amp; Y is Open holds
[:X,Y:] is Open
proofend;

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 &amp; proj2 X is inaccessible )
proofend;

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 &amp; Y is inaccessible holds
[:X,Y:] is inaccessible
proofend;

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 ) &amp; ( X <> {} implies Y is directly_closed ) )
proofend;

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 &amp; Y is directly_closed holds
[:X,Y:] is directly_closed
proofend;

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) &amp; proj2 X is property(S) )
proofend;

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) &amp; Y is property(S) holds
[:X,Y:] is property(S)
proofend;

begin

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 #) &amp; S is /\-complete holds
T is /\-complete
proofend;

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
proofend;
end;

theorem :: YELLOW10:63
for S, T being non empty reflexive RelStr st [:S,T:] is /\-complete holds
( S is /\-complete &amp; T is /\-complete )
proofend;

registration
let S, T be non empty antisymmetric bounded complemented with_suprema with_infima RelStr ;
cluster[:S,T:] ->  complemented ;
coherence
 [:S,T:] is complemented
proofend;
end;

theorem :: YELLOW10:64
for S, T being antisymmetric bounded with_suprema with_infima RelStr st [:S,T:] is complemented holds
( S is complemented &amp; T is complemented )
proofend;

registration
let S, T be non empty antisymmetric distributive with_suprema with_infima RelStr ;
cluster[:S,T:] ->  distributive ;
coherence
 [:S,T:] is distributive
proofend;
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
proofend;

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

registration
let S, T be meet-continuous Semilattice;
cluster[:S,T:] ->  satisfying_MC ;
coherence
 [:S,T:] is satisfying_MC
proofend;
end;

theorem :: YELLOW10:67
for S, T being Semilattice st [:S,T:] is meet-continuous holds
( S is meet-continuous &amp; T is meet-continuous )
proofend;

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
proofend;
end;

registration
let S, T be non empty /\-complete continuous Poset;
cluster[:S,T:] ->  continuous ;
coherence
 [:S,T:] is continuous
proofend;
end;

theorem :: YELLOW10:68
for S, T being non empty lower-bounded up-complete Poset st [:S,T:] is continuous holds
( S is continuous &amp; T is continuous )
proofend;

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
proofend;
end;

registration
let S, T be lower-bounded complete algebraic sup-Semilattice;
cluster[:S,T:] ->  algebraic ;
coherence
 [:S,T:] is algebraic
proofend;
end;

theorem Th69: :: YELLOW10:69
for S, T being non empty lower-bounded Poset st [:S,T:] is algebraic holds
( S is algebraic &amp; T is algebraic )
proofend;

registration
let S, T be lower-bounded arithmetic LATTICE;
cluster[:S,T:] ->  arithmetic ;
coherence
 [:S,T:] is arithmetic
proofend;
end;

theorem :: YELLOW10:70
for S, T being lower-bounded LATTICE st [:S,T:] is arithmetic holds
( S is arithmetic &amp; T is arithmetic )
proofend;