:: Cartesian Products of Relations and Relational Structures
:: by Artur Korni{\l}owicz
::
:: Received September 25, 1996
:: Copyright (c) 1996-2012 Association of Mizar Users


begin

scheme :: YELLOW_3:sch 1
FraenkelA2{ F1() ->  non empty set , F2( set , set ) ->  set , P1[ set , set ], P2[ set , set ] } :
  {  F2(s,t) where s, t is Element of F1() : P1[s,t]  }  is Subset of F1()
provided
A1: for s, t being Element of F1() holds F2(s,t) in F1()
proofend;

registration
let L be RelStr ;
let X be empty Subset of L;
cluster downarrow X ->  empty ;
coherence
 downarrow X is empty
proofend;
cluster uparrow X ->  empty ;
coherence
 uparrow X is empty
proofend;
end;

theorem Th1: :: YELLOW_3:1
for X, Y being set
for D being Subset of [:X,Y:] holds D c= [:(proj1 D),(proj2 D):]
proofend;

Lm1:  for x, a1, a2, b1, b2 being set st x = [[a1,a2],[b1,b2]] holds
( (x `1) `1 = a1 & (x `1) `2 = a2 & (x `2) `1 = b1 & (x `2) `2 = b2 )
proofend;

theorem :: YELLOW_3:2
for L being transitive antisymmetric with_infima RelStr
for a, b, c, d being Element of L st a <= c &amp; b <= d holds
a "/\" b <= c "/\" d
proofend;

theorem :: YELLOW_3:3
for L being transitive antisymmetric with_suprema RelStr
for a, b, c, d being Element of L st a <= c &amp; b <= d holds
a "\/" b <= c "\/" d
proofend;

theorem :: YELLOW_3:4
for L being non empty reflexive antisymmetric complete RelStr
for D being Subset of L
for x being Element of L st x in D holds
(sup D) "/\" x = x
proofend;

theorem :: YELLOW_3:5
for L being non empty reflexive antisymmetric complete RelStr
for D being Subset of L
for x being Element of L st x in D holds
(inf D) "\/" x = x
proofend;

theorem :: YELLOW_3:6
for L being RelStr
for X, Y being Subset of L st X c= Y holds
downarrow X c= downarrow Y
proofend;

theorem :: YELLOW_3:7
for L being RelStr
for X, Y being Subset of L st X c= Y holds
uparrow X c= uparrow Y
proofend;

theorem :: YELLOW_3:8
for S, T being with_infima Poset
for f being Function of S,T
for x, y being Element of S holds
( f preserves_inf_of {x,y} iff f . (x "/\" y) = (f . x) "/\" (f . y) )
proofend;

theorem :: YELLOW_3:9
for S, T being with_suprema Poset
for f being Function of S,T
for x, y being Element of S holds
( f preserves_sup_of {x,y} iff f . (x "\/" y) = (f . x) "\/" (f . y) )
proofend;

scheme :: YELLOW_3:sch 2
InfUnion{ F1() ->  non empty antisymmetric complete RelStr , P1[ set ] } :
 "/\" ( {  ("/\" (X,F1())) where X is Subset of F1() : P1[X]  }  ,F1()) >= "/\" ((union  {  X where X is Subset of F1() : P1[X]  }  ),F1())
proofend;

scheme :: YELLOW_3:sch 3
InfofInfs{ F1() ->  complete LATTICE, P1[ set ] } :
 "/\" ( {  ("/\" (X,F1())) where X is Subset of F1() : P1[X]  }  ,F1()) = "/\" ((union  {  X where X is Subset of F1() : P1[X]  }  ),F1())
proofend;

scheme :: YELLOW_3:sch 4
SupUnion{ F1() ->  non empty antisymmetric complete RelStr , P1[ set ] } :
 "\/" ( {  ("\/" (X,F1())) where X is Subset of F1() : P1[X]  }  ,F1()) <= "\/" ((union  {  X where X is Subset of F1() : P1[X]  }  ),F1())
proofend;

scheme :: YELLOW_3:sch 5
SupofSups{ F1() ->  complete LATTICE, P1[ set ] } :
 "\/" ( {  ("\/" (X,F1())) where X is Subset of F1() : P1[X]  }  ,F1()) = "\/" ((union  {  X where X is Subset of F1() : P1[X]  }  ),F1())
proofend;

begin

definition
let P, R be Relation;
func["P,R"] ->  Relation means :Def1: :: YELLOW_3:def 1
 for x, y being set holds
( [x,y] in it iff ex p, q, s, t being set st
( x = [p,q] &amp; y = [s,t] &amp; [p,s] in P &amp; [q,t] in R ) );
existence
 ex b1 being Relation st
for x, y being set holds
( [x,y] in b1 iff ex p, q, s, t being set st
( x = [p,q] &amp; y = [s,t] &amp; [p,s] in P &amp; [q,t] in R ) )
proofend;
uniqueness
 for b1, b2 being Relation st ( for x, y being set holds
( [x,y] in b1 iff ex p, q, s, t being set st
( x = [p,q] &amp; y = [s,t] &amp; [p,s] in P &amp; [q,t] in R ) ) ) &amp; ( for x, y being set holds
( [x,y] in b2 iff ex p, q, s, t being set st
( x = [p,q] &amp; y = [s,t] &amp; [p,s] in P &amp; [q,t] in R ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines [" YELLOW_3:def_1_:_
 for P, R, b3 being Relation holds
( b3 = ["P,R"] iff for x, y being set holds
( [x,y] in b3 iff ex p, q, s, t being set st
( x = [p,q] &amp; y = [s,t] &amp; [p,s] in P &amp; [q,t] in R ) ) );

theorem Th10: :: YELLOW_3:10
for P, R being Relation
for x being set holds
( x in ["P,R"] iff ( [((x `1) `1),((x `2) `1)] in P &amp; [((x `1) `2),((x `2) `2)] in R &amp; ex a, b being set st x = [a,b] &amp; ex c, d being set st x `1 = [c,d] &amp; ex e, f being set st x `2 = [e,f] ) )
proofend;

definition
let A, B, X, Y be set ;
let P be Relation of A,B;
let R be Relation of X,Y;
:: original:["
redefine func["P,R"] ->  Relation of [:A,X:],[:B,Y:];
coherence
 ["P,R"] is Relation of [:A,X:],[:B,Y:]
proofend;
end;

definition
let X, Y be RelStr ;
func[:X,Y:] ->  strict RelStr  means :Def2: :: YELLOW_3:def 2
( the carrier of it = [: the carrier of X, the carrier of Y:] &amp; the InternalRel of it = [" the InternalRel of X, the InternalRel of Y"] );
existence
 ex b1 being strict RelStr st
( the carrier of b1 = [: the carrier of X, the carrier of Y:] &amp; the InternalRel of b1 = [" the InternalRel of X, the InternalRel of Y"] )
proofend;
uniqueness
 for b1, b2 being strict RelStr st the carrier of b1 = [: the carrier of X, the carrier of Y:] &amp; the InternalRel of b1 = [" the InternalRel of X, the InternalRel of Y"] &amp; the carrier of b2 = [: the carrier of X, the carrier of Y:] &amp; the InternalRel of b2 = [" the InternalRel of X, the InternalRel of Y"] holds
b1 = b2 ;
end;

:: deftheorem Def2 defines [: YELLOW_3:def_2_:_
 for X, Y being RelStr
for b3 being strict RelStr holds
( b3 = [:X,Y:] iff ( the carrier of b3 = [: the carrier of X, the carrier of Y:] &amp; the InternalRel of b3 = [" the InternalRel of X, the InternalRel of Y"] ) );

definition
let L1, L2 be RelStr ;
let D be Subset of [:L1,L2:];
:: original:proj1
redefine func proj1 D ->  Subset of L1;
coherence
 proj1 D is Subset of L1
proofend;
:: original:proj2
redefine func proj2 D ->  Subset of L2;
coherence
 proj2 D is Subset of L2
proofend;
end;

definition
let S1, S2 be RelStr ;
let D1 be Subset of S1;
let D2 be Subset of S2;
:: original:[:
redefine func[:D1,D2:] ->  Subset of [:S1,S2:];
coherence
 [:D1,D2:] is Subset of [:S1,S2:]
proofend;
end;

definition
let S1, S2 be non empty RelStr ;
let x be Element of S1;
let y be Element of S2;
:: original:[
redefine func[x,y] ->  Element of [:S1,S2:];
coherence
 [x,y] is Element of [:S1,S2:]
proofend;
end;

definition
let L1, L2 be non empty RelStr ;
let x be Element of [:L1,L2:];
:: original:`1
redefine funcx `1  ->  Element of L1;
coherence
 x `1 is Element of L1
proofend;
:: original:`2
redefine funcx `2  ->  Element of L2;
coherence
 x `2 is Element of L2
proofend;
end;

theorem Th11: :: YELLOW_3:11
for S1, S2 being non empty RelStr
for a, c being Element of S1
for b, d being Element of S2 holds
( ( a <= c &amp; b <= d ) iff [a,b] <= [c,d] )
proofend;

theorem Th12: :: YELLOW_3:12
for S1, S2 being non empty RelStr
for x, y being Element of [:S1,S2:] holds
( x <= y iff ( x `1 <= y `1 &amp; x `2 <= y `2 ) )
proofend;

theorem :: YELLOW_3:13
for A, B being RelStr
for C being non empty RelStr
for f, g being Function of [:A,B:],C st ( for x being Element of A
for y being Element of B holds f . (x,y) = g . (x,y) ) holds
f = g
proofend;

registration
let X, Y be non empty RelStr ;
cluster[:X,Y:] ->  non empty strict ;
coherence
 not [:X,Y:] is empty
proofend;
end;

registration
let X, Y be reflexive RelStr ;
cluster[:X,Y:] ->  strict reflexive ;
coherence
 [:X,Y:] is reflexive
proofend;
end;

registration
let X, Y be antisymmetric RelStr ;
cluster[:X,Y:] ->  strict antisymmetric ;
coherence
 [:X,Y:] is antisymmetric
proofend;
end;

registration
let X, Y be transitive RelStr ;
cluster[:X,Y:] ->  strict transitive ;
coherence
 [:X,Y:] is transitive
proofend;
end;

registration
let X, Y be with_suprema RelStr ;
cluster[:X,Y:] ->  strict with_suprema ;
coherence
 [:X,Y:] is with_suprema
proofend;
end;

registration
let X, Y be with_infima RelStr ;
cluster[:X,Y:] ->  strict with_infima ;
coherence
 [:X,Y:] is with_infima
proofend;
end;

theorem :: YELLOW_3:14
for X, Y being RelStr st not [:X,Y:] is empty holds
( not X is empty &amp; not Y is empty )
proofend;

theorem :: YELLOW_3:15
for X, Y being non empty RelStr st [:X,Y:] is reflexive holds
( X is reflexive &amp; Y is reflexive )
proofend;

theorem :: YELLOW_3:16
for X, Y being non empty reflexive RelStr st [:X,Y:] is antisymmetric holds
( X is antisymmetric &amp; Y is antisymmetric )
proofend;

theorem :: YELLOW_3:17
for X, Y being non empty reflexive RelStr st [:X,Y:] is transitive holds
( X is transitive &amp; Y is transitive )
proofend;

theorem :: YELLOW_3:18
for X, Y being non empty reflexive RelStr st [:X,Y:] is with_suprema holds
( X is with_suprema &amp; Y is with_suprema )
proofend;

theorem :: YELLOW_3:19
for X, Y being non empty reflexive RelStr st [:X,Y:] is with_infima holds
( X is with_infima &amp; Y is with_infima )
proofend;

definition
let S1, S2 be RelStr ;
let D1 be directed Subset of S1;
let D2 be directed Subset of S2;
:: original:[:
redefine func[:D1,D2:] ->  directed Subset of [:S1,S2:];
coherence
 [:D1,D2:] is directed Subset of [:S1,S2:]
proofend;
end;

theorem :: YELLOW_3:20
for S1, S2 being non empty RelStr
for D1 being non empty Subset of S1
for D2 being non empty Subset of S2 st [:D1,D2:] is directed holds
( D1 is directed &amp; D2 is directed )
proofend;

theorem Th21: :: YELLOW_3:21
for S1, S2 being non empty RelStr
for D being non empty Subset of [:S1,S2:] holds
( not proj1 D is empty &amp; not proj2 D is empty )
proofend;

theorem :: YELLOW_3:22
for S1, S2 being non empty reflexive RelStr
for D being non empty directed Subset of [:S1,S2:] holds
( proj1 D is directed &amp; proj2 D is directed )
proofend;

definition
let S1, S2 be RelStr ;
let D1 be filtered Subset of S1;
let D2 be filtered Subset of S2;
:: original:[:
redefine func[:D1,D2:] ->  filtered Subset of [:S1,S2:];
coherence
 [:D1,D2:] is filtered Subset of [:S1,S2:]
proofend;
end;

theorem :: YELLOW_3:23
for S1, S2 being non empty RelStr
for D1 being non empty Subset of S1
for D2 being non empty Subset of S2 st [:D1,D2:] is filtered holds
( D1 is filtered &amp; D2 is filtered )
proofend;

theorem :: YELLOW_3:24
for S1, S2 being non empty reflexive RelStr
for D being non empty filtered Subset of [:S1,S2:] holds
( proj1 D is filtered &amp; proj2 D is filtered )
proofend;

definition
let S1, S2 be RelStr ;
let D1 be upper Subset of S1;
let D2 be upper Subset of S2;
:: original:[:
redefine func[:D1,D2:] ->  upper Subset of [:S1,S2:];
coherence
 [:D1,D2:] is upper Subset of [:S1,S2:]
proofend;
end;

theorem :: YELLOW_3:25
for S1, S2 being non empty reflexive RelStr
for D1 being non empty Subset of S1
for D2 being non empty Subset of S2 st [:D1,D2:] is upper holds
( D1 is upper &amp; D2 is upper )
proofend;

theorem :: YELLOW_3:26
for S1, S2 being non empty reflexive RelStr
for D being non empty upper Subset of [:S1,S2:] holds
( proj1 D is upper &amp; proj2 D is upper )
proofend;

definition
let S1, S2 be RelStr ;
let D1 be lower Subset of S1;
let D2 be lower Subset of S2;
:: original:[:
redefine func[:D1,D2:] ->  lower Subset of [:S1,S2:];
coherence
 [:D1,D2:] is lower Subset of [:S1,S2:]
proofend;
end;

theorem :: YELLOW_3:27
for S1, S2 being non empty reflexive RelStr
for D1 being non empty Subset of S1
for D2 being non empty Subset of S2 st [:D1,D2:] is lower holds
( D1 is lower &amp; D2 is lower )
proofend;

theorem :: YELLOW_3:28
for S1, S2 being non empty reflexive RelStr
for D being non empty lower Subset of [:S1,S2:] holds
( proj1 D is lower &amp; proj2 D is lower )
proofend;

definition
let R be RelStr ;
attrR is void  means :Def3: :: YELLOW_3:def 3
 the InternalRel of R is empty ;
end;

:: deftheorem Def3 defines void YELLOW_3:def_3_:_
 for R being RelStr holds
( R is void iff the InternalRel of R is empty );

registration
cluster empty  ->  void for RelStr ;
coherence
 for b1 being RelStr st b1 is empty holds
b1 is void
proofend;
end;

registration
cluster non empty strict V55() reflexive transitive antisymmetric non void for RelStr ;
existence
 ex b1 being Poset st
( not b1 is void &amp; not b1 is empty &amp; b1 is strict )
proofend;
end;

registration
cluster non void  ->  non empty for RelStr ;
coherence
 for b1 being RelStr st not b1 is void holds
not b1 is empty ;
end;

registration
cluster non empty reflexive  ->  non void for RelStr ;
coherence
 for b1 being RelStr st not b1 is empty &amp; b1 is reflexive holds
not b1 is void
proofend;
end;

registration
let R be non void RelStr ;
cluster the InternalRel of R ->  non empty ;
coherence
 not the InternalRel of R is empty by Def3;
end;

theorem Th29: :: YELLOW_3:29
for S1, S2 being non empty RelStr
for D1 being non empty Subset of S1
for D2 being non empty Subset of S2
for x being Element of S1
for y being Element of S2 st [x,y] is_>=_than [:D1,D2:] holds
( x is_>=_than D1 &amp; y is_>=_than D2 )
proofend;

theorem Th30: :: YELLOW_3:30
for S1, S2 being non empty RelStr
for D1 being Subset of S1
for D2 being Subset of S2
for x being Element of S1
for y being Element of S2 st x is_>=_than D1 &amp; y is_>=_than D2 holds
[x,y] is_>=_than [:D1,D2:]
proofend;

theorem Th31: :: YELLOW_3:31
for S1, S2 being non empty RelStr
for D being Subset of [:S1,S2:]
for x being Element of S1
for y being Element of S2 holds
( [x,y] is_>=_than D iff ( x is_>=_than proj1 D &amp; y is_>=_than proj2 D ) )
proofend;

theorem Th32: :: YELLOW_3:32
for S1, S2 being non empty RelStr
for D1 being non empty Subset of S1
for D2 being non empty Subset of S2
for x being Element of S1
for y being Element of S2 st [x,y] is_<=_than [:D1,D2:] holds
( x is_<=_than D1 &amp; y is_<=_than D2 )
proofend;

theorem Th33: :: YELLOW_3:33
for S1, S2 being non empty RelStr
for D1 being Subset of S1
for D2 being Subset of S2
for x being Element of S1
for y being Element of S2 st x is_<=_than D1 &amp; y is_<=_than D2 holds
[x,y] is_<=_than [:D1,D2:]
proofend;

theorem Th34: :: YELLOW_3:34
for S1, S2 being non empty RelStr
for D being Subset of [:S1,S2:]
for x being Element of S1
for y being Element of S2 holds
( [x,y] is_<=_than D iff ( x is_<=_than proj1 D &amp; y is_<=_than proj2 D ) )
proofend;

theorem Th35: :: YELLOW_3:35
for S1, S2 being non empty antisymmetric RelStr
for D1 being Subset of S1
for D2 being Subset of S2
for x being Element of S1
for y being Element of S2 st ex_sup_of D1,S1 &amp; ex_sup_of D2,S2 &amp; ( for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds
[x,y] <= b ) holds
( ( for c being Element of S1 st c is_>=_than D1 holds
x <= c ) &amp; ( for d being Element of S2 st d is_>=_than D2 holds
y <= d ) )
proofend;

theorem Th36: :: YELLOW_3:36
for S1, S2 being non empty antisymmetric RelStr
for D1 being Subset of S1
for D2 being Subset of S2
for x being Element of S1
for y being Element of S2 st ex_inf_of D1,S1 &amp; ex_inf_of D2,S2 &amp; ( for b being Element of [:S1,S2:] st b is_<=_than [:D1,D2:] holds
[x,y] >= b ) holds
( ( for c being Element of S1 st c is_<=_than D1 holds
x >= c ) &amp; ( for d being Element of S2 st d is_<=_than D2 holds
y >= d ) )
proofend;

theorem :: YELLOW_3:37
for S1, S2 being non empty antisymmetric RelStr
for D1 being non empty Subset of S1
for D2 being non empty Subset of S2
for x being Element of S1
for y being Element of S2 st ( for c being Element of S1 st c is_>=_than D1 holds
x <= c ) &amp; ( for d being Element of S2 st d is_>=_than D2 holds
y <= d ) holds
for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds
[x,y] <= b
proofend;

theorem :: YELLOW_3:38
for S1, S2 being non empty antisymmetric RelStr
for D1 being non empty Subset of S1
for D2 being non empty Subset of S2
for x being Element of S1
for y being Element of S2 st ( for c being Element of S1 st c is_>=_than D1 holds
x >= c ) &amp; ( for d being Element of S2 st d is_>=_than D2 holds
y >= d ) holds
for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds
[x,y] >= b
proofend;

theorem Th39: :: YELLOW_3:39
for S1, S2 being non empty antisymmetric RelStr
for D1 being non empty Subset of S1
for D2 being non empty Subset of S2 holds
( ( ex_sup_of D1,S1 &amp; ex_sup_of D2,S2 ) iff ex_sup_of [:D1,D2:],[:S1,S2:] )
proofend;

theorem Th40: :: YELLOW_3:40
for S1, S2 being non empty antisymmetric RelStr
for D1 being non empty Subset of S1
for D2 being non empty Subset of S2 holds
( ( ex_inf_of D1,S1 &amp; ex_inf_of D2,S2 ) iff ex_inf_of [:D1,D2:],[:S1,S2:] )
proofend;

theorem Th41: :: YELLOW_3:41
for S1, S2 being non empty antisymmetric RelStr
for D being Subset of [:S1,S2:] holds
( ( ex_sup_of proj1 D,S1 &amp; ex_sup_of proj2 D,S2 ) iff ex_sup_of D,[:S1,S2:] )
proofend;

theorem Th42: :: YELLOW_3:42
for S1, S2 being non empty antisymmetric RelStr
for D being Subset of [:S1,S2:] holds
( ( ex_inf_of proj1 D,S1 &amp; ex_inf_of proj2 D,S2 ) iff ex_inf_of D,[:S1,S2:] )
proofend;

theorem Th43: :: YELLOW_3:43
for S1, S2 being non empty antisymmetric RelStr
for D1 being non empty Subset of S1
for D2 being non empty Subset of S2 st ex_sup_of D1,S1 &amp; ex_sup_of D2,S2 holds
sup [:D1,D2:] = [(sup D1),(sup D2)]
proofend;

theorem Th44: :: YELLOW_3:44
for S1, S2 being non empty antisymmetric RelStr
for D1 being non empty Subset of S1
for D2 being non empty Subset of S2 st ex_inf_of D1,S1 &amp; ex_inf_of D2,S2 holds
inf [:D1,D2:] = [(inf D1),(inf D2)]
proofend;

registration
let X, Y be non empty antisymmetric complete RelStr ;
cluster[:X,Y:] ->  strict complete ;
coherence
 [:X,Y:] is complete
proofend;
end;

theorem :: YELLOW_3:45
for X, Y being non empty antisymmetric lower-bounded RelStr st [:X,Y:] is complete holds
( X is complete &amp; Y is complete )
proofend;

theorem :: YELLOW_3:46
for L1, L2 being non empty antisymmetric RelStr
for D being non empty Subset of [:L1,L2:] st ( [:L1,L2:] is complete or ex_sup_of D,[:L1,L2:] ) holds
sup D = [(sup (proj1 D)),(sup (proj2 D))]
proofend;

theorem :: YELLOW_3:47
for L1, L2 being non empty antisymmetric RelStr
for D being non empty Subset of [:L1,L2:] st ( [:L1,L2:] is complete or ex_inf_of D,[:L1,L2:] ) holds
inf D = [(inf (proj1 D)),(inf (proj2 D))]
proofend;

theorem :: YELLOW_3:48
for S1, S2 being non empty reflexive RelStr
for D being non empty directed Subset of [:S1,S2:] holds [:(proj1 D),(proj2 D):] c= downarrow D
proofend;

theorem :: YELLOW_3:49
for S1, S2 being non empty reflexive RelStr
for D being non empty filtered Subset of [:S1,S2:] holds [:(proj1 D),(proj2 D):] c= uparrow D
proofend;

scheme :: YELLOW_3:sch 6
Kappa2DS{ F1() ->  non empty RelStr , F2() ->  non empty RelStr , F3() ->  non empty RelStr , F4( set , set ) ->  set } :
 ex f being Function of [:F1(),F2():],F3() st
for x being Element of F1()
for y being Element of F2() holds f . (x,y) = F4(x,y)
provided
A1: for x being Element of F1()
for y being Element of F2() holds F4(x,y) is Element of F3()
proofend;