:: by Stanis{\l}awa Kanas and Jan Stankiewicz

::

:: Received September 27, 1990

:: Copyright (c) 1990-2017 Association of Mizar Users

scheme :: METRIC_3:sch 1

LambdaMCART{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}() -> non empty set , F_{4}( object , object , object , object ) -> Element of F_{3}() } :

LambdaMCART{ F

ex f being Function of [:[:F_{1}(),F_{2}():],[:F_{1}(),F_{2}():]:],F_{3}() st

for x1, y1 being Element of F_{1}()

for x2, y2 being Element of F_{2}()

for x, y being Element of [:F_{1}(),F_{2}():] st x = [x1,x2] & y = [y1,y2] holds

f . (x,y) = F_{4}(x1,y1,x2,y2)

for x1, y1 being Element of F

for x2, y2 being Element of F

for x, y being Element of [:F

f . (x,y) = F

proof end;

definition

let X, Y be non empty MetrSpace;

ex b_{1} 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

b_{1} . (x,y) = (dist (x1,y1)) + (dist (x2,y2))

for b_{1}, b_{2} 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

b_{1} . (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

b_{2} . (x,y) = (dist (x1,y1)) + (dist (x2,y2)) ) holds

b_{1} = b_{2}

end;
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 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));

ex b

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

b

proof end;

uniqueness for b

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

b

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

b

b

proof end;

:: deftheorem Def1 defines dist_cart2 METRIC_3:def 1 :

for X, Y being non empty MetrSpace

for b_{3} being Function of [:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:],REAL holds

( b_{3} = 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

b_{3} . (x,y) = (dist (x1,y1)) + (dist (x2,y2)) );

for X, Y being non empty MetrSpace

for b

( b

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

b

theorem Th1: :: METRIC_3:1

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 )

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 Th2: :: METRIC_3:2

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)

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 Th3: :: METRIC_3:3

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))

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:];

coherence

(dist_cart2 (X,Y)) . (x,y) is Real ;

end;
let x, y be Element of [: the carrier of X, the carrier of Y:];

coherence

(dist_cart2 (X,Y)) . (x,y) is Real ;

:: 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);

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;

coherence

not MetrStruct(# A,r #) is empty ;

end;
let r be Function of [:A,A:],REAL;

coherence

not MetrStruct(# A,r #) is empty ;

definition

let X, Y be non empty MetrSpace;

MetrStruct(# [: the carrier of X, the carrier of Y:],(dist_cart2 (X,Y)) #) is non empty strict MetrSpace

end;
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)) #);

MetrStruct(# [: the carrier of X, the carrier of Y:],(dist_cart2 (X,Y)) #) is non empty strict MetrSpace

proof 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)) #);

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{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}() -> non empty set , F_{4}() -> non empty set , F_{5}( object , object , object , object , object , object ) -> Element of F_{4}() } :

LambdaMCART1{ F

ex f being Function of [:[:F_{1}(),F_{2}(),F_{3}():],[:F_{1}(),F_{2}(),F_{3}():]:],F_{4}() st

for x1, y1 being Element of F_{1}()

for x2, y2 being Element of F_{2}()

for x3, y3 being Element of F_{3}()

for x, y being Element of [:F_{1}(),F_{2}(),F_{3}():] st x = [x1,x2,x3] & y = [y1,y2,y3] holds

f . (x,y) = F_{5}(x1,y1,x2,y2,x3,y3)

for x1, y1 being Element of F

for x2, y2 being Element of F

for x3, y3 being Element of F

for x, y being Element of [:F

f . (x,y) = F

proof end;

definition

let X, Y, Z be non empty MetrSpace;

ex b_{1} 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

b_{1} . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + (dist (x3,y3))

for b_{1}, b_{2} 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

b_{1} . (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

b_{2} . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + (dist (x3,y3)) ) holds

b_{1} = b_{2}

end;
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 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));

ex b

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

b

proof end;

uniqueness for b

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

b

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

b

b

proof end;

:: deftheorem Def4 defines dist_cart3 METRIC_3:def 4 :

for X, Y, Z being non empty MetrSpace

for b_{4} 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

( b_{4} = 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

b_{4} . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + (dist (x3,y3)) );

for X, Y, Z being non empty MetrSpace

for b

( b

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

b

theorem Th4: :: METRIC_3:4

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 )

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 Th5: :: METRIC_3:5

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)

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 Th6: :: METRIC_3:6

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))

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;

MetrStruct(# [: the carrier of X, the carrier of Y, the carrier of Z:],(dist_cart3 (X,Y,Z)) #) is non empty strict MetrSpace

end;
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)) #);

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;

:: 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)) #);

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:];

coherence

(dist_cart3 (X,Y,Z)) . (x,y) is Real ;

end;
let x, y be Element of [: the carrier of X, the carrier of Y, the carrier of Z:];

coherence

(dist_cart3 (X,Y,Z)) . (x,y) is Real ;

:: 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);

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{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}() -> non empty set , F_{4}() -> non empty set , F_{5}() -> non empty set , F_{6}( object , object , object , object , object , object , object , object ) -> Element of F_{5}() } :

LambdaMCART2{ F

ex f being Function of [:[:F_{1}(),F_{2}(),F_{3}(),F_{4}():],[:F_{1}(),F_{2}(),F_{3}(),F_{4}():]:],F_{5}() st

for x1, y1 being Element of F_{1}()

for x2, y2 being Element of F_{2}()

for x3, y3 being Element of F_{3}()

for x4, y4 being Element of F_{4}()

for x, y being Element of [:F_{1}(),F_{2}(),F_{3}(),F_{4}():] st x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4] holds

f . (x,y) = F_{6}(x1,y1,x2,y2,x3,y3,x4,y4)

for x1, y1 being Element of F

for x2, y2 being Element of F

for x3, y3 being Element of F

for x4, y4 being Element of F

for x, y being Element of [:F

f . (x,y) = F

proof end;

definition

let X, Y, Z, W be non empty MetrSpace;

ex b_{1} 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

b_{1} . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + ((dist (x3,y3)) + (dist (x4,y4)))

for b_{1}, b_{2} 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

b_{1} . (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

b_{2} . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + ((dist (x3,y3)) + (dist (x4,y4))) ) holds

b_{1} = b_{2}

end;
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 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)));

ex b

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

b

proof end;

uniqueness for b

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

b

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

b

b

proof end;

:: deftheorem Def7 defines dist_cart4 METRIC_3:def 7 :

for X, Y, Z, W being non empty MetrSpace

for b_{5} 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

( b_{5} = 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

b_{5} . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + ((dist (x3,y3)) + (dist (x4,y4))) );

for X, Y, Z, W being non empty MetrSpace

for b

( b

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

b

theorem Th7: :: METRIC_3:7

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 )

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 Th8: :: METRIC_3:8

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)

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 Th9: :: METRIC_3:9

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))

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;

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;
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)) #);

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;

:: 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)) #);

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:];

coherence

(dist_cart4 (X,Y,Z,W)) . (x,y) is Real ;

end;
let x, y be Element of [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:];

coherence

(dist_cart4 (X,Y,Z,W)) . (x,y) is Real ;

:: 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);

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);

definition

let X, Y be non empty MetrSpace;

ex b_{1} 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

b_{1} . (x,y) = sqrt (((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2))

for b_{1}, b_{2} 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

b_{1} . (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

b_{2} . (x,y) = sqrt (((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) ) holds

b_{1} = b_{2}

end;
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 :Def10: :: 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));

existence 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));

ex b

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

b

proof end;

uniqueness for b

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

b

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

b

b

proof end;

:: deftheorem Def10 defines dist_cart2S METRIC_3:def 10 :

for X, Y being non empty MetrSpace

for b_{3} being Function of [:[: the carrier of X, the carrier of Y:],[: the carrier of X, the carrier of Y:]:],REAL holds

( b_{3} = 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

b_{3} . (x,y) = sqrt (((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) );

for X, Y being non empty MetrSpace

for b

( b

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

b

Lm1: for a, b being Real st 0 <= a & 0 <= b holds

( sqrt (a + b) = 0 iff ( a = 0 & b = 0 ) )

by SQUARE_1:31;

theorem Th10: :: METRIC_3:10

for X, Y being non empty MetrSpace

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 )

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 )

proof end;

theorem Th11: :: METRIC_3:11

for X, Y being non empty MetrSpace

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)

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)

proof end;

theorem Th12: :: 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)))

sqrt (((a + c) ^2) + ((b + d) ^2)) <= (sqrt ((a ^2) + (b ^2))) + (sqrt ((c ^2) + (d ^2)))

proof end;

theorem Th13: :: METRIC_3:13

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))

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))

proof end;

definition

let X, Y be non empty MetrSpace;

let x, y be Element of [: the carrier of X, the carrier of Y:];

coherence

(dist_cart2S (X,Y)) . (x,y) is Real ;

end;
let x, y be Element of [: the carrier of X, the carrier of Y:];

coherence

(dist_cart2S (X,Y)) . (x,y) is Real ;

:: 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);

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);

definition

let X, Y be non empty MetrSpace;

MetrStruct(# [: the carrier of X, the carrier of Y:],(dist_cart2S (X,Y)) #) is non empty strict MetrSpace

end;
func MetrSpaceCart2S (X,Y) -> non empty strict MetrSpace equals :: METRIC_3:def 12

MetrStruct(# [: the carrier of X, the carrier of Y:],(dist_cart2S (X,Y)) #);

coherence MetrStruct(# [: the carrier of X, the carrier of Y:],(dist_cart2S (X,Y)) #);

MetrStruct(# [: the carrier of X, the carrier of Y:],(dist_cart2S (X,Y)) #) is non empty strict MetrSpace

proof end;

:: 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)) #);

for X, Y being non empty MetrSpace holds MetrSpaceCart2S (X,Y) = MetrStruct(# [: the carrier of X, the carrier of Y:],(dist_cart2S (X,Y)) #);

definition

let X, Y, Z be non empty MetrSpace;

ex b_{1} 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

b_{1} . (x,y) = sqrt ((((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) + ((dist (x3,y3)) ^2))

for b_{1}, b_{2} 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

b_{1} . (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

b_{2} . (x,y) = sqrt ((((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) + ((dist (x3,y3)) ^2)) ) holds

b_{1} = b_{2}

end;
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 :Def13: :: 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));

existence 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));

ex b

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

b

proof end;

uniqueness for b

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

b

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

b

b

proof end;

:: deftheorem Def13 defines dist_cart3S METRIC_3:def 13 :

for X, Y, Z being non empty MetrSpace

for b_{4} 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

( b_{4} = 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

b_{4} . (x,y) = sqrt ((((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) + ((dist (x3,y3)) ^2)) );

for X, Y, Z being non empty MetrSpace

for b

( b

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

b

theorem Th14: :: METRIC_3: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

( (dist_cart3S (X,Y,Z)) . (x,y) = 0 iff x = y )

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 )

proof end;

theorem Th15: :: METRIC_3:15

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)

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)

proof end;

theorem Th16: :: 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)

proof end;

theorem Th17: :: 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))

proof end;

Lm2: for a, b, c, d, e, f being Real 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)))

proof end;

theorem Th18: :: METRIC_3:18

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))

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))

proof end;

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:];

coherence

(dist_cart3S (X,Y,Z)) . (x,y) is Real ;

end;
let x, y be Element of [: the carrier of X, the carrier of Y, the carrier of Z:];

coherence

(dist_cart3S (X,Y,Z)) . (x,y) is Real ;

:: 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);

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;

MetrStruct(# [: the carrier of X, the carrier of Y, the carrier of Z:],(dist_cart3S (X,Y,Z)) #) is non empty strict MetrSpace

end;
func MetrSpaceCart3S (X,Y,Z) -> non empty strict MetrSpace equals :: METRIC_3:def 15

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)) #);

MetrStruct(# [: the carrier of X, the carrier of Y, the carrier of Z:],(dist_cart3S (X,Y,Z)) #) is non empty strict MetrSpace

proof 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)) #);

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

ex b_{1} 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

b_{1} . (x,y) = (real_dist . (x1,y1)) + (real_dist . (x2,y2))

for b_{1}, b_{2} 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

b_{1} . (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

b_{2} . (x,y) = (real_dist . (x1,y1)) + (real_dist . (x2,y2)) ) holds

b_{1} = b_{2}
end;

func taxi_dist2 -> Function of [:[:REAL,REAL:],[:REAL,REAL:]:],REAL means :Def16: :: 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));

existence 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));

ex b

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

b

proof end;

uniqueness for b

for x, y being Element of [:REAL,REAL:] st x = [x1,x2] & y = [y1,y2] holds

b

for x, y being Element of [:REAL,REAL:] st x = [x1,x2] & y = [y1,y2] holds

b

b

proof end;

:: deftheorem Def16 defines taxi_dist2 METRIC_3:def 16 :

for b_{1} being Function of [:[:REAL,REAL:],[:REAL,REAL:]:],REAL holds

( b_{1} = 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

b_{1} . (x,y) = (real_dist . (x1,y1)) + (real_dist . (x2,y2)) );

for b

( b

for x, y being Element of [:REAL,REAL:] st x = [x1,x2] & y = [y1,y2] holds

b

theorem Th21: :: 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))

proof end;

definition

MetrStruct(# [:REAL,REAL:],taxi_dist2 #) is non empty strict MetrSpace
end;

func RealSpaceCart2 -> non empty strict MetrSpace equals :: METRIC_3:def 17

MetrStruct(# [:REAL,REAL:],taxi_dist2 #);

coherence MetrStruct(# [:REAL,REAL:],taxi_dist2 #);

MetrStruct(# [:REAL,REAL:],taxi_dist2 #) is non empty strict MetrSpace

proof end;

:: deftheorem defines RealSpaceCart2 METRIC_3:def 17 :

RealSpaceCart2 = MetrStruct(# [:REAL,REAL:],taxi_dist2 #);

RealSpaceCart2 = MetrStruct(# [:REAL,REAL:],taxi_dist2 #);

definition

ex b_{1} 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

b_{1} . (x,y) = sqrt (((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2))

for b_{1}, b_{2} 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

b_{1} . (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

b_{2} . (x,y) = sqrt (((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) ) holds

b_{1} = b_{2}
end;

func Eukl_dist2 -> Function of [:[:REAL,REAL:],[:REAL,REAL:]:],REAL means :Def18: :: 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));

existence 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));

ex b

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

b

proof end;

uniqueness for b

for x, y being Element of [:REAL,REAL:] st x = [x1,x2] & y = [y1,y2] holds

b

for x, y being Element of [:REAL,REAL:] st x = [x1,x2] & y = [y1,y2] holds

b

b

proof end;

:: deftheorem Def18 defines Eukl_dist2 METRIC_3:def 18 :

for b_{1} being Function of [:[:REAL,REAL:],[:REAL,REAL:]:],REAL holds

( b_{1} = 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

b_{1} . (x,y) = sqrt (((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) );

for b

( b

for x, y being Element of [:REAL,REAL:] st x = [x1,x2] & y = [y1,y2] holds

b

theorem Th24: :: 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))

proof end;

definition

MetrStruct(# [:REAL,REAL:],Eukl_dist2 #) is non empty strict MetrSpace
end;

func EuklSpace2 -> non empty strict MetrSpace equals :: METRIC_3:def 19

MetrStruct(# [:REAL,REAL:],Eukl_dist2 #);

coherence MetrStruct(# [:REAL,REAL:],Eukl_dist2 #);

MetrStruct(# [:REAL,REAL:],Eukl_dist2 #) is non empty strict MetrSpace

proof end;

:: deftheorem defines EuklSpace2 METRIC_3:def 19 :

EuklSpace2 = MetrStruct(# [:REAL,REAL:],Eukl_dist2 #);

EuklSpace2 = MetrStruct(# [:REAL,REAL:],Eukl_dist2 #);

definition

ex b_{1} 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

b_{1} . (x,y) = ((real_dist . (x1,y1)) + (real_dist . (x2,y2))) + (real_dist . (x3,y3))

for b_{1}, b_{2} 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

b_{1} . (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

b_{2} . (x,y) = ((real_dist . (x1,y1)) + (real_dist . (x2,y2))) + (real_dist . (x3,y3)) ) holds

b_{1} = b_{2}
end;

func taxi_dist3 -> Function of [:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:],REAL means :Def20: :: 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));

existence 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));

ex b

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

b

proof end;

uniqueness for b

for x, y being Element of [:REAL,REAL,REAL:] st x = [x1,x2,x3] & y = [y1,y2,y3] holds

b

for x, y being Element of [:REAL,REAL,REAL:] st x = [x1,x2,x3] & y = [y1,y2,y3] holds

b

b

proof end;

:: deftheorem Def20 defines taxi_dist3 METRIC_3:def 20 :

for b_{1} being Function of [:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:],REAL holds

( b_{1} = 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

b_{1} . (x,y) = ((real_dist . (x1,y1)) + (real_dist . (x2,y2))) + (real_dist . (x3,y3)) );

for b

( b

for x, y being Element of [:REAL,REAL,REAL:] st x = [x1,x2,x3] & y = [y1,y2,y3] holds

b

theorem Th27: :: 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))

proof end;

definition

MetrStruct(# [:REAL,REAL,REAL:],taxi_dist3 #) is non empty strict MetrSpace
end;

func RealSpaceCart3 -> non empty strict MetrSpace equals :: METRIC_3:def 21

MetrStruct(# [:REAL,REAL,REAL:],taxi_dist3 #);

coherence MetrStruct(# [:REAL,REAL,REAL:],taxi_dist3 #);

MetrStruct(# [:REAL,REAL,REAL:],taxi_dist3 #) is non empty strict MetrSpace

proof end;

:: deftheorem defines RealSpaceCart3 METRIC_3:def 21 :

RealSpaceCart3 = MetrStruct(# [:REAL,REAL,REAL:],taxi_dist3 #);

RealSpaceCart3 = MetrStruct(# [:REAL,REAL,REAL:],taxi_dist3 #);

definition

ex b_{1} 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

b_{1} . (x,y) = sqrt ((((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) + ((real_dist . (x3,y3)) ^2))

for b_{1}, b_{2} 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

b_{1} . (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

b_{2} . (x,y) = sqrt ((((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) + ((real_dist . (x3,y3)) ^2)) ) holds

b_{1} = b_{2}
end;

func Eukl_dist3 -> Function of [:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:],REAL means :Def22: :: 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));

existence 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));

ex b

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

b

proof end;

uniqueness for b

for x, y being Element of [:REAL,REAL,REAL:] st x = [x1,x2,x3] & y = [y1,y2,y3] holds

b

for x, y being Element of [:REAL,REAL,REAL:] st x = [x1,x2,x3] & y = [y1,y2,y3] holds

b

b

proof end;

:: deftheorem Def22 defines Eukl_dist3 METRIC_3:def 22 :

for b_{1} being Function of [:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:],REAL holds

( b_{1} = 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

b_{1} . (x,y) = sqrt ((((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) + ((real_dist . (x3,y3)) ^2)) );

for b

( b

for x, y being Element of [:REAL,REAL,REAL:] st x = [x1,x2,x3] & y = [y1,y2,y3] holds

b

theorem Th30: :: 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))

proof end;

definition

MetrStruct(# [:REAL,REAL,REAL:],Eukl_dist3 #) is non empty strict MetrSpace
end;

func EuklSpace3 -> non empty strict MetrSpace equals :: METRIC_3:def 23

MetrStruct(# [:REAL,REAL,REAL:],Eukl_dist3 #);

coherence MetrStruct(# [:REAL,REAL,REAL:],Eukl_dist3 #);

MetrStruct(# [:REAL,REAL,REAL:],Eukl_dist3 #) is non empty strict MetrSpace

proof end;

:: deftheorem defines EuklSpace3 METRIC_3:def 23 :

EuklSpace3 = MetrStruct(# [:REAL,REAL,REAL:],Eukl_dist3 #);

EuklSpace3 = MetrStruct(# [:REAL,REAL,REAL:],Eukl_dist3 #);