metric_3.miz
begin
reserve X,Y,Z,W for non
empty
MetrSpace;
scheme ::
METRIC_3:sch1
LambdaMCART { X,Y,Z() -> non
empty
set , F(
object,
object,
object,
object) ->
Element of Z() } :
ex f be
Function of
[:
[:X(), Y():],
[:X(), Y():]:], Z() st for x1,y1 be
Element of X() holds for x2,y2 be
Element of Y() holds for x,y be
Element of
[:X(), Y():] st x
=
[x1, x2] & y
=
[y1, y2] holds (f
. (x,y))
= F(x1,y1,x2,y2);
deffunc
G(
Element of
[:X(), Y():],
Element of
[:X(), Y():]) = F(`1,`1,`2,`2);
consider f be
Function of
[:
[:X(), Y():],
[:X(), Y():]:], Z() such that
A1: for x,y be
Element of
[:X(), Y():] holds (f
. (x,y))
=
G(x,y) from
BINOP_1:sch 4;
take f;
let x1,y1 be
Element of X(), x2,y2 be
Element of Y(), x,y be
Element of
[:X(), Y():] such that
A2: x
=
[x1, x2] and
A3: y
=
[y1, y2];
A4: y1
= (y
`1 ) & y2
= (y
`2 ) by
A3;
x1
= (x
`1 ) & x2
= (x
`2 ) by
A2;
hence thesis by
A1,
A4;
end;
definition
let X, Y;
::
METRIC_3:def1
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 be
Element of X, x2,y2 be
Element of Y, x,y be
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
proof
deffunc
G(
Element of X,
Element of X,
Element of Y,
Element of Y) = (
In (((
dist ($1,$2))
+ (
dist ($3,$4))),
REAL ));
consider F be
Function of
[:
[:the
carrier of X, the
carrier of Y:],
[:the
carrier of X, the
carrier of Y:]:],
REAL such that
A1: for x1,y1 be
Element of X holds for x2,y2 be
Element of Y holds for x,y be
Element of
[:the
carrier of X, the
carrier of Y:] st x
=
[x1, x2] & y
=
[y1, y2] holds (F
. (x,y))
=
G(x1,y1,x2,y2) from
LambdaMCART;
take F;
let x1,y1 be
Element of X, x2,y2 be
Element of Y, x,y be
Element of
[:the
carrier of X, the
carrier of Y:];
assume x
=
[x1, x2] & y
=
[y1, y2];
then (F
. (x,y))
=
G(x1,y1,x2,y2) by
A1;
hence thesis;
end;
uniqueness
proof
let f1,f2 be
Function of
[:
[:the
carrier of X, the
carrier of Y:],
[:the
carrier of X, the
carrier of Y:]:],
REAL ;
assume that
A2: for x1,y1 be
Element of X holds for x2,y2 be
Element of Y holds for x,y be
Element of
[:the
carrier of X, the
carrier of Y:] st x
=
[x1, x2] & y
=
[y1, y2] holds (f1
. (x,y))
= ((
dist (x1,y1))
+ (
dist (x2,y2))) and
A3: for x1,y1 be
Element of X holds for x2,y2 be
Element of Y holds for x,y be
Element of
[:the
carrier of X, the
carrier of Y:] st x
=
[x1, x2] & y
=
[y1, y2] holds (f2
. (x,y))
= ((
dist (x1,y1))
+ (
dist (x2,y2)));
for x,y be
Element of
[:the
carrier of X, the
carrier of Y:] holds (f1
. (x,y))
= (f2
. (x,y))
proof
let x,y be
Element of
[:the
carrier of X, the
carrier of Y:];
consider x1 be
Element of X, x2 be
Element of Y such that
A4: x
=
[x1, x2] by
DOMAIN_1: 1;
consider y1 be
Element of X, y2 be
Element of Y such that
A5: y
=
[y1, y2] by
DOMAIN_1: 1;
thus (f1
. (x,y))
= ((
dist (x1,y1))
+ (
dist (x2,y2))) by
A2,
A4,
A5
.= (f2
. (x,y)) by
A3,
A4,
A5;
end;
hence thesis by
BINOP_1: 2;
end;
end
theorem ::
METRIC_3:1
Th1: for x,y be
Element of
[:the
carrier of X, the
carrier of Y:] holds ((
dist_cart2 (X,Y))
. (x,y))
=
0 iff x
= y
proof
let x,y be
Element of
[:the
carrier of X, the
carrier of Y:];
reconsider x1 = (x
`1 ), y1 = (y
`1 ) as
Element of X;
reconsider x2 = (x
`2 ), y2 = (y
`2 ) as
Element of Y;
A1: x
=
[x1, x2] & y
=
[y1, y2];
thus ((
dist_cart2 (X,Y))
. (x,y))
=
0 implies x
= y
proof
set d1 = (
dist (x1,y1)), d2 = (
dist (x2,y2));
assume ((
dist_cart2 (X,Y))
. (x,y))
=
0 ;
then
A2: (d1
+ d2)
=
0 by
A1,
Def1;
A3:
0
<= d1 &
0
<= d2 by
METRIC_1: 5;
then d1
=
0 by
A2,
XREAL_1: 27;
then
A4: x1
= y1 by
METRIC_1: 2;
d2
=
0 by
A2,
A3,
XREAL_1: 27;
hence thesis by
A1,
A4,
METRIC_1: 2;
end;
assume
A5: x
= y;
then
A6: (
dist (x2,y2))
=
0 by
METRIC_1: 1;
((
dist_cart2 (X,Y))
. (x,y))
= ((
dist (x1,y1))
+ (
dist (x2,y2))) by
A1,
Def1
.=
0 by
A5,
A6,
METRIC_1: 1;
hence thesis;
end;
theorem ::
METRIC_3:2
Th2: for x,y be
Element of
[:the
carrier of X, the
carrier of Y:] holds ((
dist_cart2 (X,Y))
. (x,y))
= ((
dist_cart2 (X,Y))
. (y,x))
proof
let x,y be
Element of
[:the
carrier of X, the
carrier of Y:];
reconsider x1 = (x
`1 ), y1 = (y
`1 ) as
Element of X;
reconsider x2 = (x
`2 ), y2 = (y
`2 ) as
Element of Y;
A1: x
=
[x1, x2] & y
=
[y1, y2];
then ((
dist_cart2 (X,Y))
. (x,y))
= ((
dist (y1,x1))
+ (
dist (x2,y2))) by
Def1
.= ((
dist_cart2 (X,Y))
. (y,x)) by
A1,
Def1;
hence thesis;
end;
theorem ::
METRIC_3:3
Th3: for x,y,z be
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
let x,y,z be
Element of
[:the
carrier of X, the
carrier of Y:];
reconsider x1 = (x
`1 ), y1 = (y
`1 ), z1 = (z
`1 ) as
Element of X;
reconsider x2 = (x
`2 ), y2 = (y
`2 ), z2 = (z
`2 ) as
Element of Y;
A1: y
=
[y1, y2];
set d6 = (
dist (y2,z2));
set d5 = (
dist (x2,y2));
set d4 = (
dist (x2,z2));
set d3 = (
dist (y1,z1));
set d2 = (
dist (x1,y1));
set d1 = (
dist (x1,z1));
A2: z
=
[z1, z2];
A3: x
=
[x1, x2];
then
A4: ((
dist_cart2 (X,Y))
. (x,z))
= (d1
+ d4) by
A2,
Def1;
A5: d1
<= (d2
+ d3) & d4
<= (d5
+ d6) by
METRIC_1: 4;
((d2
+ d3)
+ (d5
+ d6))
= ((d2
+ d5)
+ (d3
+ d6))
.= (((
dist_cart2 (X,Y))
. (x,y))
+ (d3
+ d6)) by
A3,
A1,
Def1
.= (((
dist_cart2 (X,Y))
. (x,y))
+ ((
dist_cart2 (X,Y))
. (y,z))) by
A1,
A2,
Def1;
hence thesis by
A5,
A4,
XREAL_1: 7;
end;
definition
let X, Y;
let x,y be
Element of
[:the
carrier of X, the
carrier of Y:];
::
METRIC_3:def2
func
dist2 (x,y) ->
Real equals ((
dist_cart2 (X,Y))
. (x,y));
coherence ;
end
registration
let A be non
empty
set, r be
Function of
[:A, A:],
REAL ;
cluster
MetrStruct (# A, r #) -> non
empty;
coherence ;
end
definition
let X, Y;
::
METRIC_3:def3
func
MetrSpaceCart2 (X,Y) ->
strict non
empty
MetrSpace equals
MetrStruct (#
[:the
carrier of X, the
carrier of Y:], (
dist_cart2 (X,Y)) #);
coherence
proof
set M =
MetrStruct (#
[:the
carrier of X, the
carrier of Y:], (
dist_cart2 (X,Y)) #);
now
let x,y,z be
Element of M;
A1: (
dist (x,y))
= ((
dist_cart2 (X,Y))
. (x,y)) by
METRIC_1:def 1;
hence (
dist (x,y))
=
0 iff x
= y by
Th1;
(
dist (y,x))
= ((
dist_cart2 (X,Y))
. (y,x)) by
METRIC_1:def 1;
hence (
dist (x,y))
= (
dist (y,x)) by
A1,
Th2;
(
dist (x,z))
= ((
dist_cart2 (X,Y))
. (x,z)) & (
dist (y,z))
= ((
dist_cart2 (X,Y))
. (y,z)) by
METRIC_1:def 1;
hence (
dist (x,z))
<= ((
dist (x,y))
+ (
dist (y,z))) by
A1,
Th3;
end;
hence thesis by
METRIC_1: 6;
end;
end
scheme ::
METRIC_3:sch2
LambdaMCART1 { X,Y,Z,T() -> non
empty
set , F(
object,
object,
object,
object,
object,
object) ->
Element of T() } :
ex f be
Function of
[:
[:X(), Y(), Z():],
[:X(), Y(), Z():]:], T() st for x1,y1 be
Element of X() holds for x2,y2 be
Element of Y() holds for x3,y3 be
Element of Z() holds for x,y be
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);
deffunc
G(
Element of
[:X(), Y(), Z():],
Element of
[:X(), Y(), Z():]) = F(`1_3,`1_3,`2_3,`2_3,`3_3,`3_3);
consider f be
Function of
[:
[:X(), Y(), Z():],
[:X(), Y(), Z():]:], T() such that
A1: for x,y be
Element of
[:X(), Y(), Z():] holds (f
. (x,y))
=
G(x,y) from
BINOP_1:sch 4;
take f;
let x1,y1 be
Element of X(), x2,y2 be
Element of Y(), x3,y3 be
Element of Z(), x,y be
Element of
[:X(), Y(), Z():] such that
A2: x
=
[x1, x2, x3] and
A3: y
=
[y1, y2, y3];
A5: y1
= (y
`1_3 ) & y2
= (y
`2_3 ) by
A3;
A7: x3
= (x
`3_3 ) by
A2;
A8: y3
= (y
`3_3 ) by
A3;
x1
= (x
`1_3 ) & x2
= (x
`2_3 ) by
A2;
hence thesis by
A1,
A5,
A7,
A8;
end;
definition
let X, Y, Z;
::
METRIC_3:def4
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 be
Element of X holds for x2,y2 be
Element of Y holds for x3,y3 be
Element of Z holds for x,y be
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
proof
deffunc
G(
Element of X,
Element of X,
Element of Y,
Element of Y,
Element of Z,
Element of Z) = (
In ((((
dist ($1,$2))
+ (
dist ($3,$4)))
+ (
dist ($5,$6))),
REAL ));
consider F be
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 such that
A1: for x1,y1 be
Element of X holds for x2,y2 be
Element of Y holds for x3,y3 be
Element of Z holds for x,y be
Element of
[:the
carrier of X, the
carrier of Y, the
carrier of Z:] st x
=
[x1, x2, x3] & y
=
[y1, y2, y3] holds (F
. (x,y))
=
G(x1,y1,x2,y2,x3,y3) from
LambdaMCART1;
take F;
let x1,y1 be
Element of X, x2,y2 be
Element of Y, x3,y3 be
Element of Z, x,y be
Element of
[:the
carrier of X, the
carrier of Y, the
carrier of Z:];
assume x
=
[x1, x2, x3] & y
=
[y1, y2, y3];
then (F
. (x,y))
=
G(x1,y1,x2,y2,x3,y3) by
A1;
hence thesis;
end;
uniqueness
proof
let f1,f2 be
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 ;
assume that
A2: for x1,y1 be
Element of X holds for x2,y2 be
Element of Y holds for x3,y3 be
Element of Z holds for x,y be
Element of
[:the
carrier of X, the
carrier of Y, the
carrier of Z:] st x
=
[x1, x2, x3] & y
=
[y1, y2, y3] holds (f1
. (x,y))
= (((
dist (x1,y1))
+ (
dist (x2,y2)))
+ (
dist (x3,y3))) and
A3: for x1,y1 be
Element of X holds for x2,y2 be
Element of Y holds for x3,y3 be
Element of Z holds for x,y be
Element of
[:the
carrier of X, the
carrier of Y, the
carrier of Z:] st x
=
[x1, x2, x3] & y
=
[y1, y2, y3] holds (f2
. (x,y))
= (((
dist (x1,y1))
+ (
dist (x2,y2)))
+ (
dist (x3,y3)));
for x,y be
Element of
[:the
carrier of X, the
carrier of Y, the
carrier of Z:] holds (f1
. (x,y))
= (f2
. (x,y))
proof
let x,y be
Element of
[:the
carrier of X, the
carrier of Y, the
carrier of Z:];
consider x1 be
Element of X, x2 be
Element of Y, x3 be
Element of Z such that
A4: x
=
[x1, x2, x3] by
DOMAIN_1: 3;
consider y1 be
Element of X, y2 be
Element of Y, y3 be
Element of Z such that
A5: y
=
[y1, y2, y3] by
DOMAIN_1: 3;
thus (f1
. (x,y))
= (((
dist (x1,y1))
+ (
dist (x2,y2)))
+ (
dist (x3,y3))) by
A2,
A4,
A5
.= (f2
. (x,y)) by
A3,
A4,
A5;
end;
hence thesis by
BINOP_1: 2;
end;
end
theorem ::
METRIC_3:4
Th4: for x,y be
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
let x,y be
Element of
[:the
carrier of X, the
carrier of Y, the
carrier of Z:];
reconsider x1 = (x
`1_3 ), y1 = (y
`1_3 ) as
Element of X;
reconsider x2 = (x
`2_3 ), y2 = (y
`2_3 ) as
Element of Y;
reconsider x3 = (x
`3_3 ), y3 = (y
`3_3 ) as
Element of Z;
A1: x
=
[x1, x2, x3] & y
=
[y1, y2, y3];
thus ((
dist_cart3 (X,Y,Z))
. (x,y))
=
0 implies x
= y
proof
set d3 = (
dist (x3,y3));
set d2 = (
dist (x2,y2));
set d1 = (
dist (x1,y1));
set d4 = (d1
+ d2);
assume ((
dist_cart3 (X,Y,Z))
. (x,y))
=
0 ;
then
A2: (d4
+ d3)
=
0 by
A1,
Def4;
A3:
0
<= d1 &
0
<= d2 by
METRIC_1: 5;
then
A4:
0
<= d3 & (
0
+
0 )
<= (d1
+ d2) by
METRIC_1: 5,
XREAL_1: 7;
then
A5: d4
=
0 by
A2,
XREAL_1: 27;
then d1
=
0 by
A3,
XREAL_1: 27;
then
A6: x1
= y1 by
METRIC_1: 2;
d3
=
0 by
A2,
A4,
XREAL_1: 27;
then
A7: x3
= y3 by
METRIC_1: 2;
d2
=
0 by
A3,
A5,
XREAL_1: 27;
hence thesis by
A1,
A7,
A6,
METRIC_1: 2;
end;
assume
A8: x
= y;
then
A9: (
dist (x1,y1))
=
0 & (
dist (x2,y2))
=
0 by
METRIC_1: 1;
((
dist_cart3 (X,Y,Z))
. (x,y))
= (((
dist (x1,y1))
+ (
dist (x2,y2)))
+ (
dist (x3,y3))) by
A1,
Def4
.=
0 by
A8,
A9,
METRIC_1: 1;
hence thesis;
end;
theorem ::
METRIC_3:5
Th5: for x,y be
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
let x,y be
Element of
[:the
carrier of X, the
carrier of Y, the
carrier of Z:];
reconsider x1 = (x
`1_3 ), y1 = (y
`1_3 ) as
Element of X;
reconsider x2 = (x
`2_3 ), y2 = (y
`2_3 ) as
Element of Y;
reconsider x3 = (x
`3_3 ), y3 = (y
`3_3 ) as
Element of Z;
A1: x
=
[x1, x2, x3] & y
=
[y1, y2, y3];
then ((
dist_cart3 (X,Y,Z))
. (x,y))
= (((
dist (y1,x1))
+ (
dist (y2,x2)))
+ (
dist (y3,x3))) by
Def4
.= ((
dist_cart3 (X,Y,Z))
. (y,x)) by
A1,
Def4;
hence thesis;
end;
theorem ::
METRIC_3:6
Th6: for x,y,z be
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
let x,y,z be
Element of
[:the
carrier of X, the
carrier of Y, the
carrier of Z:];
reconsider x1 = (x
`1_3 ), y1 = (y
`1_3 ), z1 = (z
`1_3 ) as
Element of X;
reconsider x2 = (x
`2_3 ), y2 = (y
`2_3 ), z2 = (z
`2_3 ) as
Element of Y;
reconsider x3 = (x
`3_3 ), y3 = (y
`3_3 ), z3 = (z
`3_3 ) as
Element of Z;
A1: x
=
[x1, x2, x3];
set d4 = (
dist (x2,z2)), d5 = (
dist (x2,y2)), d6 = (
dist (y2,z2));
A2: z
=
[z1, z2, z3];
set d7 = (
dist (x3,z3)), d8 = (
dist (x3,y3)), d9 = (
dist (y3,z3));
set d1 = (
dist (x1,z1)), d2 = (
dist (x1,y1)), d3 = (
dist (y1,z1));
A3: y
=
[y1, y2, y3];
set d10 = (d1
+ d4);
d1
<= (d2
+ d3) & d4
<= (d5
+ d6) by
METRIC_1: 4;
then
A4: d10
<= ((d2
+ d3)
+ (d5
+ d6)) by
XREAL_1: 7;
d7
<= (d8
+ d9) by
METRIC_1: 4;
then
A5: (d10
+ d7)
<= (((d2
+ d3)
+ (d5
+ d6))
+ (d8
+ d9)) by
A4,
XREAL_1: 7;
(((d2
+ d3)
+ (d5
+ d6))
+ (d8
+ d9))
= (((d2
+ d5)
+ d8)
+ ((d3
+ d6)
+ d9))
.= (((
dist_cart3 (X,Y,Z))
. (x,y))
+ ((d3
+ d6)
+ d9)) by
A1,
A3,
Def4
.= (((
dist_cart3 (X,Y,Z))
. (x,y))
+ ((
dist_cart3 (X,Y,Z))
. (y,z))) by
A3,
A2,
Def4;
hence thesis by
A1,
A2,
A5,
Def4;
end;
definition
let X, Y, Z;
::
METRIC_3:def5
func
MetrSpaceCart3 (X,Y,Z) ->
strict non
empty
MetrSpace equals
MetrStruct (#
[:the
carrier of X, the
carrier of Y, the
carrier of Z:], (
dist_cart3 (X,Y,Z)) #);
coherence
proof
set M =
MetrStruct (#
[:the
carrier of X, the
carrier of Y, the
carrier of Z:], (
dist_cart3 (X,Y,Z)) #);
now
let x,y,z be
Element of M;
A1: (
dist (x,y))
= ((
dist_cart3 (X,Y,Z))
. (x,y)) by
METRIC_1:def 1;
hence (
dist (x,y))
=
0 iff x
= y by
Th4;
(
dist (y,x))
= ((
dist_cart3 (X,Y,Z))
. (y,x)) by
METRIC_1:def 1;
hence (
dist (x,y))
= (
dist (y,x)) by
A1,
Th5;
(
dist (x,z))
= ((
dist_cart3 (X,Y,Z))
. (x,z)) & (
dist (y,z))
= ((
dist_cart3 (X,Y,Z))
. (y,z)) by
METRIC_1:def 1;
hence (
dist (x,z))
<= ((
dist (x,y))
+ (
dist (y,z))) by
A1,
Th6;
end;
hence thesis by
METRIC_1: 6;
end;
end
definition
let X, Y, Z;
let x,y be
Element of
[:the
carrier of X, the
carrier of Y, the
carrier of Z:];
::
METRIC_3:def6
func
dist3 (x,y) ->
Real equals ((
dist_cart3 (X,Y,Z))
. (x,y));
coherence ;
end
scheme ::
METRIC_3:sch3
LambdaMCART2 { X,Y,Z,W,T() -> non
empty
set , F(
object,
object,
object,
object,
object,
object,
object,
object) ->
Element of T() } :
ex f be
Function of
[:
[:X(), Y(), Z(), W():],
[:X(), Y(), Z(), W():]:], T() st for x1,y1 be
Element of X() holds for x2,y2 be
Element of Y() holds for x3,y3 be
Element of Z() holds for x4,y4 be
Element of W() holds for x,y be
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);
deffunc
G(
Element of
[:X(), Y(), Z(), W():],
Element of
[:X(), Y(), Z(), W():]) = F(`1_4,`1_4,`2_4,`2_4,`3_4,`3_4,`4_4,`4_4);
consider f be
Function of
[:
[:X(), Y(), Z(), W():],
[:X(), Y(), Z(), W():]:], T() such that
A1: for x,y be
Element of
[:X(), Y(), Z(), W():] holds (f
. (x,y))
=
G(x,y) from
BINOP_1:sch 4;
take f;
let x1,y1 be
Element of X(), x2,y2 be
Element of Y(), x3,y3 be
Element of Z(), x4,y4 be
Element of W(), x,y be
Element of
[:X(), Y(), Z(), W():] such that
A2: x
=
[x1, x2, x3, x4] and
A3: y
=
[y1, y2, y3, y4];
A5: y1
= (y
`1_4 ) & y2
= (y
`2_4 ) by
A3;
A7: x3
= (x
`3_4 ) & x4
= (x
`4_4 ) by
A2;
A8: y3
= (y
`3_4 ) & y4
= (y
`4_4 ) by
A3;
x1
= (x
`1_4 ) & x2
= (x
`2_4 ) by
A2;
hence thesis by
A1,
A5,
A7,
A8;
end;
definition
let X, Y, Z, W;
::
METRIC_3:def7
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 be
Element of X holds for x2,y2 be
Element of Y holds for x3,y3 be
Element of Z holds for x4,y4 be
Element of W holds for x,y be
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
proof
deffunc
G(
Element of X,
Element of X,
Element of Y,
Element of Y,
Element of Z,
Element of Z,
Element of W,
Element of W) = (
In ((((
dist ($1,$2))
+ (
dist ($3,$4)))
+ ((
dist ($5,$6))
+ (
dist ($7,$8)))),
REAL ));
consider F be
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 such that
A1: for x1,y1 be
Element of X holds for x2,y2 be
Element of Y holds for x3,y3 be
Element of Z holds for x4,y4 be
Element of W holds for x,y be
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 (F
. (x,y))
=
G(x1,y1,x2,y2,x3,y3,x4,y4) from
LambdaMCART2;
take F;
let x1,y1 be
Element of X, x2,y2 be
Element of Y, x3,y3 be
Element of Z, x4,y4 be
Element of W, x,y be
Element of
[:the
carrier of X, the
carrier of Y, the
carrier of Z, the
carrier of W:];
assume x
=
[x1, x2, x3, x4] & y
=
[y1, y2, y3, y4];
then (F
. (x,y))
=
G(x1,y1,x2,y2,x3,y3,x4,y4) by
A1;
hence thesis;
end;
uniqueness
proof
let f1,f2 be
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 ;
assume that
A2: for x1,y1 be
Element of X, x2,y2 be
Element of Y, x3,y3 be
Element of Z, x4,y4 be
Element of W, x,y be
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 (f1
. (x,y))
= (((
dist (x1,y1))
+ (
dist (x2,y2)))
+ ((
dist (x3,y3))
+ (
dist (x4,y4)))) and
A3: for x1,y1 be
Element of X, x2,y2 be
Element of Y, x3,y3 be
Element of Z, x4,y4 be
Element of W holds for x,y be
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 (f2
. (x,y))
= (((
dist (x1,y1))
+ (
dist (x2,y2)))
+ ((
dist (x3,y3))
+ (
dist (x4,y4))));
for x,y be
Element of
[:the
carrier of X, the
carrier of Y, the
carrier of Z, the
carrier of W:] holds (f1
. (x,y))
= (f2
. (x,y))
proof
let x,y be
Element of
[:the
carrier of X, the
carrier of Y, the
carrier of Z, the
carrier of W:];
consider x1 be
Element of X, x2 be
Element of Y, x3 be
Element of Z, x4 be
Element of W such that
A4: x
=
[x1, x2, x3, x4] by
DOMAIN_1: 10;
consider y1 be
Element of X, y2 be
Element of Y, y3 be
Element of Z, y4 be
Element of W such that
A5: y
=
[y1, y2, y3, y4] by
DOMAIN_1: 10;
thus (f1
. (x,y))
= (((
dist (x1,y1))
+ (
dist (x2,y2)))
+ ((
dist (x3,y3))
+ (
dist (x4,y4)))) by
A2,
A4,
A5
.= (f2
. (x,y)) by
A3,
A4,
A5;
end;
hence thesis by
BINOP_1: 2;
end;
end
theorem ::
METRIC_3:7
Th7: for x,y be
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
let x,y be
Element of
[:the
carrier of X, the
carrier of Y, the
carrier of Z, the
carrier of W:];
reconsider x1 = (x
`1_4 ), y1 = (y
`1_4 ) as
Element of X;
reconsider x2 = (x
`2_4 ), y2 = (y
`2_4 ) as
Element of Y;
reconsider x3 = (x
`3_4 ), y3 = (y
`3_4 ) as
Element of Z;
reconsider x4 = (x
`4_4 ), y4 = (y
`4_4 ) as
Element of W;
A1: x
=
[x1, x2, x3, x4] & y
=
[y1, y2, y3, y4];
thus ((
dist_cart4 (X,Y,Z,W))
. (x,y))
=
0 implies x
= y
proof
set d1 = (
dist (x1,y1)), d2 = (
dist (x2,y2)), d3 = (
dist (x3,y3));
set d5 = (
dist (x4,y4)), d4 = (d1
+ d2), d6 = (d3
+ d5);
A2:
0
<= d3 &
0
<= d5 by
METRIC_1: 5;
then
A3: (
0
+
0 )
<= (d3
+ d5) by
XREAL_1: 7;
assume ((
dist_cart4 (X,Y,Z,W))
. (x,y))
=
0 ;
then
A4: (d4
+ d6)
=
0 by
A1,
Def7;
A5:
0
<= d1 &
0
<= d2 by
METRIC_1: 5;
then
A6: (
0
+
0 )
<= (d1
+ d2) by
XREAL_1: 7;
then
A7: d4
=
0 by
A4,
A3,
XREAL_1: 27;
then d2
=
0 by
A5,
XREAL_1: 27;
then
A8: x2
= y2 by
METRIC_1: 2;
A9: d6
=
0 by
A4,
A6,
A3,
XREAL_1: 27;
then d3
=
0 by
A2,
XREAL_1: 27;
then
A10: x3
= y3 by
METRIC_1: 2;
d5
=
0 by
A2,
A9,
XREAL_1: 27;
then
A11: x4
= y4 by
METRIC_1: 2;
d1
=
0 by
A5,
A7,
XREAL_1: 27;
hence thesis by
A1,
A8,
A10,
A11,
METRIC_1: 2;
end;
assume
A12: x
= y;
then
A13: (
dist (x2,y2))
=
0 & (
dist (x3,y3))
=
0 by
METRIC_1: 1;
A14: (
dist (x4,y4))
=
0 by
A12,
METRIC_1: 1;
((
dist_cart4 (X,Y,Z,W))
. (x,y))
= (((
dist (x1,y1))
+ (
dist (x2,y2)))
+ ((
dist (x3,y3))
+ (
dist (x4,y4)))) by
A1,
Def7
.=
0 by
A12,
A13,
A14,
METRIC_1: 1;
hence thesis;
end;
theorem ::
METRIC_3:8
Th8: for x,y be
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
let x,y be
Element of
[:the
carrier of X, the
carrier of Y, the
carrier of Z, the
carrier of W:];
reconsider x1 = (x
`1_4 ), y1 = (y
`1_4 ) as
Element of X;
reconsider x2 = (x
`2_4 ), y2 = (y
`2_4 ) as
Element of Y;
reconsider x3 = (x
`3_4 ), y3 = (y
`3_4 ) as
Element of Z;
reconsider x4 = (x
`4_4 ), y4 = (y
`4_4 ) as
Element of W;
A1: x
=
[x1, x2, x3, x4] & y
=
[y1, y2, y3, y4];
then ((
dist_cart4 (X,Y,Z,W))
. (x,y))
= (((
dist (y1,x1))
+ (
dist (y2,x2)))
+ ((
dist (y3,x3))
+ (
dist (x4,y4)))) by
Def7
.= ((
dist_cart4 (X,Y,Z,W))
. (y,x)) by
A1,
Def7;
hence thesis;
end;
theorem ::
METRIC_3:9
Th9: for x,y,z be
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
let x,y,z be
Element of
[:the
carrier of X, the
carrier of Y, the
carrier of Z, the
carrier of W:];
reconsider x1 = (x
`1_4 ), y1 = (y
`1_4 ), z1 = (z
`1_4 ) as
Element of X;
reconsider x2 = (x
`2_4 ), y2 = (y
`2_4 ), z2 = (z
`2_4 ) as
Element of Y;
reconsider x3 = (x
`3_4 ), y3 = (y
`3_4 ), z3 = (z
`3_4 ) as
Element of Z;
reconsider x4 = (x
`4_4 ), y4 = (y
`4_4 ), z4 = (z
`4_4 ) as
Element of W;
A1: x
=
[x1, x2, x3, x4];
set d7 = (
dist (x3,z3)), d8 = (
dist (x3,y3)), d9 = (
dist (y3,z3));
set d1 = (
dist (x1,z1)), d2 = (
dist (x1,y1)), d3 = (
dist (y1,z1));
A2: y
=
[y1, y2, y3, y4];
set d10 = (
dist (x4,z4)), d11 = (
dist (x4,y4)), d12 = (
dist (y4,z4));
set d4 = (
dist (x2,z2)), d5 = (
dist (x2,y2)), d6 = (
dist (y2,z2));
A3: z
=
[z1, z2, z3, z4];
set d16 = (d7
+ d10);
set d14 = (d1
+ d4);
set d17 = ((d8
+ d9)
+ (d11
+ d12)), d15 = ((d2
+ d3)
+ (d5
+ d6));
d7
<= (d8
+ d9) & d10
<= (d11
+ d12) by
METRIC_1: 4;
then
A4: d16
<= d17 by
XREAL_1: 7;
d1
<= (d2
+ d3) & d4
<= (d5
+ d6) by
METRIC_1: 4;
then d14
<= d15 by
XREAL_1: 7;
then
A5: (d14
+ d16)
<= (d15
+ d17) by
A4,
XREAL_1: 7;
(d15
+ d17)
= (((d2
+ d5)
+ (d8
+ d11))
+ ((d3
+ d6)
+ (d9
+ d12)))
.= (((
dist_cart4 (X,Y,Z,W))
. (x,y))
+ ((d3
+ d6)
+ (d9
+ d12))) by
A1,
A2,
Def7
.= (((
dist_cart4 (X,Y,Z,W))
. (x,y))
+ ((
dist_cart4 (X,Y,Z,W))
. (y,z))) by
A2,
A3,
Def7;
hence thesis by
A1,
A3,
A5,
Def7;
end;
definition
let X, Y, Z, W;
::
METRIC_3:def8
func
MetrSpaceCart4 (X,Y,Z,W) ->
strict non
empty
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
proof
set M =
MetrStruct (#
[:the
carrier of X, the
carrier of Y, the
carrier of Z, the
carrier of W:], (
dist_cart4 (X,Y,Z,W)) #);
now
let x,y,z be
Element of M;
reconsider x9 = x, y9 = y, z9 = z as
Element of
[:the
carrier of X, the
carrier of Y, the
carrier of Z, the
carrier of W:];
A1: (
dist (x,y))
= ((
dist_cart4 (X,Y,Z,W))
. (x9,y9)) by
METRIC_1:def 1;
hence (
dist (x,y))
=
0 iff x
= y by
Th7;
(
dist (y,x))
= ((
dist_cart4 (X,Y,Z,W))
. (y9,x9)) by
METRIC_1:def 1;
hence (
dist (x,y))
= (
dist (y,x)) by
A1,
Th8;
(
dist (x,z))
= ((
dist_cart4 (X,Y,Z,W))
. (x9,z9)) & (
dist (y,z))
= ((
dist_cart4 (X,Y,Z,W))
. (y9,z9)) by
METRIC_1:def 1;
hence (
dist (x,z))
<= ((
dist (x,y))
+ (
dist (y,z))) by
A1,
Th9;
end;
hence thesis by
METRIC_1: 6;
end;
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:];
::
METRIC_3:def9
func
dist4 (x,y) ->
Real equals ((
dist_cart4 (X,Y,Z,W))
. (x,y));
coherence ;
end
begin
reserve X,Y for non
empty
MetrSpace;
definition
let X, Y;
::
METRIC_3:def10
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: for x1,y1 be
Element of X holds for x2,y2 be
Element of Y holds for x,y be
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
proof
deffunc
G(
Element of X,
Element of X,
Element of Y,
Element of Y) = (
In ((
sqrt (((
dist ($1,$2))
^2 )
+ ((
dist ($3,$4))
^2 ))),
REAL ));
consider F be
Function of
[:
[:the
carrier of X, the
carrier of Y:],
[:the
carrier of X, the
carrier of Y:]:],
REAL such that
A1: for x1,y1 be
Element of X holds for x2,y2 be
Element of Y holds for x,y be
Element of
[:the
carrier of X, the
carrier of Y:] st x
=
[x1, x2] & y
=
[y1, y2] holds (F
. (x,y))
=
G(x1,y1,x2,y2) from
LambdaMCART;
take F;
let x1,y1 be
Element of X, x2,y2 be
Element of Y, x,y be
Element of
[:the
carrier of X, the
carrier of Y:];
assume x
=
[x1, x2] & y
=
[y1, y2];
then (F
. (x,y))
=
G(x1,y1,x2,y2) by
A1;
hence thesis;
end;
uniqueness
proof
let f1,f2 be
Function of
[:
[:the
carrier of X, the
carrier of Y:],
[:the
carrier of X, the
carrier of Y:]:],
REAL ;
assume that
A2: for x1,y1 be
Element of X holds for x2,y2 be
Element of Y holds for x,y be
Element of
[:the
carrier of X, the
carrier of Y:] st x
=
[x1, x2] & y
=
[y1, y2] holds (f1
. (x,y))
= (
sqrt (((
dist (x1,y1))
^2 )
+ ((
dist (x2,y2))
^2 ))) and
A3: for x1,y1 be
Element of X holds for x2,y2 be
Element of Y holds for x,y be
Element of
[:the
carrier of X, the
carrier of Y:] st x
=
[x1, x2] & y
=
[y1, y2] holds (f2
. (x,y))
= (
sqrt (((
dist (x1,y1))
^2 )
+ ((
dist (x2,y2))
^2 )));
for x,y be
Element of
[:the
carrier of X, the
carrier of Y:] holds (f1
. (x,y))
= (f2
. (x,y))
proof
let x,y be
Element of
[:the
carrier of X, the
carrier of Y:];
consider x1 be
Element of X, x2 be
Element of Y such that
A4: x
=
[x1, x2] by
DOMAIN_1: 1;
consider y1 be
Element of X, y2 be
Element of Y such that
A5: y
=
[y1, y2] by
DOMAIN_1: 1;
thus (f1
. (x,y))
= (
sqrt (((
dist (x1,y1))
^2 )
+ ((
dist (x2,y2))
^2 ))) by
A2,
A4,
A5
.= (f2
. (x,y)) by
A3,
A4,
A5;
end;
hence thesis by
BINOP_1: 2;
end;
end
Lm1: for a,b be
Real st
0
<= a &
0
<= b holds (
sqrt (a
+ b))
=
0 iff a
=
0 & b
=
0 by
SQUARE_1: 31;
theorem ::
METRIC_3:10
Th10: for x,y be
Element of
[:the
carrier of X, the
carrier of Y:] holds ((
dist_cart2S (X,Y))
. (x,y))
=
0 iff x
= y
proof
let x,y be
Element of
[:the
carrier of X, the
carrier of Y:];
reconsider x1 = (x
`1 ), y1 = (y
`1 ) as
Element of X;
reconsider x2 = (x
`2 ), y2 = (y
`2 ) as
Element of Y;
A1: x
=
[x1, x2] & y
=
[y1, y2];
thus ((
dist_cart2S (X,Y))
. (x,y))
=
0 implies x
= y
proof
set d2 = (
dist (x2,y2));
set d1 = (
dist (x1,y1));
assume ((
dist_cart2S (X,Y))
. (x,y))
=
0 ;
then
A2: (
sqrt ((d1
^2 )
+ (d2
^2 )))
=
0 by
A1,
Def10;
A3:
0
<= (d1
^2 ) &
0
<= (d2
^2 ) by
XREAL_1: 63;
then d1
=
0 by
A2,
Lm1;
then
A4: x1
= y1 by
METRIC_1: 2;
d2
=
0 by
A2,
A3,
Lm1;
hence thesis by
A1,
A4,
METRIC_1: 2;
end;
assume x
= y;
then
A5: ((
dist (x1,y1))
^2 )
= (
0
^2 ) & ((
dist (x2,y2))
^2 )
= (
0
^2 ) by
METRIC_1: 1;
((
dist_cart2S (X,Y))
. (x,y))
= (
sqrt (((
dist (x1,y1))
^2 )
+ ((
dist (x2,y2))
^2 ))) by
A1,
Def10
.=
0 by
A5,
Lm1;
hence thesis;
end;
theorem ::
METRIC_3:11
Th11: for x,y be
Element of
[:the
carrier of X, the
carrier of Y:] holds ((
dist_cart2S (X,Y))
. (x,y))
= ((
dist_cart2S (X,Y))
. (y,x))
proof
let x,y be
Element of
[:the
carrier of X, the
carrier of Y:];
reconsider x1 = (x
`1 ), y1 = (y
`1 ) as
Element of X;
reconsider x2 = (x
`2 ), y2 = (y
`2 ) as
Element of Y;
A1: x
=
[x1, x2] & y
=
[y1, y2];
then ((
dist_cart2S (X,Y))
. (x,y))
= (
sqrt (((
dist (y1,x1))
^2 )
+ ((
dist (x2,y2))
^2 ))) by
Def10
.= ((
dist_cart2S (X,Y))
. (y,x)) by
A1,
Def10;
hence thesis;
end;
theorem ::
METRIC_3:12
Th12: for a,b,c,d be
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 ))))
proof
let a,b,c,d be
Real;
assume
0
<= a &
0
<= b &
0
<= c &
0
<= d;
then
0
<= (a
* c) &
0
<= (d
* b) by
XREAL_1: 127;
then
A1: (
0
+
0 )
<= ((a
* c)
+ (d
* b)) by
XREAL_1: 7;
0
<= (d
^2 ) &
0
<= (c
^2 ) by
XREAL_1: 63;
then
A2: (
0
+
0 )
<= ((c
^2 )
+ (d
^2 )) by
XREAL_1: 7;
then
A3:
0
<= (
sqrt ((c
^2 )
+ (d
^2 ))) by
SQUARE_1:def 2;
0
<= (((a
* d)
- (c
* b))
^2 ) by
XREAL_1: 63;
then
0
<= ((((a
^2 )
* (d
^2 ))
+ ((c
^2 )
* (b
^2 )))
- ((2
* (a
* d))
* (c
* b)));
then (
0
+ ((2
* (a
* d))
* (c
* b)))
<= (((a
^2 )
* (d
^2 ))
+ ((c
^2 )
* (b
^2 ))) by
XREAL_1: 19;
then (((b
^2 )
* (d
^2 ))
+ ((2
* (a
* d))
* (c
* b)))
<= ((((a
^2 )
* (d
^2 ))
+ ((c
^2 )
* (b
^2 )))
+ ((b
^2 )
* (d
^2 ))) by
XREAL_1: 6;
then
A4: (((a
^2 )
* (c
^2 ))
+ (((b
^2 )
* (d
^2 ))
+ ((2
* (a
* d))
* (c
* b))))
<= (((a
^2 )
* (c
^2 ))
+ (((b
^2 )
* (d
^2 ))
+ (((a
^2 )
* (d
^2 ))
+ ((c
^2 )
* (b
^2 ))))) by
XREAL_1: 6;
0
<= (a
^2 ) &
0
<= (b
^2 ) by
XREAL_1: 63;
then
A5: (
0
+
0 )
<= ((a
^2 )
+ (b
^2 )) by
XREAL_1: 7;
then
0
<= (
sqrt ((a
^2 )
+ (b
^2 ))) by
SQUARE_1:def 2;
then
A6: (
0
+
0 )
<= ((
sqrt ((a
^2 )
+ (b
^2 )))
+ (
sqrt ((c
^2 )
+ (d
^2 )))) by
A3,
XREAL_1: 7;
0
<= (((a
* c)
+ (d
* b))
^2 ) by
XREAL_1: 63;
then (
sqrt (((a
* c)
+ (d
* b))
^2 ))
<= (
sqrt (((a
^2 )
+ (b
^2 ))
* ((c
^2 )
+ (d
^2 )))) by
A4,
SQUARE_1: 26;
then (2
* (
sqrt (((a
* c)
+ (d
* b))
^2 )))
<= (2
* (
sqrt (((a
^2 )
+ (b
^2 ))
* ((c
^2 )
+ (d
^2 ))))) by
XREAL_1: 64;
then (2
* (
sqrt (((a
* c)
+ (d
* b))
^2 )))
<= (2
* ((
sqrt ((a
^2 )
+ (b
^2 )))
* (
sqrt ((c
^2 )
+ (d
^2 ))))) by
A5,
A2,
SQUARE_1: 29;
then (2
* ((a
* c)
+ (d
* b)))
<= (2
* ((
sqrt ((a
^2 )
+ (b
^2 )))
* (
sqrt ((d
^2 )
+ (c
^2 ))))) by
A1,
SQUARE_1: 22;
then ((b
^2 )
+ (2
* ((a
* c)
+ (d
* b))))
<= ((2
* ((
sqrt ((a
^2 )
+ (b
^2 )))
* (
sqrt ((d
^2 )
+ (c
^2 )))))
+ (b
^2 )) by
XREAL_1: 6;
then ((d
^2 )
+ ((b
^2 )
+ (2
* ((a
* c)
+ (d
* b)))))
<= ((d
^2 )
+ ((b
^2 )
+ (2
* ((
sqrt ((a
^2 )
+ (b
^2 )))
* (
sqrt ((d
^2 )
+ (c
^2 ))))))) by
XREAL_1: 6;
then ((c
^2 )
+ ((d
^2 )
+ ((b
^2 )
+ (2
* ((a
* c)
+ (d
* b))))))
<= (((d
^2 )
+ ((b
^2 )
+ (2
* ((
sqrt ((a
^2 )
+ (b
^2 )))
* (
sqrt ((d
^2 )
+ (c
^2 )))))))
+ (c
^2 )) by
XREAL_1: 6;
then ((a
^2 )
+ ((c
^2 )
+ ((d
^2 )
+ (((b
^2 )
+ (2
* (d
* b)))
+ (2
* (a
* c))))))
<= ((a
^2 )
+ ((c
^2 )
+ ((d
^2 )
+ ((b
^2 )
+ (2
* ((
sqrt ((a
^2 )
+ (b
^2 )))
* (
sqrt ((d
^2 )
+ (c
^2 ))))))))) by
XREAL_1: 6;
then (((a
+ c)
^2 )
+ ((d
+ b)
^2 ))
<= ((((a
^2 )
+ (b
^2 ))
+ (2
* ((
sqrt ((a
^2 )
+ (b
^2 )))
* (
sqrt ((c
^2 )
+ (d
^2 ))))))
+ ((c
^2 )
+ (d
^2 )));
then (((a
+ c)
^2 )
+ ((d
+ b)
^2 ))
<= ((((
sqrt ((a
^2 )
+ (b
^2 )))
^2 )
+ (2
* ((
sqrt ((a
^2 )
+ (b
^2 )))
* (
sqrt ((c
^2 )
+ (d
^2 ))))))
+ ((c
^2 )
+ (d
^2 ))) by
A5,
SQUARE_1:def 2;
then
A7: (((a
+ c)
^2 )
+ ((d
+ b)
^2 ))
<= ((((
sqrt ((a
^2 )
+ (b
^2 )))
^2 )
+ ((2
* (
sqrt ((a
^2 )
+ (b
^2 ))))
* (
sqrt ((c
^2 )
+ (d
^2 )))))
+ ((
sqrt ((c
^2 )
+ (d
^2 )))
^2 )) by
A2,
SQUARE_1:def 2;
0
<= ((a
+ c)
^2 ) &
0
<= ((d
+ b)
^2 ) by
XREAL_1: 63;
then (
0
+
0 )
<= (((a
+ c)
^2 )
+ ((d
+ b)
^2 )) by
XREAL_1: 7;
then (
sqrt (((a
+ c)
^2 )
+ ((d
+ b)
^2 )))
<= (
sqrt (((
sqrt ((a
^2 )
+ (b
^2 )))
+ (
sqrt ((c
^2 )
+ (d
^2 ))))
^2 )) by
A7,
SQUARE_1: 26;
hence thesis by
A6,
SQUARE_1: 22;
end;
theorem ::
METRIC_3:13
Th13: for x,y,z be
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
let x,y,z be
Element of
[:the
carrier of X, the
carrier of Y:];
reconsider x1 = (x
`1 ), y1 = (y
`1 ), z1 = (z
`1 ) as
Element of X;
reconsider x2 = (x
`2 ), y2 = (y
`2 ), z2 = (z
`2 ) as
Element of Y;
A1: x
=
[x1, x2];
set d5 = (
dist (x2,y2));
set d3 = (
dist (y1,z1));
set d1 = (
dist (x1,z1));
A2: y
=
[y1, y2];
set d6 = (
dist (y2,z2));
set d4 = (
dist (x2,z2));
set d2 = (
dist (x1,y1));
A3: z
=
[z1, z2];
0
<= (d1
^2 ) &
0
<= (d4
^2 ) by
XREAL_1: 63;
then
A4: (
0
+
0 )
<= ((d1
^2 )
+ (d4
^2 )) by
XREAL_1: 7;
d4
<= (d5
+ d6) &
0
<= d4 by
METRIC_1: 4,
METRIC_1: 5;
then
A5: (d4
^2 )
<= ((d5
+ d6)
^2 ) by
SQUARE_1: 15;
d1
<= (d2
+ d3) &
0
<= d1 by
METRIC_1: 4,
METRIC_1: 5;
then (d1
^2 )
<= ((d2
+ d3)
^2 ) by
SQUARE_1: 15;
then ((d1
^2 )
+ (d4
^2 ))
<= (((d2
+ d3)
^2 )
+ ((d5
+ d6)
^2 )) by
A5,
XREAL_1: 7;
then
A6: (
sqrt ((d1
^2 )
+ (d4
^2 )))
<= (
sqrt (((d2
+ d3)
^2 )
+ ((d5
+ d6)
^2 ))) by
A4,
SQUARE_1: 26;
A7:
0
<= d5 &
0
<= d6 by
METRIC_1: 5;
0
<= d2 &
0
<= d3 by
METRIC_1: 5;
then (
sqrt (((d2
+ d3)
^2 )
+ ((d5
+ d6)
^2 )))
<= ((
sqrt ((d2
^2 )
+ (d5
^2 )))
+ (
sqrt ((d3
^2 )
+ (d6
^2 )))) by
A7,
Th12;
then (
sqrt ((d1
^2 )
+ (d4
^2 )))
<= ((
sqrt ((d2
^2 )
+ (d5
^2 )))
+ (
sqrt ((d3
^2 )
+ (d6
^2 )))) by
A6,
XXREAL_0: 2;
then ((
dist_cart2S (X,Y))
. (x,z))
<= ((
sqrt ((d2
^2 )
+ (d5
^2 )))
+ (
sqrt ((d3
^2 )
+ (d6
^2 )))) by
A1,
A3,
Def10;
then ((
dist_cart2S (X,Y))
. (x,z))
<= (((
dist_cart2S (X,Y))
. (x,y))
+ (
sqrt ((d3
^2 )
+ (d6
^2 )))) by
A1,
A2,
Def10;
hence thesis by
A2,
A3,
Def10;
end;
definition
let X, Y;
let x,y be
Element of
[:the
carrier of X, the
carrier of Y:];
::
METRIC_3:def11
func
dist2S (x,y) ->
Real equals ((
dist_cart2S (X,Y))
. (x,y));
coherence ;
end
definition
let X, Y;
::
METRIC_3:def12
func
MetrSpaceCart2S (X,Y) ->
strict non
empty
MetrSpace equals
MetrStruct (#
[:the
carrier of X, the
carrier of Y:], (
dist_cart2S (X,Y)) #);
coherence
proof
now
let x,y,z be
Element of
MetrStruct (#
[:the
carrier of X, the
carrier of Y:], (
dist_cart2S (X,Y)) #);
reconsider x9 = x, y9 = y, z9 = z as
Element of
[:the
carrier of X, the
carrier of Y:];
A1: (
dist (x,y))
= ((
dist_cart2S (X,Y))
. (x9,y9)) by
METRIC_1:def 1;
hence (
dist (x,y))
=
0 iff x
= y by
Th10;
(
dist (y,x))
= ((
dist_cart2S (X,Y))
. (y9,x9)) by
METRIC_1:def 1;
hence (
dist (x,y))
= (
dist (y,x)) by
A1,
Th11;
(
dist (x,z))
= ((
dist_cart2S (X,Y))
. (x9,z9)) & (
dist (y,z))
= ((
dist_cart2S (X,Y))
. (y9,z9)) by
METRIC_1:def 1;
hence (
dist (x,z))
<= ((
dist (x,y))
+ (
dist (y,z))) by
A1,
Th13;
end;
hence thesis by
METRIC_1: 6;
end;
end
begin
reserve Z for non
empty
MetrSpace;
definition
let X, Y, Z;
::
METRIC_3:def13
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: for x1,y1 be
Element of X holds for x2,y2 be
Element of Y holds for x3,y3 be
Element of Z holds for x,y be
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
proof
deffunc
G(
Element of X,
Element of X,
Element of Y,
Element of Y,
Element of Z,
Element of Z) = (
In ((
sqrt ((((
dist ($1,$2))
^2 )
+ ((
dist ($3,$4))
^2 ))
+ ((
dist ($5,$6))
^2 ))),
REAL ));
consider F be
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 such that
A1: for x1,y1 be
Element of X holds for x2,y2 be
Element of Y holds for x3,y3 be
Element of Z holds for x,y be
Element of
[:the
carrier of X, the
carrier of Y, the
carrier of Z:] st x
=
[x1, x2, x3] & y
=
[y1, y2, y3] holds (F
. (x,y))
=
G(x1,y1,x2,y2,x3,y3) from
LambdaMCART1;
take F;
let x1,y1 be
Element of X, x2,y2 be
Element of Y, x3,y3 be
Element of Z, x,y be
Element of
[:the
carrier of X, the
carrier of Y, the
carrier of Z:];
assume x
=
[x1, x2, x3] & y
=
[y1, y2, y3];
then (F
. (x,y))
=
G(x1,y1,x2,y2,x3,y3) by
A1;
hence thesis;
end;
uniqueness
proof
let f1,f2 be
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 ;
assume that
A2: for x1,y1 be
Element of X holds for x2,y2 be
Element of Y holds for x3,y3 be
Element of Z holds for x,y be
Element of
[:the
carrier of X, the
carrier of Y, the
carrier of Z:] st x
=
[x1, x2, x3] & y
=
[y1, y2, y3] holds (f1
. (x,y))
= (
sqrt ((((
dist (x1,y1))
^2 )
+ ((
dist (x2,y2))
^2 ))
+ ((
dist (x3,y3))
^2 ))) and
A3: for x1,y1 be
Element of X holds for x2,y2 be
Element of Y holds for x3,y3 be
Element of Z holds for x,y be
Element of
[:the
carrier of X, the
carrier of Y, the
carrier of Z:] st x
=
[x1, x2, x3] & y
=
[y1, y2, y3] holds (f2
. (x,y))
= (
sqrt ((((
dist (x1,y1))
^2 )
+ ((
dist (x2,y2))
^2 ))
+ ((
dist (x3,y3))
^2 )));
for x,y be
Element of
[:the
carrier of X, the
carrier of Y, the
carrier of Z:] holds (f1
. (x,y))
= (f2
. (x,y))
proof
let x,y be
Element of
[:the
carrier of X, the
carrier of Y, the
carrier of Z:];
consider x1 be
Element of X, x2 be
Element of Y, x3 be
Element of Z such that
A4: x
=
[x1, x2, x3] by
DOMAIN_1: 3;
consider y1 be
Element of X, y2 be
Element of Y, y3 be
Element of Z such that
A5: y
=
[y1, y2, y3] by
DOMAIN_1: 3;
thus (f1
. (x,y))
= (
sqrt ((((
dist (x1,y1))
^2 )
+ ((
dist (x2,y2))
^2 ))
+ ((
dist (x3,y3))
^2 ))) by
A2,
A4,
A5
.= (f2
. (x,y)) by
A3,
A4,
A5;
end;
hence thesis by
BINOP_1: 2;
end;
end
theorem ::
METRIC_3:14
Th14: for x,y be
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
let x,y be
Element of
[:the
carrier of X, the
carrier of Y, the
carrier of Z:];
reconsider x1 = (x
`1_3 ), y1 = (y
`1_3 ) as
Element of X;
reconsider x2 = (x
`2_3 ), y2 = (y
`2_3 ) as
Element of Y;
reconsider x3 = (x
`3_3 ), y3 = (y
`3_3 ) as
Element of Z;
A1: x
=
[x1, x2, x3] & y
=
[y1, y2, y3];
thus ((
dist_cart3S (X,Y,Z))
. (x,y))
=
0 implies x
= y
proof
set d3 = (
dist (x3,y3));
set d2 = (
dist (x2,y2));
set d1 = (
dist (x1,y1));
A2:
0
<= (d2
^2 ) &
0
<= (d3
^2 ) by
XREAL_1: 63;
assume ((
dist_cart3S (X,Y,Z))
. (x,y))
=
0 ;
then (
sqrt (((d1
^2 )
+ (d2
^2 ))
+ (d3
^2 )))
=
0 by
A1,
Def13;
then
A3: (
sqrt ((d1
^2 )
+ ((d2
^2 )
+ (d3
^2 ))))
=
0 ;
0
<= (d2
^2 ) &
0
<= (d3
^2 ) by
XREAL_1: 63;
then
A4:
0
<= (d1
^2 ) & (
0
+
0 )
<= ((d2
^2 )
+ (d3
^2 )) by
XREAL_1: 7,
XREAL_1: 63;
then d1
=
0 by
A3,
Lm1;
then
A5: x1
= y1 by
METRIC_1: 2;
A6: ((d2
^2 )
+ (d3
^2 ))
=
0 by
A3,
A4,
Lm1;
then d2
=
0 by
A2,
XREAL_1: 27;
then
A7: x2
= y2 by
METRIC_1: 2;
d3
=
0 by
A6,
A2,
XREAL_1: 27;
hence thesis by
A1,
A5,
A7,
METRIC_1: 2;
end;
assume
A8: x
= y;
then
A9: ((
dist (x1,y1))
^2 )
= (
0
^2 ) & ((
dist (x2,y2))
^2 )
= (
0
^2 ) by
METRIC_1: 1;
((
dist_cart3S (X,Y,Z))
. (x,y))
= (
sqrt ((((
dist (x1,y1))
^2 )
+ ((
dist (x2,y2))
^2 ))
+ ((
dist (x3,y3))
^2 ))) by
A1,
Def13
.= (
0
^2 ) by
A8,
A9,
METRIC_1: 1,
SQUARE_1: 17;
hence thesis;
end;
theorem ::
METRIC_3:15
Th15: for x,y be
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
let x,y be
Element of
[:the
carrier of X, the
carrier of Y, the
carrier of Z:];
reconsider x1 = (x
`1_3 ), y1 = (y
`1_3 ) as
Element of X;
reconsider x2 = (x
`2_3 ), y2 = (y
`2_3 ) as
Element of Y;
reconsider x3 = (x
`3_3 ), y3 = (y
`3_3 ) as
Element of Z;
A1: x
=
[x1, x2, x3] & y
=
[y1, y2, y3];
then ((
dist_cart3S (X,Y,Z))
. (x,y))
= (
sqrt ((((
dist (y1,x1))
^2 )
+ ((
dist (y2,x2))
^2 ))
+ ((
dist (y3,x3))
^2 ))) by
Def13
.= ((
dist_cart3S (X,Y,Z))
. (y,x)) by
A1,
Def13;
hence thesis;
end;
theorem ::
METRIC_3:16
Th16: for a,b,c,d,e,f be
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
let a,b,c,d,e,f be
Real;
0
<= (((a
* f)
- (e
* c))
^2 ) &
0
<= (((b
* f)
- (e
* d))
^2 ) by
XREAL_1: 63;
then
0
<= (((a
* d)
- (c
* b))
^2 ) & (
0
+
0 )
<= ((((a
* f)
- (e
* c))
^2 )
+ (((b
* f)
- (e
* d))
^2 )) by
XREAL_1: 7,
XREAL_1: 63;
then (
0
+
0 )
<= ((((a
* d)
- (c
* b))
^2 )
+ ((((a
* f)
- (e
* c))
^2 )
+ (((b
* f)
- (e
* d))
^2 ))) by
XREAL_1: 7;
then
0
<= ((((((a
* d)
^2 )
+ ((c
* b)
^2 ))
+ (((a
* f)
- (e
* c))
^2 ))
+ (((b
* f)
- (e
* d))
^2 ))
- ((2
* (a
* d))
* (c
* b)));
then (
0
+ ((2
* (a
* d))
* (c
* b)))
<= (((((a
* d)
^2 )
+ ((c
* b)
^2 ))
+ (((a
* f)
- (e
* c))
^2 ))
+ (((b
* f)
- (e
* d))
^2 )) by
XREAL_1: 19;
then ((2
* (a
* d))
* (c
* b))
<= (((((((a
* d)
^2 )
+ ((c
* b)
^2 ))
+ ((a
* f)
^2 ))
+ ((e
* c)
^2 ))
+ (((b
* f)
- (e
* d))
^2 ))
- ((2
* (a
* f))
* (e
* c)));
then (((2
* (a
* d))
* (c
* b))
+ ((2
* (a
* f))
* (e
* c)))
<= ((((((((a
* d)
^2 )
+ ((c
* b)
^2 ))
+ ((a
* f)
^2 ))
+ ((e
* c)
^2 ))
+ ((b
* f)
^2 ))
+ ((e
* d)
^2 ))
- ((2
* (b
* f))
* (e
* d))) by
XREAL_1: 19;
hence thesis by
XREAL_1: 19;
end;
theorem ::
METRIC_3:17
Th17: for a,b,c,d,e,f be
Real holds ((((a
* c)
+ (b
* d))
+ (e
* f))
^2 )
<= ((((a
^2 )
+ (b
^2 ))
+ (e
^2 ))
* (((c
^2 )
+ (d
^2 ))
+ (f
^2 )))
proof
let a,b,c,d,e,f be
Real;
((((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 )) by
Th16;
then (((e
* f)
^2 )
+ ((((2
* (a
* b))
* (c
* d))
+ ((2
* (a
* c))
* (e
* f)))
+ ((2
* (b
* d))
* (e
* f))))
<= ((((((((a
* d)
^2 )
+ ((c
* b)
^2 ))
+ ((a
* f)
^2 ))
+ ((e
* c)
^2 ))
+ ((b
* f)
^2 ))
+ ((e
* d)
^2 ))
+ ((e
* f)
^2 )) by
XREAL_1: 6;
then (((b
* d)
^2 )
+ (((e
* f)
^2 )
+ ((((2
* (a
* b))
* (c
* d))
+ ((2
* (a
* c))
* (e
* f)))
+ ((2
* (b
* d))
* (e
* f)))))
<= (((((((((a
* d)
^2 )
+ ((c
* b)
^2 ))
+ ((a
* f)
^2 ))
+ ((e
* c)
^2 ))
+ ((b
* f)
^2 ))
+ ((e
* d)
^2 ))
+ ((e
* f)
^2 ))
+ ((b
* d)
^2 )) by
XREAL_1: 6;
then (((a
* c)
^2 )
+ (((b
* d)
^2 )
+ (((e
* f)
^2 )
+ ((((2
* (a
* b))
* (c
* d))
+ ((2
* (a
* c))
* (e
* f)))
+ ((2
* (b
* d))
* (e
* f))))))
<= ((((((((((a
* d)
^2 )
+ ((c
* b)
^2 ))
+ ((a
* f)
^2 ))
+ ((e
* c)
^2 ))
+ ((b
* f)
^2 ))
+ ((e
* d)
^2 ))
+ ((e
* f)
^2 ))
+ ((b
* d)
^2 ))
+ ((a
* c)
^2 )) by
XREAL_1: 6;
hence thesis;
end;
Lm2: for a,b,c,d,e,f be
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
let a,b,c,d,e,f be
Real;
assume that
A1:
0
<= a and
A2:
0
<= b and
A3:
0
<= c and
A4:
0
<= d &
0
<= e &
0
<= f;
0
<= (b
* d) &
0
<= (e
* f) by
A2,
A4,
XREAL_1: 127;
then
A5: (
0
+
0 )
<= ((b
* d)
+ (e
* f)) by
XREAL_1: 7;
0
<= (c
^2 ) &
0
<= (d
^2 ) by
XREAL_1: 63;
then
A6: (
0
+
0 )
<= ((c
^2 )
+ (d
^2 )) by
XREAL_1: 7;
0
<= (f
^2 ) by
XREAL_1: 63;
then
A7: (
0
+
0 )
<= (((c
^2 )
+ (d
^2 ))
+ (f
^2 )) by
A6,
XREAL_1: 7;
then
A8:
0
<= (
sqrt (((c
^2 )
+ (d
^2 ))
+ (f
^2 ))) by
SQUARE_1:def 2;
0
<= ((((a
* c)
+ (b
* d))
+ (e
* f))
^2 ) by
XREAL_1: 63;
then
A9: (
sqrt ((((a
* c)
+ (b
* d))
+ (e
* f))
^2 ))
<= (
sqrt ((((a
^2 )
+ (b
^2 ))
+ (e
^2 ))
* (((c
^2 )
+ (d
^2 ))
+ (f
^2 )))) by
Th17,
SQUARE_1: 26;
0
<= (a
^2 ) &
0
<= (b
^2 ) by
XREAL_1: 63;
then
A10: (
0
+
0 )
<= ((a
^2 )
+ (b
^2 )) by
XREAL_1: 7;
0
<= (e
^2 ) by
XREAL_1: 63;
then
A11: (
0
+
0 )
<= (((a
^2 )
+ (b
^2 ))
+ (e
^2 )) by
A10,
XREAL_1: 7;
0
<= (a
* c) by
A1,
A3,
XREAL_1: 127;
then (
0
+
0 )
<= ((a
* c)
+ ((b
* d)
+ (e
* f))) by
A5,
XREAL_1: 7;
then (((a
* c)
+ (b
* d))
+ (e
* f))
<= (
sqrt ((((a
^2 )
+ (b
^2 ))
+ (e
^2 ))
* (((c
^2 )
+ (d
^2 ))
+ (f
^2 )))) by
A9,
SQUARE_1: 22;
then (((a
* c)
+ (b
* d))
+ (e
* f))
<= ((
sqrt (((a
^2 )
+ (b
^2 ))
+ (e
^2 )))
* (
sqrt (((c
^2 )
+ (d
^2 ))
+ (f
^2 )))) by
A11,
A7,
SQUARE_1: 29;
then (2
* (((a
* c)
+ (b
* d))
+ (e
* f)))
<= (2
* ((
sqrt (((a
^2 )
+ (b
^2 ))
+ (e
^2 )))
* (
sqrt (((c
^2 )
+ (d
^2 ))
+ (f
^2 ))))) by
XREAL_1: 64;
then (((2
* ((a
* c)
+ (b
* d)))
+ (2
* (e
* f)))
+ (e
^2 ))
<= (((2
* (
sqrt (((a
^2 )
+ (b
^2 ))
+ (e
^2 ))))
* (
sqrt (((c
^2 )
+ (d
^2 ))
+ (f
^2 ))))
+ (e
^2 )) by
XREAL_1: 6;
then (((2
* ((a
* c)
+ (b
* d)))
+ ((e
^2 )
+ (2
* (e
* f))))
+ (f
^2 ))
<= ((((2
* (
sqrt (((a
^2 )
+ (b
^2 ))
+ (e
^2 ))))
* (
sqrt (((c
^2 )
+ (d
^2 ))
+ (f
^2 ))))
+ (e
^2 ))
+ (f
^2 )) by
XREAL_1: 6;
then ((((2
* (a
* c))
+ (2
* (b
* d)))
+ ((e
+ f)
^2 ))
+ (b
^2 ))
<= ((((e
^2 )
+ ((2
* (
sqrt (((a
^2 )
+ (b
^2 ))
+ (e
^2 ))))
* (
sqrt (((c
^2 )
+ (d
^2 ))
+ (f
^2 )))))
+ (f
^2 ))
+ (b
^2 )) by
XREAL_1: 6;
then ((((2
* (a
* c))
+ ((b
^2 )
+ (2
* (b
* d))))
+ ((e
+ f)
^2 ))
+ (d
^2 ))
<= (((b
^2 )
+ (((e
^2 )
+ ((2
* (
sqrt (((a
^2 )
+ (b
^2 ))
+ (e
^2 ))))
* (
sqrt (((c
^2 )
+ (d
^2 ))
+ (f
^2 )))))
+ (f
^2 )))
+ (d
^2 )) by
XREAL_1: 6;
then ((a
^2 )
+ ((2
* (a
* c))
+ (((b
+ d)
^2 )
+ ((e
+ f)
^2 ))))
<= (((b
^2 )
+ (((e
^2 )
+ ((2
* (
sqrt (((a
^2 )
+ (b
^2 ))
+ (e
^2 ))))
* (
sqrt (((c
^2 )
+ (d
^2 ))
+ (f
^2 )))))
+ ((d
^2 )
+ (f
^2 ))))
+ (a
^2 )) by
XREAL_1: 6;
then ((((a
^2 )
+ (2
* (a
* c)))
+ (((b
+ d)
^2 )
+ ((e
+ f)
^2 )))
+ (c
^2 ))
<= ((((((a
^2 )
+ (b
^2 ))
+ (e
^2 ))
+ ((2
* (
sqrt (((a
^2 )
+ (b
^2 ))
+ (e
^2 ))))
* (
sqrt (((c
^2 )
+ (d
^2 ))
+ (f
^2 )))))
+ ((d
^2 )
+ (f
^2 )))
+ (c
^2 )) by
XREAL_1: 6;
then ((((a
+ c)
^2 )
+ ((b
+ d)
^2 ))
+ ((e
+ f)
^2 ))
<= (((((a
^2 )
+ (b
^2 ))
+ (e
^2 ))
+ ((2
* (
sqrt (((a
^2 )
+ (b
^2 ))
+ (e
^2 ))))
* (
sqrt (((c
^2 )
+ (d
^2 ))
+ (f
^2 )))))
+ ((c
^2 )
+ ((d
^2 )
+ (f
^2 ))));
then ((((a
+ c)
^2 )
+ ((b
+ d)
^2 ))
+ ((e
+ f)
^2 ))
<= ((((
sqrt (((a
^2 )
+ (b
^2 ))
+ (e
^2 )))
^2 )
+ ((2
* (
sqrt (((a
^2 )
+ (b
^2 ))
+ (e
^2 ))))
* (
sqrt (((c
^2 )
+ (d
^2 ))
+ (f
^2 )))))
+ (((c
^2 )
+ (d
^2 ))
+ (f
^2 ))) by
A11,
SQUARE_1:def 2;
then
A12: ((((a
+ c)
^2 )
+ ((b
+ d)
^2 ))
+ ((e
+ f)
^2 ))
<= ((((
sqrt (((a
^2 )
+ (b
^2 ))
+ (e
^2 )))
^2 )
+ ((2
* (
sqrt (((a
^2 )
+ (b
^2 ))
+ (e
^2 ))))
* (
sqrt (((c
^2 )
+ (d
^2 ))
+ (f
^2 )))))
+ ((
sqrt (((c
^2 )
+ (d
^2 ))
+ (f
^2 )))
^2 )) by
A7,
SQUARE_1:def 2;
0
<= ((a
+ c)
^2 ) &
0
<= ((b
+ d)
^2 ) by
XREAL_1: 63;
then
A13: (
0
+
0 )
<= (((a
+ c)
^2 )
+ ((b
+ d)
^2 )) by
XREAL_1: 7;
0
<= ((e
+ f)
^2 ) by
XREAL_1: 63;
then (
0
+
0 )
<= ((((a
+ c)
^2 )
+ ((b
+ d)
^2 ))
+ ((e
+ f)
^2 )) by
A13,
XREAL_1: 7;
then
A14: (
sqrt ((((a
+ c)
^2 )
+ ((b
+ d)
^2 ))
+ ((e
+ f)
^2 )))
<= (
sqrt (((
sqrt (((a
^2 )
+ (b
^2 ))
+ (e
^2 )))
+ (
sqrt (((c
^2 )
+ (d
^2 ))
+ (f
^2 ))))
^2 )) by
A12,
SQUARE_1: 26;
0
<= (
sqrt (((a
^2 )
+ (b
^2 ))
+ (e
^2 ))) by
A11,
SQUARE_1:def 2;
then (
0
+
0 )
<= ((
sqrt (((a
^2 )
+ (b
^2 ))
+ (e
^2 )))
+ (
sqrt (((c
^2 )
+ (d
^2 ))
+ (f
^2 )))) by
A8,
XREAL_1: 7;
hence thesis by
A14,
SQUARE_1: 22;
end;
theorem ::
METRIC_3:18
Th18: for x,y,z be
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
let x,y,z be
Element of
[:the
carrier of X, the
carrier of Y, the
carrier of Z:];
reconsider x1 = (x
`1_3 ), y1 = (y
`1_3 ), z1 = (z
`1_3 ) as
Element of X;
reconsider x2 = (x
`2_3 ), y2 = (y
`2_3 ), z2 = (z
`2_3 ) as
Element of Y;
reconsider x3 = (x
`3_3 ), y3 = (y
`3_3 ), z3 = (z
`3_3 ) as
Element of Z;
A1: x
=
[x1, x2, x3];
set d7 = (
dist (x3,z3)), d8 = (
dist (x3,y3)), d9 = (
dist (y3,z3));
set d1 = (
dist (x1,z1)), d2 = (
dist (x1,y1)), d3 = (
dist (y1,z1));
A2: y
=
[y1, y2, y3];
d7
<= (d8
+ d9) &
0
<= d7 by
METRIC_1: 4,
METRIC_1: 5;
then
A3: (d7
^2 )
<= ((d8
+ d9)
^2 ) by
SQUARE_1: 15;
A4:
0
<= d8 &
0
<= d9 by
METRIC_1: 5;
set d4 = (
dist (x2,z2)), d5 = (
dist (x2,y2)), d6 = (
dist (y2,z2));
A5: z
=
[z1, z2, z3];
d4
<= (d5
+ d6) &
0
<= d4 by
METRIC_1: 4,
METRIC_1: 5;
then
A6: (d4
^2 )
<= ((d5
+ d6)
^2 ) by
SQUARE_1: 15;
A7:
0
<= d5 &
0
<= d6 by
METRIC_1: 5;
0
<= (d1
^2 ) &
0
<= (d4
^2 ) by
XREAL_1: 63;
then
A8: (
0
+
0 )
<= ((d1
^2 )
+ (d4
^2 )) by
XREAL_1: 7;
d1
<= (d2
+ d3) &
0
<= d1 by
METRIC_1: 4,
METRIC_1: 5;
then (d1
^2 )
<= ((d2
+ d3)
^2 ) by
SQUARE_1: 15;
then ((d1
^2 )
+ (d4
^2 ))
<= (((d2
+ d3)
^2 )
+ ((d5
+ d6)
^2 )) by
A6,
XREAL_1: 7;
then
A9: (((d1
^2 )
+ (d4
^2 ))
+ (d7
^2 ))
<= ((((d2
+ d3)
^2 )
+ ((d5
+ d6)
^2 ))
+ ((d8
+ d9)
^2 )) by
A3,
XREAL_1: 7;
0
<= (d7
^2 ) by
XREAL_1: 63;
then (
0
+
0 )
<= (((d1
^2 )
+ (d4
^2 ))
+ (d7
^2 )) by
A8,
XREAL_1: 7;
then
A10: (
sqrt (((d1
^2 )
+ (d4
^2 ))
+ (d7
^2 )))
<= (
sqrt ((((d2
+ d3)
^2 )
+ ((d5
+ d6)
^2 ))
+ ((d8
+ d9)
^2 ))) by
A9,
SQUARE_1: 26;
0
<= d2 &
0
<= d3 by
METRIC_1: 5;
then (
sqrt ((((d2
+ d3)
^2 )
+ ((d5
+ d6)
^2 ))
+ ((d8
+ d9)
^2 )))
<= ((
sqrt (((d2
^2 )
+ (d5
^2 ))
+ (d8
^2 )))
+ (
sqrt (((d3
^2 )
+ (d6
^2 ))
+ (d9
^2 )))) by
A7,
A4,
Lm2;
then (
sqrt (((d1
^2 )
+ (d4
^2 ))
+ (d7
^2 )))
<= ((
sqrt (((d2
^2 )
+ (d5
^2 ))
+ (d8
^2 )))
+ (
sqrt (((d3
^2 )
+ (d6
^2 ))
+ (d9
^2 )))) by
A10,
XXREAL_0: 2;
then ((
dist_cart3S (X,Y,Z))
. (x,z))
<= ((
sqrt (((d2
^2 )
+ (d5
^2 ))
+ (d8
^2 )))
+ (
sqrt (((d3
^2 )
+ (d6
^2 ))
+ (d9
^2 )))) by
A1,
A5,
Def13;
then ((
dist_cart3S (X,Y,Z))
. (x,z))
<= (((
dist_cart3S (X,Y,Z))
. (x,y))
+ (
sqrt (((d3
^2 )
+ (d6
^2 ))
+ (d9
^2 )))) by
A1,
A2,
Def13;
hence thesis by
A2,
A5,
Def13;
end;
definition
let X, Y, Z;
let x,y be
Element of
[:the
carrier of X, the
carrier of Y, the
carrier of Z:];
::
METRIC_3:def14
func
dist3S (x,y) ->
Real equals ((
dist_cart3S (X,Y,Z))
. (x,y));
coherence ;
end
definition
let X, Y, Z;
::
METRIC_3:def15
func
MetrSpaceCart3S (X,Y,Z) ->
strict non
empty
MetrSpace equals
MetrStruct (#
[:the
carrier of X, the
carrier of Y, the
carrier of Z:], (
dist_cart3S (X,Y,Z)) #);
coherence
proof
now
let x,y,z be
Element of
MetrStruct (#
[:the
carrier of X, the
carrier of Y, the
carrier of Z:], (
dist_cart3S (X,Y,Z)) #);
reconsider x9 = x, y9 = y, z9 = z as
Element of
[:the
carrier of X, the
carrier of Y, the
carrier of Z:];
A1: (
dist (x,y))
= ((
dist_cart3S (X,Y,Z))
. (x9,y9)) by
METRIC_1:def 1;
hence (
dist (x,y))
=
0 iff x
= y by
Th14;
(
dist (y,x))
= ((
dist_cart3S (X,Y,Z))
. (y9,x9)) by
METRIC_1:def 1;
hence (
dist (x,y))
= (
dist (y,x)) by
A1,
Th15;
(
dist (x,z))
= ((
dist_cart3S (X,Y,Z))
. (x9,z9)) & (
dist (y,z))
= ((
dist_cart3S (X,Y,Z))
. (y9,z9)) by
METRIC_1:def 1;
hence (
dist (x,z))
<= ((
dist (x,y))
+ (
dist (y,z))) by
A1,
Th18;
end;
hence thesis by
METRIC_1: 6;
end;
end
definition
::
METRIC_3:def16
func
taxi_dist2 ->
Function of
[:
[:
REAL ,
REAL :],
[:
REAL ,
REAL :]:],
REAL means
:
Def16: for x1,y1,x2,y2 be
Element of
REAL holds for x,y be
Element of
[:
REAL ,
REAL :] st x
=
[x1, x2] & y
=
[y1, y2] holds (it
. (x,y))
= ((
real_dist
. (x1,y1))
+ (
real_dist
. (x2,y2)));
existence
proof
deffunc
G(
Element of
REAL ,
Element of
REAL ,
Element of
REAL ,
Element of
REAL ) = ((
real_dist
. ($1,$2))
+ (
real_dist
. ($3,$4)));
consider F be
Function of
[:
[:
REAL ,
REAL :],
[:
REAL ,
REAL :]:],
REAL such that
A1: for x1,y1,x2,y2 be
Element of
REAL holds for x,y be
Element of
[:
REAL ,
REAL :] st x
=
[x1, x2] & y
=
[y1, y2] holds (F
. (x,y))
=
G(x1,y1,x2,y2) from
LambdaMCART;
take F;
let x1,y1,x2,y2 be
Element of
REAL , x,y be
Element of
[:
REAL ,
REAL :];
assume x
=
[x1, x2] & y
=
[y1, y2];
hence thesis by
A1;
end;
uniqueness
proof
let f1,f2 be
Function of
[:
[:
REAL ,
REAL :],
[:
REAL ,
REAL :]:],
REAL ;
assume that
A2: for x1,y1,x2,y2 be
Element of
REAL holds for x,y be
Element of
[:
REAL ,
REAL :] st x
=
[x1, x2] & y
=
[y1, y2] holds (f1
. (x,y))
= ((
real_dist
. (x1,y1))
+ (
real_dist
. (x2,y2))) and
A3: for x1,y1,x2,y2 be
Element of
REAL holds for x,y be
Element of
[:
REAL ,
REAL :] st x
=
[x1, x2] & y
=
[y1, y2] holds (f2
. (x,y))
= ((
real_dist
. (x1,y1))
+ (
real_dist
. (x2,y2)));
for x,y be
Element of
[:
REAL ,
REAL :] holds (f1
. (x,y))
= (f2
. (x,y))
proof
let x,y be
Element of
[:
REAL ,
REAL :];
consider x1,x2 be
Element of
REAL such that
A4: x
=
[x1, x2] by
DOMAIN_1: 1;
consider y1,y2 be
Element of
REAL such that
A5: y
=
[y1, y2] by
DOMAIN_1: 1;
thus (f1
. (x,y))
= ((
real_dist
. (x1,y1))
+ (
real_dist
. (x2,y2))) by
A2,
A4,
A5
.= (f2
. (x,y)) by
A3,
A4,
A5;
end;
hence thesis by
BINOP_1: 2;
end;
end
theorem ::
METRIC_3:19
Th19: for x,y be
Element of
[:
REAL ,
REAL :] holds (
taxi_dist2
. (x,y))
=
0 iff x
= y
proof
let x,y be
Element of
[:
REAL ,
REAL :];
reconsider x1 = (x
`1 ), x2 = (x
`2 ), y1 = (y
`1 ), y2 = (y
`2 ) as
Element of
REAL ;
A1: x
=
[x1, x2] & y
=
[y1, y2];
thus (
taxi_dist2
. (x,y))
=
0 implies x
= y
proof
set d2 = (
real_dist
. (x2,y2));
set d1 = (
real_dist
. (x1,y1));
d1
=
|.(x1
- y1).| by
METRIC_1:def 12;
then
A2:
0
<= d1 by
COMPLEX1: 46;
d2
=
|.(x2
- y2).| by
METRIC_1:def 12;
then
A3:
0
<= d2 by
COMPLEX1: 46;
assume (
taxi_dist2
. (x,y))
=
0 ;
then
A4: (d1
+ d2)
=
0 by
A1,
Def16;
then d1
=
0 by
A2,
A3,
XREAL_1: 27;
then
A5: x1
= y1 by
METRIC_1: 8;
d2
=
0 by
A4,
A2,
A3,
XREAL_1: 27;
hence thesis by
A1,
A5,
METRIC_1: 8;
end;
assume
A6: x
= y;
then
A7: (
real_dist
. (x2,y2))
=
0 by
METRIC_1: 8;
(
taxi_dist2
. (x,y))
= ((
real_dist
. (x1,y1))
+ (
real_dist
. (x2,y2))) by
A1,
Def16
.=
0 by
A6,
A7,
METRIC_1: 8;
hence thesis;
end;
theorem ::
METRIC_3:20
Th20: for x,y be
Element of
[:
REAL ,
REAL :] holds (
taxi_dist2
. (x,y))
= (
taxi_dist2
. (y,x))
proof
let x,y be
Element of
[:
REAL ,
REAL :];
reconsider x1 = (x
`1 ), x2 = (x
`2 ), y1 = (y
`1 ), y2 = (y
`2 ) as
Element of
REAL ;
A1: x
=
[x1, x2] & y
=
[y1, y2];
then (
taxi_dist2
. (x,y))
= ((
real_dist
. (x1,y1))
+ (
real_dist
. (x2,y2))) by
Def16
.= ((
real_dist
. (y1,x1))
+ (
real_dist
. (x2,y2))) by
METRIC_1: 9
.= ((
real_dist
. (y1,x1))
+ (
real_dist
. (y2,x2))) by
METRIC_1: 9
.= (
taxi_dist2
. (y,x)) by
A1,
Def16;
hence thesis;
end;
theorem ::
METRIC_3:21
Th21: for x,y,z be
Element of
[:
REAL ,
REAL :] holds (
taxi_dist2
. (x,z))
<= ((
taxi_dist2
. (x,y))
+ (
taxi_dist2
. (y,z)))
proof
let x,y,z be
Element of
[:
REAL ,
REAL :];
reconsider x1 = (x
`1 ), x2 = (x
`2 ), y1 = (y
`1 ), y2 = (y
`2 ), z1 = (z
`1 ), z2 = (z
`2 ) as
Element of
REAL ;
A1: y
=
[y1, y2];
set d5 = (
real_dist
. (x2,y2)), d6 = (
real_dist
. (y2,z2));
set d3 = (
real_dist
. (y1,z1)), d4 = (
real_dist
. (x2,z2));
set d1 = (
real_dist
. (x1,z1)), d2 = (
real_dist
. (x1,y1));
A2: z
=
[z1, z2];
A3: x
=
[x1, x2];
then
A4: (
taxi_dist2
. (x,z))
= (d1
+ d4) by
A2,
Def16;
A5: d1
<= (d2
+ d3) & d4
<= (d5
+ d6) by
METRIC_1: 10;
((d2
+ d3)
+ (d5
+ d6))
= ((d2
+ d5)
+ (d3
+ d6))
.= ((
taxi_dist2
. (x,y))
+ (d3
+ d6)) by
A3,
A1,
Def16
.= ((
taxi_dist2
. (x,y))
+ (
taxi_dist2
. (y,z))) by
A1,
A2,
Def16;
hence thesis by
A5,
A4,
XREAL_1: 7;
end;
definition
::
METRIC_3:def17
func
RealSpaceCart2 ->
strict non
empty
MetrSpace equals
MetrStruct (#
[:
REAL ,
REAL :],
taxi_dist2 #);
coherence
proof
now
let x,y,z be
Element of
MetrStruct (#
[:
REAL ,
REAL :],
taxi_dist2 #);
reconsider x9 = x, y9 = y, z9 = z as
Element of
[:
REAL ,
REAL :];
A1: (
dist (x,y))
= (
taxi_dist2
. (x9,y9)) by
METRIC_1:def 1;
hence (
dist (x,y))
=
0 iff x
= y by
Th19;
(
dist (y,x))
= (
taxi_dist2
. (y9,x9)) by
METRIC_1:def 1;
hence (
dist (x,y))
= (
dist (y,x)) by
A1,
Th20;
(
dist (x,z))
= (
taxi_dist2
. (x9,z9)) & (
dist (y,z))
= (
taxi_dist2
. (y9,z9)) by
METRIC_1:def 1;
hence (
dist (x,z))
<= ((
dist (x,y))
+ (
dist (y,z))) by
A1,
Th21;
end;
hence thesis by
METRIC_1: 6;
end;
end
definition
::
METRIC_3:def18
func
Eukl_dist2 ->
Function of
[:
[:
REAL ,
REAL :],
[:
REAL ,
REAL :]:],
REAL means
:
Def18: for x1,y1,x2,y2 be
Element of
REAL holds for x,y be
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
proof
deffunc
G(
Element of
REAL ,
Element of
REAL ,
Element of
REAL ,
Element of
REAL ) = (
In ((
sqrt (((
real_dist
. ($1,$2))
^2 )
+ ((
real_dist
. ($3,$4))
^2 ))),
REAL ));
consider F be
Function of
[:
[:
REAL ,
REAL :],
[:
REAL ,
REAL :]:],
REAL such that
A1: for x1,y1,x2,y2 be
Element of
REAL holds for x,y be
Element of
[:
REAL ,
REAL :] st x
=
[x1, x2] & y
=
[y1, y2] holds (F
. (x,y))
=
G(x1,y1,x2,y2) from
LambdaMCART;
take F;
let x1,y1,x2,y2 be
Element of
REAL , x,y be
Element of
[:
REAL ,
REAL :];
assume x
=
[x1, x2] & y
=
[y1, y2];
then (F
. (x,y))
=
G(x1,y1,x2,y2) by
A1;
hence thesis;
end;
uniqueness
proof
let f1,f2 be
Function of
[:
[:
REAL ,
REAL :],
[:
REAL ,
REAL :]:],
REAL ;
assume that
A2: for x1,y1,x2,y2 be
Element of
REAL holds for x,y be
Element of
[:
REAL ,
REAL :] st x
=
[x1, x2] & y
=
[y1, y2] holds (f1
. (x,y))
= (
sqrt (((
real_dist
. (x1,y1))
^2 )
+ ((
real_dist
. (x2,y2))
^2 ))) and
A3: for x1,y1,x2,y2 be
Element of
REAL holds for x,y be
Element of
[:
REAL ,
REAL :] st x
=
[x1, x2] & y
=
[y1, y2] holds (f2
. (x,y))
= (
sqrt (((
real_dist
. (x1,y1))
^2 )
+ ((
real_dist
. (x2,y2))
^2 )));
for x,y be
Element of
[:
REAL ,
REAL :] holds (f1
. (x,y))
= (f2
. (x,y))
proof
let x,y be
Element of
[:
REAL ,
REAL :];
consider x1,x2 be
Element of
REAL such that
A4: x
=
[x1, x2] by
DOMAIN_1: 1;
consider y1,y2 be
Element of
REAL such that
A5: y
=
[y1, y2] by
DOMAIN_1: 1;
thus (f1
. (x,y))
= (
sqrt (((
real_dist
. (x1,y1))
^2 )
+ ((
real_dist
. (x2,y2))
^2 ))) by
A2,
A4,
A5
.= (f2
. (x,y)) by
A3,
A4,
A5;
end;
hence thesis by
BINOP_1: 2;
end;
end
theorem ::
METRIC_3:22
Th22: for x,y be
Element of
[:
REAL ,
REAL :] holds (
Eukl_dist2
. (x,y))
=
0 iff x
= y
proof
let x,y be
Element of
[:
REAL ,
REAL :];
reconsider x1 = (x
`1 ), x2 = (x
`2 ), y1 = (y
`1 ), y2 = (y
`2 ) as
Element of
REAL ;
A1: x
=
[x1, x2] & y
=
[y1, y2];
thus (
Eukl_dist2
. (x,y))
=
0 implies x
= y
proof
set d2 = (
real_dist
. (x2,y2));
set d1 = (
real_dist
. (x1,y1));
assume (
Eukl_dist2
. (x,y))
=
0 ;
then
A2: (
sqrt ((d1
^2 )
+ (d2
^2 )))
=
0 by
A1,
Def18;
A3:
0
<= (d1
^2 ) &
0
<= (d2
^2 ) by
XREAL_1: 63;
then d1
=
0 by
A2,
Lm1;
then
A4: x1
= y1 by
METRIC_1: 8;
d2
=
0 by
A2,
A3,
Lm1;
hence thesis by
A1,
A4,
METRIC_1: 8;
end;
assume x
= y;
then
A5: ((
real_dist
. (x1,y1))
^2 )
= (
0
^2 ) & ((
real_dist
. (x2,y2))
^2 )
= (
0
^2 ) by
METRIC_1: 8;
(
Eukl_dist2
. (x,y))
= (
sqrt (((
real_dist
. (x1,y1))
^2 )
+ ((
real_dist
. (x2,y2))
^2 ))) by
A1,
Def18
.=
0 by
A5,
Lm1;
hence thesis;
end;
theorem ::
METRIC_3:23
Th23: for x,y be
Element of
[:
REAL ,
REAL :] holds (
Eukl_dist2
. (x,y))
= (
Eukl_dist2
. (y,x))
proof
let x,y be
Element of
[:
REAL ,
REAL :];
reconsider x1 = (x
`1 ), x2 = (x
`2 ), y1 = (y
`1 ), y2 = (y
`2 ) as
Element of
REAL ;
A1: x
=
[x1, x2] & y
=
[y1, y2];
then (
Eukl_dist2
. (x,y))
= (
sqrt (((
real_dist
. (x1,y1))
^2 )
+ ((
real_dist
. (x2,y2))
^2 ))) by
Def18
.= (
sqrt (((
real_dist
. (y1,x1))
^2 )
+ ((
real_dist
. (x2,y2))
^2 ))) by
METRIC_1: 9
.= (
sqrt (((
real_dist
. (y1,x1))
^2 )
+ ((
real_dist
. (y2,x2))
^2 ))) by
METRIC_1: 9
.= (
Eukl_dist2
. (y,x)) by
A1,
Def18;
hence thesis;
end;
theorem ::
METRIC_3:24
Th24: for x,y,z be
Element of
[:
REAL ,
REAL :] holds (
Eukl_dist2
. (x,z))
<= ((
Eukl_dist2
. (x,y))
+ (
Eukl_dist2
. (y,z)))
proof
let x,y,z be
Element of
[:
REAL ,
REAL :];
reconsider x1 = (x
`1 ), x2 = (x
`2 ), y1 = (y
`1 ), y2 = (y
`2 ), z1 = (z
`1 ), z2 = (z
`2 ) as
Element of
REAL ;
A1: x
=
[x1, x2];
set d5 = (
real_dist
. (x2,y2));
set d3 = (
real_dist
. (y1,z1));
set d1 = (
real_dist
. (x1,z1));
A2: y
=
[y1, y2];
set d6 = (
real_dist
. (y2,z2));
set d4 = (
real_dist
. (x2,z2));
set d2 = (
real_dist
. (x1,y1));
A3: z
=
[z1, z2];
d4
=
|.(x2
- z2).| by
METRIC_1:def 12;
then
0
<= d4 by
COMPLEX1: 46;
then
A4: (d4
^2 )
<= ((d5
+ d6)
^2 ) by
METRIC_1: 10,
SQUARE_1: 15;
0
<= (d1
^2 ) &
0
<= (d4
^2 ) by
XREAL_1: 63;
then
A5: (
0
+
0 )
<= ((d1
^2 )
+ (d4
^2 )) by
XREAL_1: 7;
d1
=
|.(x1
- z1).| by
METRIC_1:def 12;
then
0
<= d1 by
COMPLEX1: 46;
then (d1
^2 )
<= ((d2
+ d3)
^2 ) by
METRIC_1: 10,
SQUARE_1: 15;
then ((d1
^2 )
+ (d4
^2 ))
<= (((d2
+ d3)
^2 )
+ ((d5
+ d6)
^2 )) by
A4,
XREAL_1: 7;
then
A6: (
sqrt ((d1
^2 )
+ (d4
^2 )))
<= (
sqrt (((d2
+ d3)
^2 )
+ ((d5
+ d6)
^2 ))) by
A5,
SQUARE_1: 26;
d6
=
|.(y2
- z2).| by
METRIC_1:def 12;
then
A7:
0
<= d6 by
COMPLEX1: 46;
d5
=
|.(x2
- y2).| by
METRIC_1:def 12;
then
A8:
0
<= d5 by
COMPLEX1: 46;
d3
=
|.(y1
- z1).| by
METRIC_1:def 12;
then
A9:
0
<= d3 by
COMPLEX1: 46;
d2
=
|.(x1
- y1).| by
METRIC_1:def 12;
then
0
<= d2 by
COMPLEX1: 46;
then (
sqrt (((d2
+ d3)
^2 )
+ ((d5
+ d6)
^2 )))
<= ((
sqrt ((d2
^2 )
+ (d5
^2 )))
+ (
sqrt ((d3
^2 )
+ (d6
^2 )))) by
A9,
A8,
A7,
Th12;
then (
sqrt ((d1
^2 )
+ (d4
^2 )))
<= ((
sqrt ((d2
^2 )
+ (d5
^2 )))
+ (
sqrt ((d3
^2 )
+ (d6
^2 )))) by
A6,
XXREAL_0: 2;
then (
Eukl_dist2
. (x,z))
<= ((
sqrt ((d2
^2 )
+ (d5
^2 )))
+ (
sqrt ((d3
^2 )
+ (d6
^2 )))) by
A1,
A3,
Def18;
then (
Eukl_dist2
. (x,z))
<= ((
Eukl_dist2
. (x,y))
+ (
sqrt ((d3
^2 )
+ (d6
^2 )))) by
A1,
A2,
Def18;
hence thesis by
A2,
A3,
Def18;
end;
definition
::
METRIC_3:def19
func
EuklSpace2 ->
strict non
empty
MetrSpace equals
MetrStruct (#
[:
REAL ,
REAL :],
Eukl_dist2 #);
coherence
proof
now
let x,y,z be
Element of
MetrStruct (#
[:
REAL ,
REAL :],
Eukl_dist2 #);
reconsider x9 = x, y9 = y, z9 = z as
Element of
[:
REAL ,
REAL :];
A1: (
dist (x,y))
= (
Eukl_dist2
. (x9,y9)) by
METRIC_1:def 1;
hence (
dist (x,y))
=
0 iff x
= y by
Th22;
(
dist (y,x))
= (
Eukl_dist2
. (y9,x9)) by
METRIC_1:def 1;
hence (
dist (x,y))
= (
dist (y,x)) by
A1,
Th23;
(
dist (x,z))
= (
Eukl_dist2
. (x9,z9)) & (
dist (y,z))
= (
Eukl_dist2
. (y9,z9)) by
METRIC_1:def 1;
hence (
dist (x,z))
<= ((
dist (x,y))
+ (
dist (y,z))) by
A1,
Th24;
end;
hence thesis by
METRIC_1: 6;
end;
end
definition
::
METRIC_3:def20
func
taxi_dist3 ->
Function of
[:
[:
REAL ,
REAL ,
REAL :],
[:
REAL ,
REAL ,
REAL :]:],
REAL means
:
Def20: for x1,y1,x2,y2,x3,y3 be
Element of
REAL holds for x,y be
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
proof
deffunc
G(
Element of
REAL ,
Element of
REAL ,
Element of
REAL ,
Element of
REAL ,
Element of
REAL ,
Element of
REAL ) = (((
real_dist
. ($1,$2))
+ (
real_dist
. ($3,$4)))
+ (
real_dist
. ($5,$6)));
consider F be
Function of
[:
[:
REAL ,
REAL ,
REAL :],
[:
REAL ,
REAL ,
REAL :]:],
REAL such that
A1: for x1,y1,x2,y2,x3,y3 be
Element of
REAL holds for x,y be
Element of
[:
REAL ,
REAL ,
REAL :] st x
=
[x1, x2, x3] & y
=
[y1, y2, y3] holds (F
. (x,y))
=
G(x1,y1,x2,y2,x3,y3) from
LambdaMCART1;
take F;
let x1,y1,x2,y2,x3,y3 be
Element of
REAL , x,y be
Element of
[:
REAL ,
REAL ,
REAL :];
assume x
=
[x1, x2, x3] & y
=
[y1, y2, y3];
hence thesis by
A1;
end;
uniqueness
proof
let f1,f2 be
Function of
[:
[:
REAL ,
REAL ,
REAL :],
[:
REAL ,
REAL ,
REAL :]:],
REAL ;
assume that
A2: for x1,y1,x2,y2,x3,y3 be
Element of
REAL holds for x,y be
Element of
[:
REAL ,
REAL ,
REAL :] st x
=
[x1, x2, x3] & y
=
[y1, y2, y3] holds (f1
. (x,y))
= (((
real_dist
. (x1,y1))
+ (
real_dist
. (x2,y2)))
+ (
real_dist
. (x3,y3))) and
A3: for x1,y1,x2,y2,x3,y3 be
Element of
REAL holds for x,y be
Element of
[:
REAL ,
REAL ,
REAL :] st x
=
[x1, x2, x3] & y
=
[y1, y2, y3] holds (f2
. (x,y))
= (((
real_dist
. (x1,y1))
+ (
real_dist
. (x2,y2)))
+ (
real_dist
. (x3,y3)));
for x,y be
Element of
[:
REAL ,
REAL ,
REAL :] holds (f1
. (x,y))
= (f2
. (x,y))
proof
let x,y be
Element of
[:
REAL ,
REAL ,
REAL :];
consider x1,x2,x3 be
Element of
REAL such that
A4: x
=
[x1, x2, x3] by
DOMAIN_1: 3;
consider y1,y2,y3 be
Element of
REAL such that
A5: y
=
[y1, y2, y3] by
DOMAIN_1: 3;
thus (f1
. (x,y))
= (((
real_dist
. (x1,y1))
+ (
real_dist
. (x2,y2)))
+ (
real_dist
. (x3,y3))) by
A2,
A4,
A5
.= (f2
. (x,y)) by
A3,
A4,
A5;
end;
hence thesis by
BINOP_1: 2;
end;
end
theorem ::
METRIC_3:25
Th25: for x,y be
Element of
[:
REAL ,
REAL ,
REAL :] holds (
taxi_dist3
. (x,y))
=
0 iff x
= y
proof
let x,y be
Element of
[:
REAL ,
REAL ,
REAL :];
reconsider x1 = (x
`1_3 ), x2 = (x
`2_3 ), x3 = (x
`3_3 ), y1 = (y
`1_3 ), y2 = (y
`2_3 ), y3 = (y
`3_3 ) as
Element of
REAL ;
A1: x
=
[x1, x2, x3] & y
=
[y1, y2, y3];
thus (
taxi_dist3
. (x,y))
=
0 implies x
= y
proof
set d3 = (
real_dist
. (x3,y3));
set d2 = (
real_dist
. (x2,y2));
set d1 = (
real_dist
. (x1,y1));
set d4 = (d1
+ d2);
d3
=
|.(x3
- y3).| by
METRIC_1:def 12;
then
A2:
0
<= d3 by
COMPLEX1: 46;
d1
=
|.(x1
- y1).| by
METRIC_1:def 12;
then
A3:
0
<= d1 by
COMPLEX1: 46;
assume (
taxi_dist3
. (x,y))
=
0 ;
then
A4: (d4
+ d3)
=
0 by
A1,
Def20;
d2
=
|.(x2
- y2).| by
METRIC_1:def 12;
then
A5:
0
<= d2 by
COMPLEX1: 46;
then
A6: (
0
+
0 )
<= (d1
+ d2) by
A3,
XREAL_1: 7;
then
A7: d4
=
0 by
A4,
A2,
XREAL_1: 27;
then d1
=
0 by
A5,
A3,
XREAL_1: 27;
then
A8: x1
= y1 by
METRIC_1: 8;
d3
=
0 by
A4,
A2,
A6,
XREAL_1: 27;
then
A9: x3
= y3 by
METRIC_1: 8;
d2
=
0 by
A5,
A3,
A7,
XREAL_1: 27;
hence thesis by
A1,
A9,
A8,
METRIC_1: 8;
end;
assume
A10: x
= y;
then
A11: (
real_dist
. (x1,y1))
=
0 & (
real_dist
. (x2,y2))
=
0 by
METRIC_1: 8;
(
taxi_dist3
. (x,y))
= (((
real_dist
. (x1,y1))
+ (
real_dist
. (x2,y2)))
+ (
real_dist
. (x3,y3))) by
A1,
Def20
.=
0 by
A10,
A11,
METRIC_1: 8;
hence thesis;
end;
theorem ::
METRIC_3:26
Th26: for x,y be
Element of
[:
REAL ,
REAL ,
REAL :] holds (
taxi_dist3
. (x,y))
= (
taxi_dist3
. (y,x))
proof
let x,y be
Element of
[:
REAL ,
REAL ,
REAL :];
reconsider x1 = (x
`1_3 ), x2 = (x
`2_3 ), x3 = (x
`3_3 ), y1 = (y
`1_3 ), y2 = (y
`2_3 ), y3 = (y
`3_3 ) as
Element of
REAL ;
A1: x
=
[x1, x2, x3] & y
=
[y1, y2, y3];
then (
taxi_dist3
. (x,y))
= (((
real_dist
. (x1,y1))
+ (
real_dist
. (x2,y2)))
+ (
real_dist
. (x3,y3))) by
Def20
.= (((
real_dist
. (y1,x1))
+ (
real_dist
. (x2,y2)))
+ (
real_dist
. (x3,y3))) by
METRIC_1: 9
.= (((
real_dist
. (y1,x1))
+ (
real_dist
. (y2,x2)))
+ (
real_dist
. (x3,y3))) by
METRIC_1: 9
.= (((
real_dist
. (y1,x1))
+ (
real_dist
. (y2,x2)))
+ (
real_dist
. (y3,x3))) by
METRIC_1: 9
.= (
taxi_dist3
. (y,x)) by
A1,
Def20;
hence thesis;
end;
theorem ::
METRIC_3:27
Th27: for x,y,z be
Element of
[:
REAL ,
REAL ,
REAL :] holds (
taxi_dist3
. (x,z))
<= ((
taxi_dist3
. (x,y))
+ (
taxi_dist3
. (y,z)))
proof
let x,y,z be
Element of
[:
REAL ,
REAL ,
REAL :];
reconsider x1 = (x
`1_3 ), x2 = (x
`2_3 ), x3 = (x
`3_3 ), y1 = (y
`1_3 ), y2 = (y
`2_3 ), y3 = (y
`3_3 ), z1 = (z
`1_3 ), z2 = (z
`2_3 ), z3 = (z
`3_3 ) as
Element of
REAL ;
A1: x
=
[x1, x2, x3];
set d7 = (
real_dist
. (x3,z3)), d8 = (
real_dist
. (x3,y3));
set d3 = (
real_dist
. (y1,z1)), d4 = (
real_dist
. (x2,z2));
A2: z
=
[z1, z2, z3];
set d9 = (
real_dist
. (y3,z3));
set d5 = (
real_dist
. (x2,y2)), d6 = (
real_dist
. (y2,z2));
set d1 = (
real_dist
. (x1,z1)), d2 = (
real_dist
. (x1,y1));
A3: y
=
[y1, y2, y3];
set d10 = (d1
+ d4);
d1
<= (d2
+ d3) & d4
<= (d5
+ d6) by
METRIC_1: 10;
then
A4: d10
<= ((d2
+ d3)
+ (d5
+ d6)) by
XREAL_1: 7;
d7
<= (d8
+ d9) by
METRIC_1: 10;
then
A5: (d10
+ d7)
<= (((d2
+ d3)
+ (d5
+ d6))
+ (d8
+ d9)) by
A4,
XREAL_1: 7;
(((d2
+ d3)
+ (d5
+ d6))
+ (d8
+ d9))
= (((d2
+ d5)
+ d8)
+ ((d3
+ d6)
+ d9))
.= ((
taxi_dist3
. (x,y))
+ ((d3
+ d6)
+ d9)) by
A1,
A3,
Def20
.= ((
taxi_dist3
. (x,y))
+ (
taxi_dist3
. (y,z))) by
A3,
A2,
Def20;
hence thesis by
A1,
A2,
A5,
Def20;
end;
definition
::
METRIC_3:def21
func
RealSpaceCart3 ->
strict non
empty
MetrSpace equals
MetrStruct (#
[:
REAL ,
REAL ,
REAL :],
taxi_dist3 #);
coherence
proof
now
let x,y,z be
Element of
MetrStruct (#
[:
REAL ,
REAL ,
REAL :],
taxi_dist3 #);
reconsider x9 = x, y9 = y, z9 = z as
Element of
[:
REAL ,
REAL ,
REAL :];
A1: (
dist (x,y))
= (
taxi_dist3
. (x9,y9)) by
METRIC_1:def 1;
hence (
dist (x,y))
=
0 iff x
= y by
Th25;
(
dist (y,x))
= (
taxi_dist3
. (y9,x9)) by
METRIC_1:def 1;
hence (
dist (x,y))
= (
dist (y,x)) by
A1,
Th26;
(
dist (x,z))
= (
taxi_dist3
. (x9,z9)) & (
dist (y,z))
= (
taxi_dist3
. (y9,z9)) by
METRIC_1:def 1;
hence (
dist (x,z))
<= ((
dist (x,y))
+ (
dist (y,z))) by
A1,
Th27;
end;
hence thesis by
METRIC_1: 6;
end;
end
definition
::
METRIC_3:def22
func
Eukl_dist3 ->
Function of
[:
[:
REAL ,
REAL ,
REAL :],
[:
REAL ,
REAL ,
REAL :]:],
REAL means
:
Def22: for x1,y1,x2,y2,x3,y3 be
Element of
REAL holds for x,y be
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
proof
deffunc
G(
Element of
REAL ,
Element of
REAL ,
Element of
REAL ,
Element of
REAL ,
Element of
REAL ,
Element of
REAL ) = (
In ((
sqrt ((((
real_dist
. ($1,$2))
^2 )
+ ((
real_dist
. ($3,$4))
^2 ))
+ ((
real_dist
. ($5,$6))
^2 ))),
REAL ));
consider F be
Function of
[:
[:
REAL ,
REAL ,
REAL :],
[:
REAL ,
REAL ,
REAL :]:],
REAL such that
A1: for x1,y1,x2,y2,x3,y3 be
Element of
REAL holds for x,y be
Element of
[:
REAL ,
REAL ,
REAL :] st x
=
[x1, x2, x3] & y
=
[y1, y2, y3] holds (F
. (x,y))
=
G(x1,y1,x2,y2,x3,y3) from
LambdaMCART1;
take F;
let x1,y1,x2,y2,x3,y3 be
Element of
REAL , x,y be
Element of
[:
REAL ,
REAL ,
REAL :];
assume x
=
[x1, x2, x3] & y
=
[y1, y2, y3];
then (F
. (x,y))
=
G(x1,y1,x2,y2,x3,y3) by
A1;
hence thesis;
end;
uniqueness
proof
let f1,f2 be
Function of
[:
[:
REAL ,
REAL ,
REAL :],
[:
REAL ,
REAL ,
REAL :]:],
REAL ;
assume that
A2: for x1,y1,x2,y2,x3,y3 be
Element of
REAL holds for x,y be
Element of
[:
REAL ,
REAL ,
REAL :] st x
=
[x1, x2, x3] & y
=
[y1, y2, y3] holds (f1
. (x,y))
= (
sqrt ((((
real_dist
. (x1,y1))
^2 )
+ ((
real_dist
. (x2,y2))
^2 ))
+ ((
real_dist
. (x3,y3))
^2 ))) and
A3: for x1,y1,x2,y2,x3,y3 be
Element of
REAL holds for x,y be
Element of
[:
REAL ,
REAL ,
REAL :] st x
=
[x1, x2, x3] & y
=
[y1, y2, y3] holds (f2
. (x,y))
= (
sqrt ((((
real_dist
. (x1,y1))
^2 )
+ ((
real_dist
. (x2,y2))
^2 ))
+ ((
real_dist
. (x3,y3))
^2 )));
for x,y be
Element of
[:
REAL ,
REAL ,
REAL :] holds (f1
. (x,y))
= (f2
. (x,y))
proof
let x,y be
Element of
[:
REAL ,
REAL ,
REAL :];
consider x1,x2,x3 be
Element of
REAL such that
A4: x
=
[x1, x2, x3] by
DOMAIN_1: 3;
consider y1,y2,y3 be
Element of
REAL such that
A5: y
=
[y1, y2, y3] by
DOMAIN_1: 3;
thus (f1
. (x,y))
= (
sqrt ((((
real_dist
. (x1,y1))
^2 )
+ ((
real_dist
. (x2,y2))
^2 ))
+ ((
real_dist
. (x3,y3))
^2 ))) by
A2,
A4,
A5
.= (f2
. (x,y)) by
A3,
A4,
A5;
end;
hence thesis by
BINOP_1: 2;
end;
end
theorem ::
METRIC_3:28
Th28: for x,y be
Element of
[:
REAL ,
REAL ,
REAL :] holds (
Eukl_dist3
. (x,y))
=
0 iff x
= y
proof
let x,y be
Element of
[:
REAL ,
REAL ,
REAL :];
reconsider x1 = (x
`1_3 ), x2 = (x
`2_3 ), x3 = (x
`3_3 ), y1 = (y
`1_3 ), y2 = (y
`2_3 ), y3 = (y
`3_3 ) as
Element of
REAL ;
A1: x
=
[x1, x2, x3] & y
=
[y1, y2, y3];
thus (
Eukl_dist3
. (x,y))
=
0 implies x
= y
proof
set d3 = (
real_dist
. (x3,y3));
set d2 = (
real_dist
. (x2,y2));
set d1 = (
real_dist
. (x1,y1));
A2:
0
<= (d2
^2 ) &
0
<= (d3
^2 ) by
XREAL_1: 63;
assume (
Eukl_dist3
. (x,y))
=
0 ;
then (
sqrt (((d1
^2 )
+ (d2
^2 ))
+ (d3
^2 )))
=
0 by
A1,
Def22;
then
A3: (
sqrt ((d1
^2 )
+ ((d2
^2 )
+ (d3
^2 ))))
=
0 ;
0
<= (d2
^2 ) &
0
<= (d3
^2 ) by
XREAL_1: 63;
then
A4:
0
<= (d1
^2 ) & (
0
+
0 )
<= ((d2
^2 )
+ (d3
^2 )) by
XREAL_1: 7,
XREAL_1: 63;
then d1
=
0 by
A3,
Lm1;
then
A5: x1
= y1 by
METRIC_1: 8;
A6: ((d2
^2 )
+ (d3
^2 ))
=
0 by
A3,
A4,
Lm1;
then d2
=
0 by
A2,
XREAL_1: 27;
then
A7: x2
= y2 by
METRIC_1: 8;
d3
=
0 by
A6,
A2,
XREAL_1: 27;
hence thesis by
A1,
A5,
A7,
METRIC_1: 8;
end;
assume
A8: x
= y;
then
A9: ((
real_dist
. (x1,y1))
^2 )
= (
0
^2 ) & ((
real_dist
. (x2,y2))
^2 )
= (
0
^2 ) by
METRIC_1: 8;
(
Eukl_dist3
. (x,y))
= (
sqrt ((((
real_dist
. (x1,y1))
^2 )
+ ((
real_dist
. (x2,y2))
^2 ))
+ ((
real_dist
. (x3,y3))
^2 ))) by
A1,
Def22
.= (
0
^2 ) by
A8,
A9,
METRIC_1: 8,
SQUARE_1: 17;
hence thesis;
end;
theorem ::
METRIC_3:29
Th29: for x,y be
Element of
[:
REAL ,
REAL ,
REAL :] holds (
Eukl_dist3
. (x,y))
= (
Eukl_dist3
. (y,x))
proof
let x,y be
Element of
[:
REAL ,
REAL ,
REAL :];
reconsider x1 = (x
`1_3 ), x2 = (x
`2_3 ), x3 = (x
`3_3 ), y1 = (y
`1_3 ), y2 = (y
`2_3 ), y3 = (y
`3_3 ) as
Element of
REAL ;
A1: x
=
[x1, x2, x3] & y
=
[y1, y2, y3];
then (
Eukl_dist3
. (x,y))
= (
sqrt ((((
real_dist
. (x1,y1))
^2 )
+ ((
real_dist
. (x2,y2))
^2 ))
+ ((
real_dist
. (x3,y3))
^2 ))) by
Def22
.= (
sqrt ((((
real_dist
. (y1,x1))
^2 )
+ ((
real_dist
. (x2,y2))
^2 ))
+ ((
real_dist
. (x3,y3))
^2 ))) by
METRIC_1: 9
.= (
sqrt ((((
real_dist
. (y1,x1))
^2 )
+ ((
real_dist
. (y2,x2))
^2 ))
+ ((
real_dist
. (x3,y3))
^2 ))) by
METRIC_1: 9
.= (
sqrt ((((
real_dist
. (y1,x1))
^2 )
+ ((
real_dist
. (y2,x2))
^2 ))
+ ((
real_dist
. (y3,x3))
^2 ))) by
METRIC_1: 9
.= (
Eukl_dist3
. (y,x)) by
A1,
Def22;
hence thesis;
end;
theorem ::
METRIC_3:30
Th30: for x,y,z be
Element of
[:
REAL ,
REAL ,
REAL :] holds (
Eukl_dist3
. (x,z))
<= ((
Eukl_dist3
. (x,y))
+ (
Eukl_dist3
. (y,z)))
proof
let x,y,z be
Element of
[:
REAL ,
REAL ,
REAL :];
reconsider x1 = (x
`1_3 ), x2 = (x
`2_3 ), x3 = (x
`3_3 ), y1 = (y
`1_3 ), y2 = (y
`2_3 ), y3 = (y
`3_3 ), z1 = (z
`1_3 ), z2 = (z
`2_3 ), z3 = (z
`3_3 ) as
Element of
REAL ;
A1: x
=
[x1, x2, x3];
set d9 = (
real_dist
. (y3,z3));
set d5 = (
real_dist
. (x2,y2)), d6 = (
real_dist
. (y2,z2));
set d1 = (
real_dist
. (x1,z1)), d2 = (
real_dist
. (x1,y1));
A2: y
=
[y1, y2, y3];
d9
=
|.(y3
- z3).| by
METRIC_1:def 12;
then
A3:
0
<= d9 by
COMPLEX1: 46;
d6
=
|.(y2
- z2).| by
METRIC_1:def 12;
then
A4:
0
<= d6 by
COMPLEX1: 46;
d5
=
|.(x2
- y2).| by
METRIC_1:def 12;
then
A5:
0
<= d5 by
COMPLEX1: 46;
set d7 = (
real_dist
. (x3,z3)), d8 = (
real_dist
. (x3,y3));
set d3 = (
real_dist
. (y1,z1)), d4 = (
real_dist
. (x2,z2));
A6: z
=
[z1, z2, z3];
d7
=
|.(x3
- z3).| by
METRIC_1:def 12;
then
0
<= d7 by
COMPLEX1: 46;
then
A7: (d7
^2 )
<= ((d8
+ d9)
^2 ) by
METRIC_1: 10,
SQUARE_1: 15;
d4
=
|.(x2
- z2).| by
METRIC_1:def 12;
then
0
<= d4 by
COMPLEX1: 46;
then
A8: (d4
^2 )
<= ((d5
+ d6)
^2 ) by
METRIC_1: 10,
SQUARE_1: 15;
d1
=
|.(x1
- z1).| by
METRIC_1:def 12;
then
0
<= d1 by
COMPLEX1: 46;
then (d1
^2 )
<= ((d2
+ d3)
^2 ) by
METRIC_1: 10,
SQUARE_1: 15;
then ((d1
^2 )
+ (d4
^2 ))
<= (((d2
+ d3)
^2 )
+ ((d5
+ d6)
^2 )) by
A8,
XREAL_1: 7;
then
A9: (((d1
^2 )
+ (d4
^2 ))
+ (d7
^2 ))
<= ((((d2
+ d3)
^2 )
+ ((d5
+ d6)
^2 ))
+ ((d8
+ d9)
^2 )) by
A7,
XREAL_1: 7;
0
<= (d1
^2 ) &
0
<= (d4
^2 ) by
XREAL_1: 63;
then
A10: (
0
+
0 )
<= ((d1
^2 )
+ (d4
^2 )) by
XREAL_1: 7;
0
<= (d7
^2 ) by
XREAL_1: 63;
then (
0
+
0 )
<= (((d1
^2 )
+ (d4
^2 ))
+ (d7
^2 )) by
A10,
XREAL_1: 7;
then
A11: (
sqrt (((d1
^2 )
+ (d4
^2 ))
+ (d7
^2 )))
<= (
sqrt ((((d2
+ d3)
^2 )
+ ((d5
+ d6)
^2 ))
+ ((d8
+ d9)
^2 ))) by
A9,
SQUARE_1: 26;
d8
=
|.(x3
- y3).| by
METRIC_1:def 12;
then
A12:
0
<= d8 by
COMPLEX1: 46;
d3
=
|.(y1
- z1).| by
METRIC_1:def 12;
then
A13:
0
<= d3 by
COMPLEX1: 46;
d2
=
|.(x1
- y1).| by
METRIC_1:def 12;
then
0
<= d2 by
COMPLEX1: 46;
then (
sqrt ((((d2
+ d3)
^2 )
+ ((d5
+ d6)
^2 ))
+ ((d8
+ d9)
^2 )))
<= ((
sqrt (((d2
^2 )
+ (d5
^2 ))
+ (d8
^2 )))
+ (
sqrt (((d3
^2 )
+ (d6
^2 ))
+ (d9
^2 )))) by
A13,
A5,
A4,
A12,
A3,
Lm2;
then (
sqrt (((d1
^2 )
+ (d4
^2 ))
+ (d7
^2 )))
<= ((
sqrt (((d2
^2 )
+ (d5
^2 ))
+ (d8
^2 )))
+ (
sqrt (((d3
^2 )
+ (d6
^2 ))
+ (d9
^2 )))) by
A11,
XXREAL_0: 2;
then (
Eukl_dist3
. (x,z))
<= ((
sqrt (((d2
^2 )
+ (d5
^2 ))
+ (d8
^2 )))
+ (
sqrt (((d3
^2 )
+ (d6
^2 ))
+ (d9
^2 )))) by
A1,
A6,
Def22;
then (
Eukl_dist3
. (x,z))
<= ((
Eukl_dist3
. (x,y))
+ (
sqrt (((d3
^2 )
+ (d6
^2 ))
+ (d9
^2 )))) by
A1,
A2,
Def22;
hence thesis by
A2,
A6,
Def22;
end;
definition
::
METRIC_3:def23
func
EuklSpace3 ->
strict non
empty
MetrSpace equals
MetrStruct (#
[:
REAL ,
REAL ,
REAL :],
Eukl_dist3 #);
coherence
proof
now
let x,y,z be
Element of
MetrStruct (#
[:
REAL ,
REAL ,
REAL :],
Eukl_dist3 #);
reconsider x9 = x, y9 = y, z9 = z as
Element of
[:
REAL ,
REAL ,
REAL :];
A1: (
dist (x,y))
= (
Eukl_dist3
. (x9,y9)) by
METRIC_1:def 1;
hence (
dist (x,y))
=
0 iff x
= y by
Th28;
(
dist (y,x))
= (
Eukl_dist3
. (y9,x9)) by
METRIC_1:def 1;
hence (
dist (x,y))
= (
dist (y,x)) by
A1,
Th29;
(
dist (x,z))
= (
Eukl_dist3
. (x9,z9)) & (
dist (y,z))
= (
Eukl_dist3
. (y9,z9)) by
METRIC_1:def 1;
hence (
dist (x,z))
<= ((
dist (x,y))
+ (
dist (y,z))) by
A1,
Th30;
end;
hence thesis by
METRIC_1: 6;
end;
end