:: Metrics in Cartesian Product
:: by Stanis{\l}awa Kanas and Jan Stankiewicz
::
:: Received September 27, 1990
:: Copyright (c) 1990 Association of Mizar Users



scheme :: METRIC_3:sch 1
LambdaMCART{ F1() -> non empty set , F2() -> non empty set , F3() -> non empty set , F4( set , set , set , set ) -> Element of F3() } :
ex f being Function of [:[:F1(),F2():],[:F1(),F2():]:],F3() st
for x1, y1 being Element of F1()
for x2, y2 being Element of F2()
for x, y being Element of [:F1(),F2():] st x = [x1,x2] & y = [y1,y2] holds
f . x,y = F4(x1,y1,x2,y2)
proof end;

definition
let X, Y be non empty MetrSpace;
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 :Def1: :: METRIC_3:def 1
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 = (dist x1,y1) + (dist x2,y2);
existence
ex b1 being Function of [:[:the carrier of X,the carrier of Y:],[:the carrier of X,the carrier of Y:]:],REAL st
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
b1 . x,y = (dist x1,y1) + (dist x2,y2)
proof end;
uniqueness
for b1, b2 being Function of [:[:the carrier of X,the carrier of Y:],[:the carrier of X,the carrier of Y:]:],REAL st ( 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
b1 . x,y = (dist x1,y1) + (dist x2,y2) ) & ( 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
b2 . x,y = (dist x1,y1) + (dist x2,y2) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines dist_cart2 METRIC_3:def 1 :
for X, Y being non empty MetrSpace
for b3 being Function of [:[:the carrier of X,the carrier of Y:],[:the carrier of X,the carrier of Y:]:],REAL holds
( b3 = dist_cart2 X,Y iff 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
b3 . x,y = (dist x1,y1) + (dist x2,y2) );

theorem :: METRIC_3:1
canceled;

theorem :: METRIC_3:2
canceled;

theorem :: METRIC_3:3
canceled;

theorem :: METRIC_3:4
canceled;

theorem Th5: :: METRIC_3:5
for X, Y being non empty MetrSpace
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 )
proof end;

theorem Th6: :: METRIC_3:6
for X, Y being non empty MetrSpace
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
proof end;

theorem Th7: :: METRIC_3:7
for X, Y being non empty MetrSpace
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)
proof end;

definition
let X, Y be non empty MetrSpace;
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;
coherence
(dist_cart2 X,Y) . x,y is Real ;
end;

:: deftheorem defines dist2 METRIC_3:def 2 :
for X, Y being non empty MetrSpace
for x, y being Element of [:the carrier of X,the carrier of Y:] holds dist2 x,y = (dist_cart2 X,Y) . x,y;

registration
let A be non empty set ;
let r be Function of [:A,A:],REAL ;
cluster MetrStruct(# A,r #) -> non empty ;
coherence
not MetrStruct(# A,r #) is empty ;
end;

definition
let X, Y be non empty MetrSpace;
func MetrSpaceCart2 X,Y -> non empty strict MetrSpace equals :: METRIC_3:def 3
 MetrStruct(# [:the carrier of X,the carrier of Y:],(dist_cart2 X,Y) #);
coherence
MetrStruct(# [:the carrier of X,the carrier of Y:],(dist_cart2 X,Y) #) is non empty strict MetrSpace
proof end;
end;

:: deftheorem defines MetrSpaceCart2 METRIC_3:def 3 :
for X, Y being non empty MetrSpace holds MetrSpaceCart2 X,Y = MetrStruct(# [:the carrier of X,the carrier of Y:],(dist_cart2 X,Y) #);

scheme :: METRIC_3:sch 2
LambdaMCART1{ F1() -> non empty set , F2() -> non empty set , F3() -> non empty set , F4() -> non empty set , F5( set , set , set , set , set , set ) -> Element of F4() } :
ex f being Function of [:[:F1(),F2(),F3():],[:F1(),F2(),F3():]:],F4() st
for x1, y1 being Element of F1()
for x2, y2 being Element of F2()
for x3, y3 being Element of F3()
for x, y being Element of [:F1(),F2(),F3():] st x = [x1,x2,x3] & y = [y1,y2,y3] holds
f . x,y = F5(x1,y1,x2,y2,x3,y3)
proof end;

definition
let X, Y, Z be non empty MetrSpace;
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 :Def4: :: 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);
existence
ex b1 being 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 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 [:the carrier of X,the carrier of Y,the carrier of Z:] st x = [x1,x2,x3] & y = [y1,y2,y3] holds
b1 . x,y = ((dist x1,y1) + (dist x2,y2)) + (dist x3,y3)
proof end;
uniqueness
for b1, b2 being 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 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 [:the carrier of X,the carrier of Y,the carrier of Z:] st x = [x1,x2,x3] & y = [y1,y2,y3] holds
b1 . x,y = ((dist x1,y1) + (dist x2,y2)) + (dist x3,y3) ) & ( 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
b2 . x,y = ((dist x1,y1) + (dist x2,y2)) + (dist x3,y3) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines dist_cart3 METRIC_3:def 4 :
for X, Y, Z being non empty MetrSpace
for b4 being 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 holds
( b4 = dist_cart3 X,Y,Z iff 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
b4 . x,y = ((dist x1,y1) + (dist x2,y2)) + (dist x3,y3) );

theorem :: METRIC_3:8
canceled;

theorem :: METRIC_3:9
canceled;

theorem :: METRIC_3:10
canceled;

theorem :: METRIC_3:11
canceled;

theorem Th12: :: METRIC_3:12
for X, Y, Z being non empty MetrSpace
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 )
proof end;

theorem Th13: :: METRIC_3:13
for X, Y, Z being non empty MetrSpace
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
proof end;

theorem Th14: :: METRIC_3:14
for X, Y, Z being non empty MetrSpace
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)
proof end;

definition
let X, Y, Z be non empty MetrSpace;
func MetrSpaceCart3 X,Y,Z -> non empty strict MetrSpace equals :: METRIC_3:def 5
 MetrStruct(# [:the carrier of X,the carrier of Y,the carrier of Z:],(dist_cart3 X,Y,Z) #);
coherence
MetrStruct(# [:the carrier of X,the carrier of Y,the carrier of Z:],(dist_cart3 X,Y,Z) #) is non empty strict MetrSpace
proof end;
end;

:: deftheorem defines MetrSpaceCart3 METRIC_3:def 5 :
for X, Y, Z being non empty MetrSpace holds MetrSpaceCart3 X,Y,Z = MetrStruct(# [:the carrier of X,the carrier of Y,the carrier of Z:],(dist_cart3 X,Y,Z) #);

definition
let X, Y, Z be non empty MetrSpace;
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;
coherence
(dist_cart3 X,Y,Z) . x,y is Real ;
end;

:: deftheorem defines dist3 METRIC_3:def 6 :
for X, Y, Z being non empty MetrSpace
for x, y being Element of [:the carrier of X,the carrier of Y,the carrier of Z:] holds dist3 x,y = (dist_cart3 X,Y,Z) . x,y;

scheme :: METRIC_3:sch 3
LambdaMCART2{ F1() -> non empty set , F2() -> non empty set , F3() -> non empty set , F4() -> non empty set , F5() -> non empty set , F6( set , set , set , set , set , set , set , set ) -> Element of F5() } :
ex f being Function of [:[:F1(),F2(),F3(),F4():],[:F1(),F2(),F3(),F4():]:],F5() st
for x1, y1 being Element of F1()
for x2, y2 being Element of F2()
for x3, y3 being Element of F3()
for x4, y4 being Element of F4()
for x, y being Element of [:F1(),F2(),F3(),F4():] st x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4] holds
f . x,y = F6(x1,y1,x2,y2,x3,y3,x4,y4)
proof end;

definition
let X, Y, Z, W be non empty MetrSpace;
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 :Def7: :: 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));
existence
ex b1 being 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 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 [: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
b1 . x,y = ((dist x1,y1) + (dist x2,y2)) + ((dist x3,y3) + (dist x4,y4))
proof end;
uniqueness
for b1, b2 being 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 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 [: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
b1 . x,y = ((dist x1,y1) + (dist x2,y2)) + ((dist x3,y3) + (dist x4,y4)) ) & ( 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
b2 . x,y = ((dist x1,y1) + (dist x2,y2)) + ((dist x3,y3) + (dist x4,y4)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines dist_cart4 METRIC_3:def 7 :
for X, Y, Z, W being non empty MetrSpace
for b5 being 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 holds
( b5 = dist_cart4 X,Y,Z,W iff 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
b5 . x,y = ((dist x1,y1) + (dist x2,y2)) + ((dist x3,y3) + (dist x4,y4)) );

theorem :: METRIC_3:15
canceled;

theorem :: METRIC_3:16
canceled;

theorem :: METRIC_3:17
canceled;

theorem :: METRIC_3:18
canceled;

theorem Th19: :: METRIC_3:19
for X, Y, Z, W being non empty MetrSpace
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 )
proof end;

theorem Th20: :: METRIC_3:20
for X, Y, Z, W being non empty MetrSpace
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
proof end;

theorem Th21: :: METRIC_3:21
for X, Y, Z, W being non empty MetrSpace
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)
proof end;

definition
let X, Y, Z, W be non empty MetrSpace;
func MetrSpaceCart4 X,Y,Z,W -> non empty strict 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) #);
coherence
MetrStruct(# [:the carrier of X,the carrier of Y,the carrier of Z,the carrier of W:],(dist_cart4 X,Y,Z,W) #) is non empty strict MetrSpace
proof end;
end;

:: deftheorem defines MetrSpaceCart4 METRIC_3:def 8 :
for X, Y, Z, W being non empty MetrSpace holds MetrSpaceCart4 X,Y,Z,W = MetrStruct(# [:the carrier of X,the carrier of Y,the carrier of Z,the carrier of W:],(dist_cart4 X,Y,Z,W) #);

definition
let X, Y, Z, W be non empty MetrSpace;
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;
coherence
(dist_cart4 X,Y,Z,W) . x,y is Real ;
end;

:: deftheorem defines dist4 METRIC_3:def 9 :
for X, Y, Z, W being non empty MetrSpace
for x, y being Element of [:the carrier of X,the carrier of Y,the carrier of Z,the carrier of W:] holds dist4 x,y = (dist_cart4 X,Y,Z,W) . x,y;