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

registration
let L be RelStr ;
let X be empty Subset of L;
cluster downarrow X -> empty ;
coherence
downarrow X is empty
proof end;
cluster uparrow X -> empty ;
coherence
uparrow X is empty
proof end;
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):]
proof end;

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

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

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

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

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

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

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

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

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

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

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

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

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

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] & y = [s,t] & [p,s] in P & [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] & y = [s,t] & [p,s] in P & [q,t] in R ) )
proof end;
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] & y = [s,t] & [p,s] in P & [q,t] in R ) ) ) & ( for x, y being set holds
( [x,y] in b2 iff ex p, q, s, t being set st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) ) ) holds
b1 = b2
proof end;
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] & y = [s,t] & [p,s] in P & [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 & [((x `1) `2),((x `2) `2)] in R & ex a, b being set st x = [a,b] & ex c, d being set st x `1 = [c,d] & ex e, f being set st x `2 = [e,f] ) )
proof end;

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:]
proof end;
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:] & 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:] & the InternalRel of b1 = [" the InternalRel of X, the InternalRel of Y"] )
proof end;
uniqueness
for b1, b2 being strict RelStr st the carrier of b1 = [: the carrier of X, the carrier of Y:] & the InternalRel of b1 = [" the InternalRel of X, the InternalRel of Y"] & the carrier of b2 = [: the carrier of X, the carrier of Y:] & 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:] & 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
proof end;
:: original: proj2
redefine func proj2 D -> Subset of L2;
coherence
proj2 D is Subset of L2
proof end;
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:]
proof end;
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:]
proof end;
end;

definition
let L1, L2 be non empty RelStr ;
let x be Element of [:L1,L2:];
:: original: `1
redefine func x `1 -> Element of L1;
coherence
x `1 is Element of L1
proof end;
:: original: `2
redefine func x `2 -> Element of L2;
coherence
x `2 is Element of L2
proof end;
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 & b <= d ) iff [a,b] <= [c,d] )
proof end;

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 & x `2 <= y `2 ) )
proof end;

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

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

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

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

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

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

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

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

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

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

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

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

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

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:]
proof end;
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 & D2 is directed )
proof end;

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 & not proj2 D is empty )
proof end;

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 & proj2 D is directed )
proof end;

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:]
proof end;
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 & D2 is filtered )
proof end;

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 & proj2 D is filtered )
proof end;

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:]
proof end;
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 & D2 is upper )
proof end;

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 & proj2 D is upper )
proof end;

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:]
proof end;
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 & D2 is lower )
proof end;

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 & proj2 D is lower )
proof end;

definition
let R be RelStr ;
attr R 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
proof end;
end;

registration
cluster non empty strict V55() reflexive transitive antisymmetric non void for RelStr ;
existence
ex b1 being Poset st
( not b1 is void & not b1 is empty & b1 is strict )
proof end;
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 & b1 is reflexive holds
not b1 is void
proof end;
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 & y is_>=_than D2 )
proof end;

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 & y is_>=_than D2 holds
[x,y] is_>=_than [:D1,D2:]
proof end;

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 & y is_>=_than proj2 D ) )
proof end;

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 & y is_<=_than D2 )
proof end;

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 & y is_<=_than D2 holds
[x,y] is_<=_than [:D1,D2:]
proof end;

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 & y is_<=_than proj2 D ) )
proof end;

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 & ex_sup_of D2,S2 & ( 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 ) & ( for d being Element of S2 st d is_>=_than D2 holds
y <= d ) )
proof end;

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 & ex_inf_of D2,S2 & ( 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 ) & ( for d being Element of S2 st d is_<=_than D2 holds
y >= d ) )
proof end;

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

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

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 & ex_sup_of D2,S2 ) iff ex_sup_of [:D1,D2:],[:S1,S2:] )
proof end;

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 & ex_inf_of D2,S2 ) iff ex_inf_of [:D1,D2:],[:S1,S2:] )
proof end;

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 & ex_sup_of proj2 D,S2 ) iff ex_sup_of D,[:S1,S2:] )
proof end;

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 & ex_inf_of proj2 D,S2 ) iff ex_inf_of D,[:S1,S2:] )
proof end;

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 & ex_sup_of D2,S2 holds
sup [:D1,D2:] = [(sup D1),(sup D2)]
proof end;

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 & ex_inf_of D2,S2 holds
inf [:D1,D2:] = [(inf D1),(inf D2)]
proof end;

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

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

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))]
proof end;

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))]
proof end;

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

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

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