:: Metrics in Cartesian Product :: by Stanis{\l}awa Kanas and Jan Stankiewicz :: :: Received September 27, 1990 :: Copyright (c) 1990-2021 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, METRIC_1, SUBSET_1, FUNCT_1, ZFMISC_1, MCART_1, STRUCT_0, NUMBERS, ARYTM_3, CARD_1, XXREAL_0, REAL_1, METRIC_3, SQUARE_1, RELAT_1, ARYTM_1, COMPLEX1, RECDEF_2, FUNCT_7; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, FUNCT_2, BINOP_1, STRUCT_0, METRIC_1, MCART_1, XXREAL_0, SQUARE_1; constructors XXREAL_0, REAL_1, MEMBERED, METRIC_1, SQUARE_1, DOMAIN_1, COMPLEX1, BINOP_1; registrations SUBSET_1, NUMBERS, STRUCT_0, METRIC_1, RELAT_1, XCMPLX_0, XREAL_0, SQUARE_1, ORDINAL1, XTUPLE_0, MCART_1; requirements SUBSET, BOOLE, ARITHM, NUMERALS, REAL; begin reserve X, Y, Z, W for non empty MetrSpace; scheme :: METRIC_3:sch 1 LambdaMCART { X, Y, Z() -> non empty set, F(object,object,object,object) -> Element of Z()} : ex f being Function of [:[:X(),Y():],[:X(),Y():]:],Z() st for x1,y1 being Element of X() for x2,y2 being Element of Y() for x,y being Element of [:X(),Y():] st x = [x1,x2] & y = [y1,y2] holds f.(x,y) = F(x1,y1,x2,y2); definition let X,Y; func dist_cart2(X,Y) -> Function of [:[:the carrier of X,the carrier of Y:], [:the carrier of X,the carrier of Y:]:], REAL means :: METRIC_3:def 1 for x1, y1 being Element of X, x2, y2 being Element of Y, x, y being Element of [:the carrier of X,the carrier of Y:] st x = [x1,x2] & y = [y1,y2] holds it.(x,y) = dist(x1,y1) + dist(x2,y2); end; theorem :: METRIC_3:1 for x, y being Element of [:the carrier of X,the carrier of Y:] holds dist_cart2(X,Y).(x,y) = 0 iff x = y; theorem :: METRIC_3:2 for x,y being Element of [:the carrier of X,the carrier of Y:] holds dist_cart2(X,Y).(x,y) = dist_cart2(X,Y).(y,x); theorem :: METRIC_3:3 for x,y,z being Element of [:the carrier of X,the carrier of Y:] holds dist_cart2(X,Y).(x,z) <= dist_cart2(X,Y).(x,y) + dist_cart2(X,Y).(y,z); definition let X,Y; let x,y be Element of [:the carrier of X,the carrier of Y:]; func dist2(x,y) -> Real equals :: METRIC_3:def 2 dist_cart2(X,Y).(x,y); end; registration let A be non empty set, r be Function of [:A,A:], REAL; cluster MetrStruct(#A,r#) -> non empty; end; definition let X,Y; func MetrSpaceCart2(X,Y) -> strict non empty MetrSpace equals :: METRIC_3:def 3 MetrStruct (#[:the carrier of X,the carrier of Y:], dist_cart2(X,Y)#); end; :: Metrics in the Cartesian product of three sets scheme :: METRIC_3:sch 2 LambdaMCART1 { X, Y, Z, T() -> non empty set, F(object,object,object,object,object,object) -> Element of T()}: ex f being Function of [:[:X(),Y(),Z():],[:X(),Y(),Z():]:],T() st for x1,y1 being Element of X() for x2,y2 being Element of Y() for x3,y3 being Element of Z() for x,y being Element of [:X(),Y(),Z():] st x = [x1,x2,x3] & y = [y1,y2,y3] holds f.(x,y) = F(x1,y1,x2,y2,x3,y3); definition let X,Y,Z; func dist_cart3(X,Y,Z) -> Function of [:[:the carrier of X,the carrier of Y, the carrier of Z:], [:the carrier of X,the carrier of Y,the carrier of Z:]:], REAL means :: METRIC_3:def 4 for x1,y1 being Element of X for x2,y2 being Element of Y for x3,y3 being Element of Z for x,y being Element of [:the carrier of X,the carrier of Y,the carrier of Z:] st x = [x1,x2,x3] & y = [y1,y2,y3] holds it.(x, y) = (dist(x1,y1) + dist(x2,y2)) + dist(x3,y3); end; theorem :: METRIC_3:4 for x,y being Element of [:the carrier of X,the carrier of Y,the carrier of Z:] holds dist_cart3(X,Y,Z).(x,y) = 0 iff x = y; theorem :: METRIC_3:5 for x,y being Element of [:the carrier of X,the carrier of Y,the carrier of Z:] holds dist_cart3(X,Y,Z).(x,y) = dist_cart3(X,Y,Z).(y,x); theorem :: METRIC_3:6 for x,y,z being Element of [:the carrier of X,the carrier of Y, the carrier of Z:] holds dist_cart3(X,Y,Z).(x,z) <= dist_cart3(X,Y,Z).(x,y) + dist_cart3(X,Y,Z).(y,z); definition let X,Y,Z; func MetrSpaceCart3(X,Y,Z) -> strict non empty MetrSpace equals :: METRIC_3:def 5 MetrStruct(# [:the carrier of X,the carrier of Y,the carrier of Z:], dist_cart3(X,Y,Z)#); end; definition let X,Y,Z; let x,y be Element of [:the carrier of X,the carrier of Y,the carrier of Z:]; func dist3(x,y) -> Real equals :: METRIC_3:def 6 dist_cart3(X,Y,Z).(x,y); end; :: Metrics in the Cartesian product of four sets scheme :: METRIC_3:sch 3 LambdaMCART2 { X, Y, Z, W, T() -> non empty set, F(object,object,object,object,object,object,object,object) ->Element of T()}: ex f being Function of [:[:X(),Y(),Z(),W():],[:X(), Y(),Z(),W():]:],T() st for x1,y1 being Element of X() for x2,y2 being Element of Y() for x3,y3 being Element of Z() for x4,y4 being Element of W() for x,y being Element of [:X(),Y(),Z(),W():] st x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4] holds f.(x,y) = F(x1,y1,x2,y2,x3,y3,x4,y4); definition let X,Y,Z,W; func dist_cart4(X,Y,Z,W) -> Function of [:[:the carrier of X,the carrier of Y,the carrier of Z,the carrier of W:], [:the carrier of X,the carrier of Y,the carrier of Z,the carrier of W:]:], REAL means :: METRIC_3:def 7 for x1,y1 being Element of X for x2,y2 being Element of Y for x3,y3 being Element of Z for x4,y4 being Element of W for x,y being Element of [:the carrier of X,the carrier of Y,the carrier of Z,the carrier of W:] st x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4] holds it.(x,y) = (dist(x1,y1) + dist(x2,y2)) + (dist(x3,y3) + dist(x4,y4)); end; theorem :: METRIC_3:7 for x,y being Element of [:the carrier of X,the carrier of Y,the carrier of Z,the carrier of W:] holds dist_cart4(X,Y,Z,W).(x,y) = 0 iff x = y ; theorem :: METRIC_3:8 for x,y being Element of [:the carrier of X,the carrier of Y,the carrier of Z,the carrier of W:] holds dist_cart4(X,Y,Z,W).(x,y) = dist_cart4(X, Y,Z,W).(y,x); theorem :: METRIC_3:9 for x,y,z being Element of [:the carrier of X,the carrier of Y, the carrier of Z,the carrier of W:] holds dist_cart4(X,Y,Z,W).(x,z) <= dist_cart4(X,Y,Z,W).(x,y) + dist_cart4(X,Y,Z,W).(y,z); definition let X,Y,Z,W; func MetrSpaceCart4(X,Y,Z,W) -> strict non empty MetrSpace equals :: METRIC_3:def 8 MetrStruct (#[:the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:], dist_cart4(X,Y,Z,W)#); end; definition let X,Y,Z,W; let x,y be Element of [:the carrier of X,the carrier of Y,the carrier of Z, the carrier of W:]; func dist4(x,y) -> Real equals :: METRIC_3:def 9 dist_cart4(X,Y,Z,W).(x,y); end; begin :: Metrics in the Cartesian Product of Two Sets (METRIC_4) reserve X,Y for non empty MetrSpace; definition let X,Y; func dist_cart2S(X,Y) -> Function of [:[:the carrier of X,the carrier of Y:] , [:the carrier of X,the carrier of Y:]:],REAL means :: METRIC_3:def 10 for x1,y1 being Element of X for x2,y2 being Element of Y for x,y being Element of [:the carrier of X,the carrier of Y:] st x = [x1,x2] & y = [y1,y2] holds it.(x,y) = sqrt((dist(x1,y1))^2 + (dist(x2,y2)^2)); end; theorem :: METRIC_3:10 for x,y being Element of [:the carrier of X,the carrier of Y:] holds dist_cart2S(X,Y).(x,y) = 0 iff x = y; theorem :: METRIC_3:11 for x,y being Element of [:the carrier of X,the carrier of Y:] holds dist_cart2S(X,Y).(x,y) = dist_cart2S(X,Y).(y,x); theorem :: METRIC_3:12 ::: for a,b,c,d being Real st 0 <= a & 0 <= b & 0 <= c & 0 <= d holds sqrt((a + c)^2 + (b + d)^2) <= sqrt(a^2 + b^2) + sqrt(c^2 + d^2); theorem :: METRIC_3:13 for x,y,z being Element of [:the carrier of X,the carrier of Y:] holds dist_cart2S(X,Y).(x,z) <= dist_cart2S(X,Y).(x,y) + dist_cart2S(X,Y).(y,z) ; definition let X,Y; let x,y be Element of [:the carrier of X,the carrier of Y:]; func dist2S(x,y) -> Real equals :: METRIC_3:def 11 dist_cart2S(X,Y).(x,y); end; definition let X,Y; func MetrSpaceCart2S(X,Y) -> strict non empty MetrSpace equals :: METRIC_3:def 12 MetrStruct(#[:the carrier of X,the carrier of Y:],dist_cart2S(X,Y)#); end; begin :: Metrics in the Cartesian Product of Three Sets reserve Z for non empty MetrSpace; definition let X,Y,Z; func dist_cart3S(X,Y,Z) -> Function of [:[:the carrier of X,the carrier of Y ,the carrier of Z:], [:the carrier of X,the carrier of Y,the carrier of Z:]:], REAL means :: METRIC_3:def 13 for x1,y1 being Element of X for x2,y2 being Element of Y for x3,y3 being Element of Z for x,y being Element of [:the carrier of X,the carrier of Y, the carrier of Z:] st x = [x1,x2,x3] & y = [y1,y2,y3] holds it.(x,y) =sqrt((dist(x1,y1))^2 + (dist(x2,y2))^2 + (dist(x3,y3))^2); end; theorem :: METRIC_3:14 for x,y being Element of [:the carrier of X,the carrier of Y,the carrier of Z:] holds dist_cart3S(X,Y,Z).(x,y) = 0 iff x = y; theorem :: METRIC_3:15 for x,y being Element of [:the carrier of X,the carrier of Y,the carrier of Z:] holds dist_cart3S(X,Y,Z).(x,y) = dist_cart3S(X,Y,Z).(y,x); theorem :: METRIC_3:16 ::: for a,b,c,d,e,f being Real holds (2*(a*d)*(c*b) + 2*(a*f) *(e*c) + 2*(b*f)*(e*d)) <= (((a*d)^2 + (c*b)^2 + (a*f)^2 + (e*c)^2 + (b*f)^2) + (e*d)^2); theorem :: METRIC_3:17 ::: for a,b,c,d,e,f being Real holds ((a*c) + (b*d) + (e*f)) ^2 <= (a^2 + b^2 + e^2)*(c^2 + d^2 + f^2); theorem :: METRIC_3:18 for x,y,z being Element of [:the carrier of X,the carrier of Y, the carrier of Z:] holds dist_cart3S(X,Y,Z).(x,z) <= dist_cart3S(X,Y,Z).(x,y) + dist_cart3S(X,Y,Z).(y,z); definition let X,Y,Z; let x,y be Element of [:the carrier of X,the carrier of Y,the carrier of Z:]; func dist3S(x,y) -> Real equals :: METRIC_3:def 14 dist_cart3S(X,Y,Z).(x,y); end; definition let X,Y,Z; func MetrSpaceCart3S(X,Y,Z) -> strict non empty MetrSpace equals :: METRIC_3:def 15 MetrStruct (#[:the carrier of X,the carrier of Y,the carrier of Z:], dist_cart3S(X,Y,Z)#); end; definition func taxi_dist2 -> Function of [:[:REAL,REAL:],[:REAL,REAL:]:],REAL means :: METRIC_3:def 16 for x1,y1,x2,y2 being Element of REAL for x,y being Element of [:REAL, REAL:] st x = [x1,x2] & y = [y1,y2] holds it.(x,y) = real_dist.(x1,y1) + real_dist.(x2,y2); end; theorem :: METRIC_3:19 for x,y being Element of [:REAL,REAL:] holds taxi_dist2.(x,y) = 0 iff x = y; theorem :: METRIC_3:20 for x,y being Element of [:REAL,REAL:] holds taxi_dist2.(x,y) = taxi_dist2.(y,x); theorem :: METRIC_3:21 for x,y,z being Element of [:REAL,REAL:] holds taxi_dist2.(x,z) <= taxi_dist2.(x,y) + taxi_dist2.(y,z); definition func RealSpaceCart2 -> strict non empty MetrSpace equals :: METRIC_3:def 17 MetrStruct(#[:REAL,REAL:],taxi_dist2#); end; definition func Eukl_dist2 -> Function of [:[:REAL,REAL:],[:REAL,REAL:]:],REAL means :: METRIC_3:def 18 for x1,y1,x2,y2 being Element of REAL for x,y being Element of [:REAL, REAL:] st x = [x1,x2] & y = [y1,y2] holds it.(x,y) = sqrt((real_dist.(x1,y1))^2 + (real_dist.(x2,y2)^2)); end; theorem :: METRIC_3:22 for x,y being Element of [:REAL,REAL:] holds Eukl_dist2.(x,y) = 0 iff x = y; theorem :: METRIC_3:23 for x,y being Element of [:REAL,REAL:] holds Eukl_dist2.(x,y) = Eukl_dist2.(y,x); theorem :: METRIC_3:24 for x,y,z being Element of [:REAL,REAL:] holds Eukl_dist2.(x,z) <= Eukl_dist2.(x,y) + Eukl_dist2.(y,z); definition func EuklSpace2 -> strict non empty MetrSpace equals :: METRIC_3:def 19 MetrStruct(#[:REAL,REAL:],Eukl_dist2#); end; definition func taxi_dist3 -> Function of [:[:REAL,REAL,REAL:], [:REAL,REAL,REAL:]:], REAL means :: METRIC_3:def 20 for x1,y1,x2,y2,x3,y3 being Element of REAL for x,y being Element of [:REAL,REAL,REAL:] st x = [x1,x2,x3] & y = [y1,y2,y3] holds it.(x,y) = real_dist.(x1,y1) + real_dist.(x2,y2) + real_dist.(x3,y3); end; theorem :: METRIC_3:25 for x,y being Element of [:REAL,REAL,REAL:] holds taxi_dist3.(x,y) = 0 iff x = y; theorem :: METRIC_3:26 for x,y being Element of [:REAL,REAL,REAL:] holds taxi_dist3.(x, y) = taxi_dist3.(y,x); theorem :: METRIC_3:27 for x,y,z being Element of [:REAL,REAL,REAL:] holds taxi_dist3.( x,z) <= taxi_dist3.(x,y) + taxi_dist3.(y,z); definition func RealSpaceCart3 -> strict non empty MetrSpace equals :: METRIC_3:def 21 MetrStruct(#[:REAL,REAL,REAL:],taxi_dist3#); end; definition func Eukl_dist3 -> Function of [:[:REAL,REAL,REAL:], [:REAL,REAL,REAL:]:], REAL means :: METRIC_3:def 22 for x1,y1,x2,y2,x3,y3 being Element of REAL for x,y being Element of [:REAL,REAL,REAL:] st x = [x1,x2,x3] & y = [y1,y2,y3] holds it.(x,y) = sqrt((real_dist.(x1,y1))^2 + (real_dist.(x2,y2)^2) + (real_dist.(x3,y3)^2)); end; theorem :: METRIC_3:28 for x,y being Element of [:REAL,REAL,REAL:] holds Eukl_dist3.(x,y) = 0 iff x = y; theorem :: METRIC_3:29 for x,y being Element of [:REAL,REAL,REAL:] holds Eukl_dist3.(x, y) = Eukl_dist3.(y,x); theorem :: METRIC_3:30 for x,y,z being Element of [:REAL,REAL,REAL:] holds Eukl_dist3.( x,z) <= Eukl_dist3.(x,y) + Eukl_dist3.(y,z); definition func EuklSpace3 -> strict non empty MetrSpace equals :: METRIC_3:def 23 MetrStruct(#[:REAL,REAL,REAL:],Eukl_dist3#); end;