begin
scheme
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)
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:
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)
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
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 Th5:
theorem Th6:
theorem Th7:
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)
:: 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;
:: 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
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)
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:
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)
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
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 Th12:
theorem Th13:
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
theorem Th14:
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)
definition
let X,
Y,
Z be non
empty MetrSpace;
func MetrSpaceCart3 X,
Y,
Z -> non
empty strict MetrSpace equals
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
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
(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
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)
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:
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))
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
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 Th19:
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 )
theorem Th20:
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
theorem Th21:
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)
definition
let X,
Y,
Z,
W be non
empty MetrSpace;
func MetrSpaceCart4 X,
Y,
Z,
W -> non
empty strict MetrSpace equals
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
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
(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;
begin
definition
let X,
Y be non
empty MetrSpace;
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 :
Def1:
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 ));
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 = sqrt (((dist x1,y1) ^2 ) + ((dist x2,y2) ^2 ))
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 = sqrt (((dist x1,y1) ^2 ) + ((dist x2,y2) ^2 )) ) & ( 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 = sqrt (((dist x1,y1) ^2 ) + ((dist x2,y2) ^2 )) ) holds
b1 = b2
end;
:: deftheorem Def1 defines dist_cart2S METRIC_3:def 10 :
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_cart2S 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 = sqrt (((dist x1,y1) ^2 ) + ((dist x2,y2) ^2 )) );
Th2:
for a, b being real number st 0 <= a & 0 <= b holds
( sqrt (a + b) = 0 iff ( a = 0 & b = 0 ) )
by SQUARE_1:100;
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
for
X,
Y being non
empty MetrSpace 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)
:: deftheorem defines dist2S METRIC_3:def 11 :
for X, Y being non empty MetrSpace
for x, y being Element of [:the carrier of X,the carrier of Y:] holds dist2S x,y = (dist_cart2S X,Y) . x,y;
:: deftheorem defines MetrSpaceCart2S METRIC_3:def 12 :
for X, Y being non empty MetrSpace holds MetrSpaceCart2S X,Y = MetrStruct(# [:the carrier of X,the carrier of Y:],(dist_cart2S X,Y) #);
begin
definition
let X,
Y,
Z be non
empty MetrSpace;
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 :
Def4:
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 ));
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 = sqrt ((((dist x1,y1) ^2 ) + ((dist x2,y2) ^2 )) + ((dist x3,y3) ^2 ))
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 = sqrt ((((dist x1,y1) ^2 ) + ((dist x2,y2) ^2 )) + ((dist x3,y3) ^2 )) ) & ( 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 = sqrt ((((dist x1,y1) ^2 ) + ((dist x2,y2) ^2 )) + ((dist x3,y3) ^2 )) ) holds
b1 = b2
end;
:: deftheorem Def4 defines dist_cart3S METRIC_3:def 13 :
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_cart3S 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 = sqrt ((((dist x1,y1) ^2 ) + ((dist x2,y2) ^2 )) + ((dist x3,y3) ^2 )) );
theorem Th10:
theorem Th11:
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_cart3S X,Y,Z) . x,
y = (dist_cart3S X,Y,Z) . y,
x
theorem Th13:
theorem Th15:
Lm1:
for a, b, c, d, e, f being real number st 0 <= a & 0 <= b & 0 <= c & 0 <= d & 0 <= e & 0 <= f holds
sqrt ((((a + c) ^2 ) + ((b + d) ^2 )) + ((e + f) ^2 )) <= (sqrt (((a ^2 ) + (b ^2 )) + (e ^2 ))) + (sqrt (((c ^2 ) + (d ^2 )) + (f ^2 )))
theorem Th16:
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_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 be non
empty MetrSpace;
let x,
y be
Element of
[:the carrier of X,the carrier of Y,the carrier of Z:];
func dist3S x,
y -> Real equals
(dist_cart3S X,Y,Z) . x,
y;
coherence
(dist_cart3S X,Y,Z) . x,y is Real
;
end;
:: deftheorem defines dist3S METRIC_3:def 14 :
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 dist3S x,y = (dist_cart3S X,Y,Z) . x,y;
definition
let X,
Y,
Z be non
empty MetrSpace;
func MetrSpaceCart3S X,
Y,
Z -> non
empty strict MetrSpace equals
MetrStruct(#
[:the carrier of X,the carrier of Y,the carrier of Z:],
(dist_cart3S X,Y,Z) #);
coherence
MetrStruct(# [:the carrier of X,the carrier of Y,the carrier of Z:],(dist_cart3S X,Y,Z) #) is non empty strict MetrSpace
end;
:: deftheorem defines MetrSpaceCart3S METRIC_3:def 15 :
for X, Y, Z being non empty MetrSpace holds MetrSpaceCart3S X,Y,Z = MetrStruct(# [:the carrier of X,the carrier of Y,the carrier of Z:],(dist_cart3S X,Y,Z) #);
definition
func taxi_dist2 -> Function of
[:[:REAL ,REAL :],[:REAL ,REAL :]:],
REAL means :
Def7:
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);
existence
ex b1 being Function of [:[:REAL ,REAL :],[:REAL ,REAL :]:],REAL st
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
b1 . x,y = (real_dist . x1,y1) + (real_dist . x2,y2)
uniqueness
for b1, b2 being Function of [:[:REAL ,REAL :],[:REAL ,REAL :]:],REAL st ( 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
b1 . x,y = (real_dist . x1,y1) + (real_dist . x2,y2) ) & ( 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
b2 . x,y = (real_dist . x1,y1) + (real_dist . x2,y2) ) holds
b1 = b2
end;
:: deftheorem Def7 defines taxi_dist2 METRIC_3:def 16 :
for b1 being Function of [:[:REAL ,REAL :],[:REAL ,REAL :]:],REAL holds
( b1 = taxi_dist2 iff 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
b1 . x,y = (real_dist . x1,y1) + (real_dist . x2,y2) );
theorem Th19:
theorem Th20:
theorem Th21:
:: deftheorem defines RealSpaceCart2 METRIC_3:def 17 :
RealSpaceCart2 = MetrStruct(# [:REAL ,REAL :],taxi_dist2 #);
definition
func Eukl_dist2 -> Function of
[:[:REAL ,REAL :],[:REAL ,REAL :]:],
REAL means :
Def9:
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 ));
existence
ex b1 being Function of [:[:REAL ,REAL :],[:REAL ,REAL :]:],REAL st
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
b1 . x,y = sqrt (((real_dist . x1,y1) ^2 ) + ((real_dist . x2,y2) ^2 ))
uniqueness
for b1, b2 being Function of [:[:REAL ,REAL :],[:REAL ,REAL :]:],REAL st ( 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
b1 . x,y = sqrt (((real_dist . x1,y1) ^2 ) + ((real_dist . x2,y2) ^2 )) ) & ( 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
b2 . x,y = sqrt (((real_dist . x1,y1) ^2 ) + ((real_dist . x2,y2) ^2 )) ) holds
b1 = b2
end;
:: deftheorem Def9 defines Eukl_dist2 METRIC_3:def 18 :
for b1 being Function of [:[:REAL ,REAL :],[:REAL ,REAL :]:],REAL holds
( b1 = Eukl_dist2 iff 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
b1 . x,y = sqrt (((real_dist . x1,y1) ^2 ) + ((real_dist . x2,y2) ^2 )) );
theorem Th22:
theorem Th23:
theorem Th24:
:: deftheorem defines EuklSpace2 METRIC_3:def 19 :
EuklSpace2 = MetrStruct(# [:REAL ,REAL :],Eukl_dist2 #);
definition
func taxi_dist3 -> Function of
[:[:REAL ,REAL ,REAL :],[:REAL ,REAL ,REAL :]:],
REAL means :
Def11:
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);
existence
ex b1 being Function of [:[:REAL ,REAL ,REAL :],[:REAL ,REAL ,REAL :]:],REAL st
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
b1 . x,y = ((real_dist . x1,y1) + (real_dist . x2,y2)) + (real_dist . x3,y3)
uniqueness
for b1, b2 being Function of [:[:REAL ,REAL ,REAL :],[:REAL ,REAL ,REAL :]:],REAL st ( 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
b1 . x,y = ((real_dist . x1,y1) + (real_dist . x2,y2)) + (real_dist . x3,y3) ) & ( 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
b2 . x,y = ((real_dist . x1,y1) + (real_dist . x2,y2)) + (real_dist . x3,y3) ) holds
b1 = b2
end;
:: deftheorem Def11 defines taxi_dist3 METRIC_3:def 20 :
for b1 being Function of [:[:REAL ,REAL ,REAL :],[:REAL ,REAL ,REAL :]:],REAL holds
( b1 = taxi_dist3 iff 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
b1 . x,y = ((real_dist . x1,y1) + (real_dist . x2,y2)) + (real_dist . x3,y3) );
theorem Th25:
theorem Th26:
theorem Th27:
:: deftheorem defines RealSpaceCart3 METRIC_3:def 21 :
RealSpaceCart3 = MetrStruct(# [:REAL ,REAL ,REAL :],taxi_dist3 #);
definition
func Eukl_dist3 -> Function of
[:[:REAL ,REAL ,REAL :],[:REAL ,REAL ,REAL :]:],
REAL means :
Def13:
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 ));
existence
ex b1 being Function of [:[:REAL ,REAL ,REAL :],[:REAL ,REAL ,REAL :]:],REAL st
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
b1 . x,y = sqrt ((((real_dist . x1,y1) ^2 ) + ((real_dist . x2,y2) ^2 )) + ((real_dist . x3,y3) ^2 ))
uniqueness
for b1, b2 being Function of [:[:REAL ,REAL ,REAL :],[:REAL ,REAL ,REAL :]:],REAL st ( 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
b1 . x,y = sqrt ((((real_dist . x1,y1) ^2 ) + ((real_dist . x2,y2) ^2 )) + ((real_dist . x3,y3) ^2 )) ) & ( 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
b2 . x,y = sqrt ((((real_dist . x1,y1) ^2 ) + ((real_dist . x2,y2) ^2 )) + ((real_dist . x3,y3) ^2 )) ) holds
b1 = b2
end;
:: deftheorem Def13 defines Eukl_dist3 METRIC_3:def 22 :
for b1 being Function of [:[:REAL ,REAL ,REAL :],[:REAL ,REAL ,REAL :]:],REAL holds
( b1 = Eukl_dist3 iff 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
b1 . x,y = sqrt ((((real_dist . x1,y1) ^2 ) + ((real_dist . x2,y2) ^2 )) + ((real_dist . x3,y3) ^2 )) );
theorem Th28:
theorem Th29:
theorem Th30:
:: deftheorem defines EuklSpace3 METRIC_3:def 23 :
EuklSpace3 = MetrStruct(# [:REAL ,REAL ,REAL :],Eukl_dist3 #);