Journal of Formalized Mathematics
Volume 8, 1996
University of Bialystok
Copyright (c) 1996 Association of Mizar Users

### Cartesian Products of Relations and Relational Structures

by
Artur Kornilowicz

MML identifier: YELLOW_3
[ Mizar article, MML identifier index ]

```environ

vocabulary RELAT_1, FUNCT_5, ORDERS_1, WAYBEL_0, MCART_1, LATTICE3, RELAT_2,
LATTICES, YELLOW_0, BHSP_3, ORDINAL2, PRE_TOPC, FUNCT_1, TARSKI,
QUANTAL1, AMI_1, YELLOW_3;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2, RELSET_1,
FUNCT_1, MCART_1, DOMAIN_1, FUNCT_2, PRE_TOPC, FUNCT_5, STRUCT_0,
ORDERS_1, LATTICE3, YELLOW_0, WAYBEL_0;
constructors LATTICE3, DOMAIN_1, ORDERS_3, YELLOW_2, PRE_TOPC;
clusters LATTICE3, STRUCT_0, ORDERS_3, RELSET_1, WAYBEL_0, YELLOW_0, SUBSET_1,
XBOOLE_0;
requirements SUBSET, BOOLE;

begin :: Preliminaries

scheme FraenkelA2 {A() -> non empty set,
F(set, set) -> set,
P[set, set], Q[set, set] } :
{ F(s,t) where s is Element of A(), t is Element of A() : P[s,t] }
is Subset of A()
provided
for s being Element of A(), t being Element of A() holds F(s,t) in A();

scheme ExtensionalityR { A, B() -> Relation,
P[set,set] }:
A() = B()
provided
for a, b being set holds [a,b] in A() iff P[a,b] and
for a, b being set holds [a,b] in B() iff P[a,b];

definition let X be empty set;
cluster proj1 X -> empty;
cluster proj2 X -> empty;
end;

definition let X, Y be non empty set,
D be non empty Subset of [:X,Y:];
cluster proj1 D -> non empty;
cluster proj2 D -> non empty;
end;

definition let L be RelStr,
X be empty Subset of L;
cluster downarrow X -> empty;

cluster uparrow X -> empty;
end;

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

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

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

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

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

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

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

theorem :: YELLOW_3:8
for S, T being with_infima Poset, f being map 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;

theorem :: YELLOW_3:9
for S, T being with_suprema Poset, f being map 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;

scheme Inf_Union { L() -> complete antisymmetric (non empty RelStr),
P[set] } :
"/\" ({ "/\"(X,L()) where X is Subset of L(): P[X] },L())
>= "/\" (union {X where X is Subset of L(): P[X]},L());

scheme Inf_of_Infs { L() -> complete LATTICE,
P[set] } :
"/\" ({ "/\"(X,L()) where X is Subset of L(): P[X] },L())
= "/\" (union {X where X is Subset of L(): P[X]},L());

scheme Sup_Union { L() -> complete antisymmetric (non empty RelStr),
P[set] } :
"\/" ({ "\/"(X,L()) where X is Subset of L(): P[X] },L())
<= "\/" (union {X where X is Subset of L(): P[X]},L());

scheme Sup_of_Sups { L() -> complete LATTICE,
P[set] } :
"\/" ({ "\/"(X,L()) where X is Subset of L(): P[X] },L())
= "\/" (union {X where X is Subset of L(): P[X]},L());

begin :: Properties of Cartesian Products of Relational Structures

definition let P, R be Relation;
func ["P,R"] -> Relation means
:: 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;
end;

theorem :: YELLOW_3:10
for P, R being Relation, 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];

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

definition let X, Y be RelStr;
func [:X,Y:] -> strict RelStr means
:: 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"];
end;

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

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

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

definition let L1, L2 be non empty RelStr,
x be Element of [:L1,L2:];
redefine func x`1 -> Element of L1;
redefine func x`2 -> Element of L2;
end;

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

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

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

definition let X, Y be non empty RelStr;
cluster [:X,Y:] -> non empty;
end;

definition let X, Y be reflexive RelStr;
cluster [:X,Y:] -> reflexive;
end;

definition let X, Y be antisymmetric RelStr;
cluster [:X,Y:] -> antisymmetric;
end;

definition let X, Y be transitive RelStr;
cluster [:X,Y:] -> transitive;
end;

definition let X, Y be with_suprema RelStr;
cluster [:X,Y:] -> with_suprema;
end;

definition let X, Y be with_infima RelStr;
cluster [:X,Y:] -> with_infima;
end;

theorem :: YELLOW_3:14
for X, Y being RelStr st [:X,Y:] is non empty
holds X is non empty & Y is non empty;

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

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

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

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;

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;

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

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

theorem :: YELLOW_3:21
for S1, S2 being non empty RelStr
for D being non empty Subset of [:S1,S2:]
holds proj1 D is non empty & proj2 D is non empty;

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;

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

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

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;

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

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

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;

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

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

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;

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

definition
cluster empty -> void RelStr;
end;

definition
cluster non void non empty strict Poset;
end;

definition
cluster non void -> non empty RelStr;
end;

definition
cluster non empty reflexive -> non void RelStr;
end;

definition let R be non void RelStr;
cluster the InternalRel of R -> non empty;
end;

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

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

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

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

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

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

theorem :: YELLOW_3:35
for S1, S2 being antisymmetric non empty RelStr
for D1 being Subset of S1, D2 being Subset of S2
for x being Element of S1, 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;

theorem :: YELLOW_3:36
for S1, S2 being antisymmetric non empty RelStr
for D1 being Subset of S1, D2 being Subset of S2
for x being Element of S1, 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;

theorem :: YELLOW_3:37
for S1, S2 being antisymmetric non empty RelStr
for D1 being non empty Subset of S1, D2 being non empty Subset of S2
for x being Element of S1, 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;

theorem :: YELLOW_3:38
for S1, S2 being antisymmetric non empty RelStr
for D1 being non empty Subset of S1, D2 being non empty Subset of S2
for x being Element of S1, 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;

theorem :: YELLOW_3:39
for S1, S2 being antisymmetric non empty RelStr
for D1 being non empty Subset of S1, 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:];

theorem :: YELLOW_3:40
for S1, S2 being antisymmetric non empty RelStr
for D1 being non empty Subset of S1, 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:];

theorem :: YELLOW_3:41
for S1, S2 being antisymmetric non empty 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:];

theorem :: YELLOW_3:42
for S1, S2 being antisymmetric non empty 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:];

theorem :: YELLOW_3:43
for S1, S2 being antisymmetric non empty RelStr
for D1 being non empty Subset of S1, 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];

theorem :: YELLOW_3:44
for S1, S2 being antisymmetric non empty RelStr
for D1 being non empty Subset of S1, 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];

definition let X, Y be complete antisymmetric (non empty RelStr);
cluster [:X,Y:] -> complete;
end;

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

theorem :: YELLOW_3:46
for L1,L2 being antisymmetric non empty 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];

theorem :: YELLOW_3:47
for L1,L2 being antisymmetric non empty 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];

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;

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;

scheme Kappa2DS { X,Y,Z() -> non empty RelStr,
F(set,set) -> set }:
ex f being map of [:X(),Y():], Z()
st for x being Element of X(), y being Element of Y() holds f.[x,y]=F(x,y)
provided
for x being Element of X(), y being Element of Y() holds
F(x,y) is Element of Z();
```