:: Tuples, Projections and Cartesian Products :: by Andrzej Trybulec :: :: Received March 30, 1989 :: Copyright (c) 1990-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, ZFMISC_1, RELAT_1, FUNCT_1, MCART_1, XTUPLE_0, RECDEF_2, FACIRC_1; notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, SUBSET_1, RELAT_1, FUNCT_1; constructors TARSKI, ENUMSET1, XTUPLE_0, SUBSET_1, FUNCT_1; registrations RELAT_1, XTUPLE_0, SUBSET_1; requirements SUBSET, BOOLE; begin reserve v,x,x1,x2,x3,x4,y,y1,y2,y3,y4,z,z1,z2 for object, X,X1,X2,X3,X4,Y,Y1,Y2,Y3,Y4,Y5, Z,Z1,Z2,Z3,Z4,Z5 for set; reserve p for pair object; :: :: Ordered pairs :: :: Now we introduce the projections of ordered pairs (functions that assign :: to an ordered pair its first and its second element). The definitions :: are permissive, function are defined for an arbitrary object. If it is not :: an ordered pair, they are of course meaningless. ::\$CT 8 theorem :: MCART_1:9 X <> {} implies ex v st v in X & not ex x,y st (x in X or y in X) & v = [x,y]; :: Now we prove theorems describing relationships between projections :: of ordered pairs and Cartesian products of two sets. theorem :: MCART_1:10 z in [:X,Y:] implies z`1 in X & z`2 in Y; ::\$CT theorem :: MCART_1:12 z in [:{x},Y:] implies z`1=x & z`2 in Y; theorem :: MCART_1:13 z in [:X,{y}:] implies z`1 in X & z`2 = y; theorem :: MCART_1:14 z in [:{x},{y}:] implies z`1 = x & z`2 = y; theorem :: MCART_1:15 z in [:{x1,x2},Y:] implies (z`1=x1 or z`1=x2) & z`2 in Y; theorem :: MCART_1:16 z in [:X,{y1,y2}:] implies z`1 in X & (z`2 = y1 or z`2 = y2); theorem :: MCART_1:17 z in [:{x1,x2},{y}:] implies (z`1=x1 or z`1=x2) & z`2 = y; theorem :: MCART_1:18 z in [:{x},{y1,y2}:] implies z`1 = x & (z`2 = y1 or z`2 = y2); theorem :: MCART_1:19 z in [:{x1,x2},{y1,y2}:] implies (z`1 = x1 or z`1 = x2) & (z`2 = y1 or z`2 = y2); theorem :: MCART_1:20 (ex y,z st x = [y,z]) implies x <> x`1 & x <> x`2; :: Some of theorems proved above may be simplified , if we state them :: for elements of Cartesian product rather than for arbitrary objects. reserve R for Relation; theorem :: MCART_1:21 x in R implies x = [x`1,x`2]; registration let X1,X2 be non empty set; cluster -> pair for Element of [:X1,X2:]; end; theorem :: MCART_1:22 X <> {} & Y <> {} implies for x being Element of [:X,Y:] holds x = [x`1,x`2]; theorem :: MCART_1:23 [:{x1,x2},{y1,y2}:] = {[x1,y1],[x1,y2],[x2,y1],[x2,y2]}; theorem :: MCART_1:24 X <> {} & Y <> {} implies for x being Element of [:X,Y:] holds x <> x`1 & x <> x`2; :: :: Triples :: ::\$CT theorem :: MCART_1:26 X <> {} implies ex v st v in X & not ex x,y,z st (x in X or y in X) & v = [x,y,z]; :: :: Quadruples :: ::\$CT 3 theorem :: MCART_1:30 X <> {} implies ex v st v in X & not ex x1,x2,x3,x4 st (x1 in X or x2 in X) & v = [x1,x2,x3,x4]; :: :: Cartesian products of three sets :: theorem :: MCART_1:31 X1 <> {} & X2 <> {} & X3 <> {} iff [:X1,X2,X3:] <> {}; reserve xx1 for Element of X1, xx2 for Element of X2, xx3 for Element of X3; theorem :: MCART_1:32 X1<>{} & X2<>{} & X3<>{} implies ( [:X1,X2,X3:] = [:Y1,Y2,Y3:] implies X1=Y1 & X2=Y2 & X3=Y3); theorem :: MCART_1:33 [:X1,X2,X3:]<>{} & [:X1,X2,X3:] = [:Y1,Y2,Y3:] implies X1=Y1 & X2=Y2 & X3=Y3; theorem :: MCART_1:34 [:X,X,X:] = [:Y,Y,Y:] implies X = Y; theorem :: MCART_1:35 [:{x1},{x2},{x3}:] = { [x1,x2,x3] }; theorem :: MCART_1:36 [:{x1,y1},{x2},{x3}:] = { [x1,x2,x3],[y1,x2,x3] }; theorem :: MCART_1:37 [:{x1},{x2,y2},{x3}:] = { [x1,x2,x3],[x1,y2,x3] }; theorem :: MCART_1:38 [:{x1},{x2},{x3,y3}:] = { [x1,x2,x3],[x1,x2,y3] }; theorem :: MCART_1:39 [:{x1,y1},{x2,y2},{x3}:] = { [x1,x2,x3],[y1,x2,x3],[x1,y2,x3],[y1,y2, x3] }; theorem :: MCART_1:40 [:{x1,y1},{x2},{x3,y3}:] = { [x1,x2,x3],[y1,x2,x3],[x1,x2,y3],[y1,x2, y3] }; theorem :: MCART_1:41 [:{x1},{x2,y2},{x3,y3}:] = { [x1,x2,x3],[x1,y2,x3],[x1,x2,y3],[x1,y2, y3] }; theorem :: MCART_1:42 [:{x1,y1},{x2,y2},{x3,y3}:] = { [x1,x2,x3],[x1,y2,x3],[x1,x2,y3],[x1, y2,y3], [y1,x2,x3],[y1,y2,x3],[y1,x2,y3],[y1,y2,y3] }; registration let X1,X2,X3 be non empty set; cluster -> triple for Element of [:X1,X2,X3:]; end; definition ::\$CD 4 let X1,X2,X3 be non empty set; let x be Element of [:X1,X2,X3:]; redefine func x`1_3 -> Element of X1 means :: MCART_1:def 5 x = [x1,x2,x3] implies it = x1; redefine func x`2_3 -> Element of X2 means :: MCART_1:def 6 x = [x1,x2,x3] implies it = x2; redefine func x`3_3 -> Element of X3 means :: MCART_1:def 7 x = [x1,x2,x3] implies it = x3; end; ::\$CT 2 theorem :: MCART_1:45 X c= [:X,Y,Z:] or X c= [:Y,Z,X:] or X c= [:Z,X,Y:] implies X = {}; ::\$CT theorem :: MCART_1:47 for X1,X2,X3 being non empty set for x being Element of [:X1,X2,X3:] holds x <> x`1_3 & x <> x`2_3 & x <> x`3_3; theorem :: MCART_1:48 [:X1,X2,X3:] meets [:Y1,Y2,Y3:] implies X1 meets Y1 & X2 meets Y2 & X3 meets Y3; :: :: Cartesian products of four sets :: theorem :: MCART_1:49 [:X1,X2,X3,X4:] = [:[:[:X1,X2:],X3:],X4:]; theorem :: MCART_1:50 [:[:X1,X2:],X3,X4:] = [:X1,X2,X3,X4:]; theorem :: MCART_1:51 X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} iff [:X1,X2,X3,X4:] <> {}; theorem :: MCART_1:52 X1<>{} & X2<>{} & X3<>{} & X4<>{} & [:X1,X2,X3,X4:] = [:Y1,Y2,Y3 ,Y4:] implies X1=Y1 & X2=Y2 & X3=Y3 & X4=Y4; theorem :: MCART_1:53 [:X1,X2,X3,X4:]<>{} & [:X1,X2,X3,X4:] = [:Y1,Y2,Y3,Y4:] implies X1=Y1 & X2=Y2 & X3=Y3 & X4=Y4; theorem :: MCART_1:54 [:X,X,X,X:] = [:Y,Y,Y,Y:] implies X = Y; reserve xx4 for Element of X4; registration let X1,X2,X3,X4 be non empty set; cluster -> quadruple for Element of [:X1,X2,X3,X4:]; end; definition let X1,X2,X3,X4 be non empty set; let x be Element of [:X1,X2,X3,X4:]; redefine func x`1_4 -> Element of X1 means :: MCART_1:def 8 x = [x1,x2,x3,x4] implies it = x1; redefine func x`2_4 -> Element of X2 means :: MCART_1:def 9 x = [x1,x2,x3,x4] implies it = x2; redefine func x`3_4 -> Element of X3 means :: MCART_1:def 10 x = [x1,x2,x3,x4] implies it = x3; redefine func x`4_4 -> Element of X4 means :: MCART_1:def 11 x = [x1,x2,x3,x4] implies it = x4; end; ::\$CT 3 theorem :: MCART_1:58 for X1,X2,X3,X4 being non empty set for x being Element of [:X1,X2,X3,X4:] holds x <> x`1_4 & x <> x`2_4 & x <> x`3_4 & x <> x`4_4; theorem :: MCART_1:59 X1 c= [:X1,X2,X3,X4:] or X1 c= [:X2,X3,X4,X1:] or X1 c= [:X3,X4,X1,X2 :] or X1 c= [:X4,X1,X2,X3:] implies X1 = {}; theorem :: MCART_1:60 [:X1,X2,X3,X4:] meets [:Y1,Y2,Y3,Y4:] implies X1 meets Y1 & X2 meets Y2 & X3 meets Y3 & X4 meets Y4; theorem :: MCART_1:61 [:{x1},{x2},{x3},{x4}:] = { [x1,x2,x3,x4] }; :: Ordered pairs theorem :: MCART_1:62 [:X,Y:] <> {} implies for x being Element of [:X,Y:] holds x <> x`1 & x <> x`2; theorem :: MCART_1:63 x in [:X,Y:] implies x <> x`1 & x <> x`2; :: Triples reserve A1 for Subset of X1, A2 for Subset of X2, A3 for Subset of X3, A4 for Subset of X4; reserve x for Element of [:X1,X2,X3:]; theorem :: MCART_1:64 for X1,X2,X3 being non empty set for x being Element of [:X1,X2,X3:] for x1,x2,x3 st x = [x1,x2,x3] holds x`1_3 = x1 & x`2_3 = x2 & x`3_3 = x3; theorem :: MCART_1:65 for X1,X2,X3 being non empty set for x being Element of [:X1,X2,X3:] st for xx1 being Element of X1,xx2 being Element of X2, xx3 being Element of X3 st x = [xx1,xx2,xx3] holds y1 = xx1 holds y1 =x`1_3; theorem :: MCART_1:66 for X1,X2,X3 being non empty set for x being Element of [:X1,X2,X3:] st for xx1 being Element of X1,xx2 being Element of X2, xx3 being Element of X3 st x = [xx1,xx2,xx3] holds y2 = xx2 holds y2 =x`2_3; theorem :: MCART_1:67 for X1,X2,X3 being non empty set for x being Element of [:X1,X2,X3:] st for xx1 being Element of X1,xx2 being Element of X2, xx3 being Element of X3 st x = [xx1,xx2,xx3] holds y3 = xx3 holds y3 =x`3_3; theorem :: MCART_1:68 z in [: X1,X2,X3 :] implies ex x1,x2,x3 st x1 in X1 & x2 in X2 & x3 in X3 & z = [x1,x2,x3]; theorem :: MCART_1:69 [x1,x2,x3] in [: X1,X2,X3 :] iff x1 in X1 & x2 in X2 & x3 in X3; theorem :: MCART_1:70 (for z holds z in Z iff ex x1,x2,x3 st x1 in X1 & x2 in X2 & x3 in X3 & z = [x1,x2,x3]) implies Z = [: X1,X2,X3 :]; ::\$CT theorem :: MCART_1:72 for X1,X2,X3 being non empty set for A1 being non empty Subset of X1, A2 being non empty Subset of X2, A3 being non empty Subset of X3 for x being Element of [:X1,X2,X3:] st x in [:A1,A2,A3:] holds x`1_3 in A1 & x`2_3 in A2 & x`3_3 in A3; theorem :: MCART_1:73 X1 c= Y1 & X2 c= Y2 & X3 c= Y3 implies [:X1,X2,X3:] c= [:Y1,Y2, Y3:]; :: Quadruples reserve x for Element of [:X1,X2,X3,X4:]; theorem :: MCART_1:74 for X1,X2,X3,X4 being non empty set for x being Element of [:X1,X2,X3,X4:] for x1,x2,x3,x4 being set st x = [x1, x2,x3,x4] holds x`1_4 = x1 & x`2_4 = x2 & x`3_4 = x3 & x`4_4 = x4; theorem :: MCART_1:75 for X1,X2,X3,X4 being non empty set for x being Element of [:X1,X2,X3,X4:] st for xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3, xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds y1 = xx1 holds y1 =x`1_4; theorem :: MCART_1:76 for X1,X2,X3,X4 being non empty set for x being Element of [:X1,X2,X3,X4:] st for xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3, xx4 being Element of X4 st x = [xx1, xx2,xx3,xx4] holds y2 = xx2 holds y2 =x`2_4; theorem :: MCART_1:77 for X1,X2,X3,X4 being non empty set for x being Element of [:X1,X2,X3,X4:] st for xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3, xx4 being Element of X4 st x = [xx1, xx2,xx3,xx4] holds y3 = xx3 holds y3 =x`3_4; theorem :: MCART_1:78 for X1,X2,X3,X4 being non empty set for x being Element of [:X1,X2,X3,X4:] st for xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3, xx4 being Element of X4 st x = [xx1, xx2,xx3,xx4] holds y4 = xx4 holds y4 =x`4_4; theorem :: MCART_1:79 z in [: X1,X2,X3,X4 :] implies ex x1,x2,x3,x4 st x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & z = [x1,x2,x3,x4]; theorem :: MCART_1:80 [x1,x2,x3,x4] in [: X1,X2,X3,X4 :] iff x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4; theorem :: MCART_1:81 (for z holds z in Z iff ex x1,x2,x3,x4 st x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & z = [x1,x2,x3,x4]) implies Z = [: X1,X2,X3,X4 :]; ::\$CT theorem :: MCART_1:83 for X1,X2,X3,X4 being non empty set, A1 being non empty Subset of X1, A2 being non empty Subset of X2, A3 being non empty Subset of X3, A4 being non empty Subset of X4 for x being Element of [:X1,X2,X3,X4:] st x in [:A1,A2,A3,A4:] holds x`1_4 in A1 & x`2_4 in A2 & x`3_4 in A3 & x`4_4 in A4; theorem :: MCART_1:84 X1 c= Y1 & X2 c= Y2 & X3 c= Y3 & X4 c= Y4 implies [:X1,X2,X3,X4:] c= [:Y1,Y2,Y3,Y4:]; definition let X1,X2,A1,A2; redefine func [:A1,A2:] -> Subset of [:X1,X2:]; end; definition let X1,X2,X3,A1,A2,A3; redefine func [:A1,A2,A3:] -> Subset of [:X1,X2,X3:]; end; definition let X1,X2,X3,X4,A1,A2,A3,A4; redefine func [:A1,A2,A3,A4:] -> Subset of [:X1,X2,X3,X4:]; end; begin :: Addenda :: from DTCONSTR definition let f be Function; func pr1 f -> Function means :: MCART_1:def 12 dom it = dom f & for x being object st x in dom f holds it.x = (f.x)`1; func pr2 f -> Function means :: MCART_1:def 13 dom it = dom f & for x being object st x in dom f holds it.x = (f.x)`2; end; definition let x be object; func x`11 -> set equals :: MCART_1:def 14 x`1`1; func x`12 -> set equals :: MCART_1:def 15 x`1`2; func x`21 -> set equals :: MCART_1:def 16 x`2`1; func x`22 -> set equals :: MCART_1:def 17 x`2`2; end; reserve x for object; theorem :: MCART_1:85 [[x1,x2],y]`11 = x1 & [[x1,x2],y]`12 = x2 & [x,[y1,y2]]`21 = y1 & [x,[ y1,y2]]`22 = y2; :: missing, 2007.04.13, A.T. theorem :: MCART_1:86 x in R implies x`1 in dom R & x`2 in rng R; :: 2009.08.29, A.T. theorem :: MCART_1:87 for R being non empty Relation, x being object holds Im(R,x) = { I`2 where I is Element of R: I`1 = x }; theorem :: MCART_1:88 x in R implies x`2 in Im(R,x`1); theorem :: MCART_1:89 x in R & y in R & x`1 = y`1 & x`2 = y`2 implies x = y; theorem :: MCART_1:90 for R being non empty Relation, x,y being Element of R st x`1 = y`1 & x`2 = y`2 holds x = y; :: 2010.05.120, A.T. theorem :: MCART_1:91 proj1 proj1 {[x1,x2,x3],[y1,y2,y3]} = {x1,y1}; theorem :: MCART_1:92 proj1 proj1 {[x1,x2,x3]} = {x1}; scheme :: MCART_1:sch 1 BiFuncEx{A()->set,B()->set,C()->set,P[object,object,object]}: ex f,g being Function st dom f = A() & dom g = A() & for x st x in A() holds P[x,f.x,g.x] provided x in A() implies ex y,z st y in B() & z in C() & P[x,y,z]; theorem :: MCART_1:93 [[x1,x2],[x3,x4]] = [[y1,y2],[y3,y4]] implies x1=y1 & x2=y2 & x3=y3 & x4=y4;