:: Cartesian Products of Relations and Relational Structures :: by Artur Korni{\l}owicz :: :: Received September 25, 1996 :: Copyright (c) 1996-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, SUBSET_1, TARSKI, ORDERS_2, WAYBEL_0, XXREAL_0, ZFMISC_1, RELAT_1, MCART_1, LATTICE3, RELAT_2, LATTICES, YELLOW_0, EQREL_1, REWRITE1, ORDINAL2, FUNCT_1, STRUCT_0, YELLOW_3; notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, RELAT_1, RELAT_2, RELSET_1, MCART_1, DOMAIN_1, FUNCT_2, BINOP_1, STRUCT_0, ORDERS_2, LATTICE3, YELLOW_0, WAYBEL_0; constructors DOMAIN_1, LATTICE3, ORDERS_3, WAYBEL_0, RELSET_1, XTUPLE_0; registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, LATTICE3, YELLOW_0, ORDERS_2, WAYBEL_0, RELAT_1, XTUPLE_0; requirements SUBSET, BOOLE; begin :: Preliminaries scheme :: YELLOW_3:sch 1 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 (); registration 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 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; theorem :: YELLOW_3:9 for S, T being with_suprema Poset, 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; scheme :: YELLOW_3:sch 2 InfUnion { 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 :: YELLOW_3:sch 3 InfofInfs { 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 :: YELLOW_3:sch 4 SupUnion { 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 :: YELLOW_3:sch 5 SupofSups { 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 object holds [x,y] in it iff ex p,q,s,t being object 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 object 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 object st x = [a,b]) & (ex c, d being object st x`1 = [c,d]) & ex e, f being object 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 Function 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; registration let X, Y be non empty RelStr; cluster [:X,Y:] -> non empty; end; registration let X, Y be reflexive RelStr; cluster [:X,Y:] -> reflexive; end; registration let X, Y be antisymmetric RelStr; cluster [:X,Y:] -> antisymmetric; end; registration let X, Y be transitive RelStr; cluster [:X,Y:] -> transitive; end; registration let X, Y be with_suprema RelStr; cluster [:X,Y:] -> with_suprema; end; registration 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; registration let S1, S2 be RelStr; let D1 be directed Subset of S1, D2 be directed Subset of S2; cluster [:D1,D2:] -> directed for 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; registration let S1, S2 be RelStr; let D1 be filtered Subset of S1, D2 be filtered Subset of S2; cluster [:D1,D2:] -> filtered for 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; registration let S1, S2 be RelStr, D1 be upper Subset of S1, D2 be upper Subset of S2; cluster [:D1,D2:] -> upper for 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; registration let S1, S2 be RelStr, D1 be lower Subset of S1, D2 be lower Subset of S2; cluster [:D1,D2:] -> lower for 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; registration cluster empty -> void for RelStr; end; registration cluster non void non empty strict for Poset; end; registration cluster non void -> non empty for RelStr; end; registration cluster non empty reflexive -> non void for RelStr; end; registration 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]; registration 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 :: YELLOW_3:sch 6 Kappa2DS { X,Y,Z() -> non empty RelStr, F(set,set) -> set }: ex f being Function 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();