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

begin

scheme :: YELLOW_3:sch 1
FraenkelA2{ F₁() -> non empty set , F₂( set , set ) -> set , P₁[ set , set ], P₂[ set , set ] } :

{ F₂(s,t) where s, t is Element of F₁() : P₁[s,t] } is Subset of F₁()

provided

A1: for s, t being Element of F₁() holds F₂(s,t) in F₁()

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{ F₁() -> non empty antisymmetric complete RelStr , P₁[ set ] } :

"/\" ( { ("/\" (X,F₁())) where X is Subset of F₁() : P₁[X] } ,F₁()) >= "/\" ((union { X where X is Subset of F₁() : P₁[X] } ),F₁())

proof end;

scheme :: YELLOW_3:sch 3
InfofInfs{ F₁() -> complete LATTICE, P₁[ set ] } :

"/\" ( { ("/\" (X,F₁())) where X is Subset of F₁() : P₁[X] } ,F₁()) = "/\" ((union { X where X is Subset of F₁() : P₁[X] } ),F₁())

proof end;

scheme :: YELLOW_3:sch 4
SupUnion{ F₁() -> non empty antisymmetric complete RelStr , P₁[ set ] } :

"\/" ( { ("\/" (X,F₁())) where X is Subset of F₁() : P₁[X] } ,F₁()) <= "\/" ((union { X where X is Subset of F₁() : P₁[X] } ),F₁())

proof end;

scheme :: YELLOW_3:sch 5
SupofSups{ F₁() -> complete LATTICE, P₁[ set ] } :

"\/" ( { ("\/" (X,F₁())) where X is Subset of F₁() : P₁[X] } ,F₁()) = "\/" ((union { X where X is Subset of F₁() : P₁[X] } ),F₁())

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 b₁ being Relation st
for x, y being set holds
( [x,y] in b₁ 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 b₁, b₂ being Relation st ( for x, y being set holds
( [x,y] in b₁ 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 b₂ iff ex p, q, s, t being set st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines [" YELLOW_3:def 1 :
for P, R, b₃ being Relation holds
( b₃ = ["P,R"] iff for x, y being set holds
( [x,y] in b₃ 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 b₁ being strict RelStr st
( the carrier of b₁ = [: the carrier of X, the carrier of Y:] & the InternalRel of b₁ = [" the InternalRel of X, the InternalRel of Y"] )

proof end;

uniqueness
for b₁, b₂ being strict RelStr st the carrier of b₁ = [: the carrier of X, the carrier of Y:] & the InternalRel of b₁ = [" the InternalRel of X, the InternalRel of Y"] & the carrier of b₂ = [: the carrier of X, the carrier of Y:] & the InternalRel of b₂ = [" the InternalRel of X, the InternalRel of Y"] holds
b₁ = b₂ ;

end;

:: deftheorem Def2 defines [: YELLOW_3:def 2 :
for X, Y being RelStr
for b₃ being strict RelStr holds
( b₃ = [:X,Y:] iff ( the carrier of b₃ = [: the carrier of X, the carrier of Y:] & the InternalRel of b₃ = [" 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 RelStr ;
coherence
for b₁ being RelStr st b₁ is empty holds
b₁ is void

proof end;

end;

registration

cluster non empty strict V48() reflexive transitive antisymmetric non void RelStr ;
existence
ex b₁ being Poset st
( not b₁ is void & not b₁ is empty & b₁ is strict )

proof end;

end;

registration

cluster non void -> non empty RelStr ;
coherence
for b₁ being RelStr st not b₁ is void holds
not b₁ is empty ;

end;

registration

cluster non empty reflexive -> non void RelStr ;
coherence
for b₁ being RelStr st not b₁ is empty & b₁ is reflexive holds
not b₁ 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{ F₁() -> non empty RelStr , F₂() -> non empty RelStr , F₃() -> non empty RelStr , F₄( set , set ) -> set } :

ex f being Function of [:F₁(),F₂():],F₃() st
for x being Element of F₁()
for y being Element of F₂() holds f . (x,y) = F₄(x,y)

provided

A1: for x being Element of F₁()
for y being Element of F₂() holds F₄(x,y) is Element of F₃()

proof end;