Volume 8, 1996

University of Bialystok

Copyright (c) 1996 Association of Mizar Users

### The abstract of the Mizar article:

### Cartesian Products of Relations and Relational Structures

**by****Artur Kornilowicz**- Received September 25, 1996
- 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();

Back to top