:: Metric Spaces
:: by Stanis{\l}awa Kanas, Adam Lecko and Mariusz Startek
::
:: Received May 3, 1990
:: Copyright (c) 1990-2011 Association of Mizar Users

begin

definition

attr c₁ is strict ;
struct MetrStruct -> 1-sorted ;
aggr MetrStruct(# carrier, distance #) -> MetrStruct ;
sel distance c₁ -> Function of [: the carrier of c₁, the carrier of c₁:],REAL;

end;

registration

cluster non empty strict MetrStruct ;
existence
ex b₁ being MetrStruct st
( not b₁ is empty & b₁ is strict )

proof end;

end;

definition

let A, B be set ;
let f be PartFunc of [:A,B:],REAL;
let a be Element of A;
let b be Element of B;
:: original: .
redefine func f . (a,b) -> Real;
coherence
f . (a,b) is Real

proof end;

end;

definition

let M be MetrStruct ;
let a, b be Element of M;
func dist (a,b) -> Real equals :: METRIC_1:def 1
the distance of M . (a,b);
coherence
the distance of M . (a,b) is Real ;

end;

:: deftheorem defines dist METRIC_1:def 1 :
for M being MetrStruct
for a, b being Element of M holds dist (a,b) = the distance of M . (a,b);

notation

synonym Empty^2-to-zero for op2 ;

end;

definition

:: original: Empty^2-to-zero
redefine func Empty^2-to-zero -> Function of [:1,1:],REAL;
coherence
Empty^2-to-zero is Function of [:1,1:],REAL

proof end;

end;

Lm1: op2 . ({},{}) = 0

proof end;

Lm2: for x, y being Element of 1 holds
( op2 . (x,y) = 0 iff x = y )

proof end;

Lm3: for x, y being Element of 1 holds op2 . (x,y) = op2 . (y,x)

proof end;

registration

cluster Empty^2-to-zero -> natural-valued Function;
coherence
for b₁ being Function st b₁ = op2 holds
b₁ is natural-valued ;

end;

registration

let f be natural-valued Function;
let x, y be set ;
cluster f . (x,y) -> natural ;
coherence
f . (x,y) is natural ;

end;

Lm4: for x, y, z being Element of 1 holds op2 . (x,z) <= (op2 . (x,y)) + (op2 . (y,z))

proof end;

definition

canceled;
let A be set ;
let f be PartFunc of [:A,A:],REAL;
attr f is Reflexive means :Def3: :: METRIC_1:def 3
for a being Element of A holds f . (a,a) = 0 ;
attr f is discerning means :Def4: :: METRIC_1:def 4
for a, b being Element of A st f . (a,b) = 0 holds
a = b;
attr f is symmetric means :Def5: :: METRIC_1:def 5
for a, b being Element of A holds f . (a,b) = f . (b,a);
attr f is triangle means :Def6: :: METRIC_1:def 6
for a, b, c being Element of A holds f . (a,c) <= (f . (a,b)) + (f . (b,c));

end;

:: deftheorem METRIC_1:def 2 :
canceled;

:: deftheorem Def3 defines Reflexive METRIC_1:def 3 :
for A being set
for f being PartFunc of [:A,A:],REAL holds
( f is Reflexive iff for a being Element of A holds f . (a,a) = 0 );

:: deftheorem Def4 defines discerning METRIC_1:def 4 :
for A being set
for f being PartFunc of [:A,A:],REAL holds
( f is discerning iff for a, b being Element of A st f . (a,b) = 0 holds
a = b );

:: deftheorem Def5 defines symmetric METRIC_1:def 5 :
for A being set
for f being PartFunc of [:A,A:],REAL holds
( f is symmetric iff for a, b being Element of A holds f . (a,b) = f . (b,a) );

:: deftheorem Def6 defines triangle METRIC_1:def 6 :
for A being set
for f being PartFunc of [:A,A:],REAL holds
( f is triangle iff for a, b, c being Element of A holds f . (a,c) <= (f . (a,b)) + (f . (b,c)) );

definition

let M be MetrStruct ;
attr M is Reflexive means :Def7: :: METRIC_1:def 7
the distance of M is Reflexive ;
attr M is discerning means :Def8: :: METRIC_1:def 8
the distance of M is discerning ;
attr M is symmetric means :Def9: :: METRIC_1:def 9
the distance of M is symmetric ;
attr M is triangle means :Def10: :: METRIC_1:def 10
the distance of M is triangle ;

end;

:: deftheorem Def7 defines Reflexive METRIC_1:def 7 :
for M being MetrStruct holds
( M is Reflexive iff the distance of M is Reflexive );

:: deftheorem Def8 defines discerning METRIC_1:def 8 :
for M being MetrStruct holds
( M is discerning iff the distance of M is discerning );

:: deftheorem Def9 defines symmetric METRIC_1:def 9 :
for M being MetrStruct holds
( M is symmetric iff the distance of M is symmetric );

:: deftheorem Def10 defines triangle METRIC_1:def 10 :
for M being MetrStruct holds
( M is triangle iff the distance of M is triangle );

registration

cluster non empty strict Reflexive discerning symmetric triangle MetrStruct ;
existence
ex b₁ being MetrStruct st
( b₁ is strict & b₁ is Reflexive & b₁ is discerning & b₁ is symmetric & b₁ is triangle & not b₁ is empty )

proof end;

end;

definition

mode MetrSpace is Reflexive discerning symmetric triangle MetrStruct ;

end;

theorem Th1: :: METRIC_1:1

for M being MetrStruct holds
( ( for a being Element of M holds dist (a,a) = 0 ) iff M is Reflexive )

proof end;

theorem Th2: :: METRIC_1:2

for M being MetrStruct holds
( ( for a, b being Element of M st dist (a,b) = 0 holds
a = b ) iff M is discerning )

proof end;

theorem Th3: :: METRIC_1:3

for M being MetrStruct st ( for a, b being Element of M holds dist (a,b) = dist (b,a) ) holds
M is symmetric

proof end;

theorem Th4: :: METRIC_1:4

for M being MetrStruct holds
( ( for a, b, c being Element of M holds dist (a,c) <= (dist (a,b)) + (dist (b,c)) ) iff M is triangle )

proof end;

definition

let M be symmetric MetrStruct ;
let a, b be Element of M;
:: original: dist
redefine func dist (a,b) -> Real;
commutativity
for a, b being Element of M holds dist (a,b) = dist (b,a)

proof end;

end;

theorem Th5: :: METRIC_1:5

for M being Reflexive symmetric triangle MetrStruct
for a, b being Element of M holds 0 <= dist (a,b)

proof end;

theorem Th6: :: METRIC_1:6

for M being MetrStruct st ( for a, b, c being Element of M holds
( ( dist (a,b) = 0 implies a = b ) & ( a = b implies dist (a,b) = 0 ) & dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) ) ) holds
M is MetrSpace

proof end;

theorem Th7: :: METRIC_1:7

for M being MetrSpace
for x, y being Element of M st x <> y holds
0 < dist (x,y)

proof end;

definition

let A be set ;
func discrete_dist A -> Function of [:A,A:],REAL means :Def11: :: METRIC_1:def 11
for x, y being Element of A holds
( it . (x,x) = 0 & ( x <> y implies it . (x,y) = 1 ) );
existence
ex b₁ being Function of [:A,A:],REAL st
for x, y being Element of A holds
( b₁ . (x,x) = 0 & ( x <> y implies b₁ . (x,y) = 1 ) )

proof end;

uniqueness
for b₁, b₂ being Function of [:A,A:],REAL st ( for x, y being Element of A holds
( b₁ . (x,x) = 0 & ( x <> y implies b₁ . (x,y) = 1 ) ) ) & ( for x, y being Element of A holds
( b₂ . (x,x) = 0 & ( x <> y implies b₂ . (x,y) = 1 ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def11 defines discrete_dist METRIC_1:def 11 :
for A being set
for b₂ being Function of [:A,A:],REAL holds
( b₂ = discrete_dist A iff for x, y being Element of A holds
( b₂ . (x,x) = 0 & ( x <> y implies b₂ . (x,y) = 1 ) ) );

definition

let A be set ;
func DiscreteSpace A -> strict MetrStruct equals :: METRIC_1:def 12
MetrStruct(# A,(discrete_dist A) #);
coherence
MetrStruct(# A,(discrete_dist A) #) is strict MetrStruct ;

end;

:: deftheorem defines DiscreteSpace METRIC_1:def 12 :
for A being set holds DiscreteSpace A = MetrStruct(# A,(discrete_dist A) #);

registration

let A be non empty set ;
cluster DiscreteSpace A -> non empty strict ;
coherence
not DiscreteSpace A is empty ;

end;

registration

let A be set ;
cluster DiscreteSpace A -> strict Reflexive discerning symmetric triangle ;
coherence
( DiscreteSpace A is Reflexive & DiscreteSpace A is discerning & DiscreteSpace A is symmetric & DiscreteSpace A is triangle )

proof end;

end;

definition

func real_dist -> Function of [:REAL,REAL:],REAL means :Def13: :: METRIC_1:def 13
for x, y being Element of REAL holds it . (x,y) = abs (x - y);
existence
ex b₁ being Function of [:REAL,REAL:],REAL st
for x, y being Element of REAL holds b₁ . (x,y) = abs (x - y)

proof end;

uniqueness
for b₁, b₂ being Function of [:REAL,REAL:],REAL st ( for x, y being Element of REAL holds b₁ . (x,y) = abs (x - y) ) & ( for x, y being Element of REAL holds b₂ . (x,y) = abs (x - y) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def13 defines real_dist METRIC_1:def 13 :
for b₁ being Function of [:REAL,REAL:],REAL holds
( b₁ = real_dist iff for x, y being Element of REAL holds b₁ . (x,y) = abs (x - y) );

theorem :: METRIC_1:8

canceled;

theorem Th9: :: METRIC_1:9

for x, y being Element of REAL holds
( real_dist . (x,y) = 0 iff x = y )

proof end;

theorem Th10: :: METRIC_1:10

for x, y being Element of REAL holds real_dist . (x,y) = real_dist . (y,x)

proof end;

theorem Th11: :: METRIC_1:11

for x, y, z being Element of REAL holds real_dist . (x,y) <= (real_dist . (x,z)) + (real_dist . (z,y))

proof end;

definition

func RealSpace -> strict MetrStruct equals :: METRIC_1:def 14
MetrStruct(# REAL,real_dist #);
coherence
MetrStruct(# REAL,real_dist #) is strict MetrStruct ;

end;

:: deftheorem defines RealSpace METRIC_1:def 14 :
RealSpace = MetrStruct(# REAL,real_dist #);

registration

cluster RealSpace -> non empty strict ;
coherence
not RealSpace is empty ;

end;

registration

cluster RealSpace -> strict Reflexive discerning symmetric triangle ;
coherence
( RealSpace is Reflexive & RealSpace is discerning & RealSpace is symmetric & RealSpace is triangle )

proof end;

end;

definition

let M be MetrStruct ;
let p be Element of M;
let r be real number ;
func Ball (p,r) -> Subset of M means :Def15: :: METRIC_1:def 15
ex M9 being non empty MetrStruct ex p9 being Element of M9 st
( M9 = M & p9 = p & it = { q where q is Element of M9 : dist (p9,q) < r } ) if not M is empty
otherwise it is empty ;
existence
( ( not M is empty implies ex b₁ being Subset of M ex M9 being non empty MetrStruct ex p9 being Element of M9 st
( M9 = M & p9 = p & b₁ = { q where q is Element of M9 : dist (p9,q) < r } ) ) & ( M is empty implies ex b₁ being Subset of M st b₁ is empty ) )

proof end;

correctness
consistency
for b₁ being Subset of M holds verum;
uniqueness
for b₁, b₂ being Subset of M holds
( ( not M is empty & ex M9 being non empty MetrStruct ex p9 being Element of M9 st
( M9 = M & p9 = p & b₁ = { q where q is Element of M9 : dist (p9,q) < r } ) & ex M9 being non empty MetrStruct ex p9 being Element of M9 st
( M9 = M & p9 = p & b₂ = { q where q is Element of M9 : dist (p9,q) < r } ) implies b₁ = b₂ ) & ( M is empty & b₁ is empty & b₂ is empty implies b₁ = b₂ ) );
;

end;

:: deftheorem Def15 defines Ball METRIC_1:def 15 :
for M being MetrStruct
for p being Element of M
for r being real number
for b₄ being Subset of M holds
( ( not M is empty implies ( b₄ = Ball (p,r) iff ex M9 being non empty MetrStruct ex p9 being Element of M9 st
( M9 = M & p9 = p & b₄ = { q where q is Element of M9 : dist (p9,q) < r } ) ) ) & ( M is empty implies ( b₄ = Ball (p,r) iff b₄ is empty ) ) );

definition

let M be MetrStruct ;
let p be Element of M;
let r be real number ;
func cl_Ball (p,r) -> Subset of M means :Def16: :: METRIC_1:def 16
ex M9 being non empty MetrStruct ex p9 being Element of M9 st
( M9 = M & p9 = p & it = { q where q is Element of M9 : dist (p9,q) <= r } ) if not M is empty
otherwise it is empty ;
existence
( ( not M is empty implies ex b₁ being Subset of M ex M9 being non empty MetrStruct ex p9 being Element of M9 st
( M9 = M & p9 = p & b₁ = { q where q is Element of M9 : dist (p9,q) <= r } ) ) & ( M is empty implies ex b₁ being Subset of M st b₁ is empty ) )

proof end;

correctness
consistency
for b₁ being Subset of M holds verum;
uniqueness
for b₁, b₂ being Subset of M holds
( ( not M is empty & ex M9 being non empty MetrStruct ex p9 being Element of M9 st
( M9 = M & p9 = p & b₁ = { q where q is Element of M9 : dist (p9,q) <= r } ) & ex M9 being non empty MetrStruct ex p9 being Element of M9 st
( M9 = M & p9 = p & b₂ = { q where q is Element of M9 : dist (p9,q) <= r } ) implies b₁ = b₂ ) & ( M is empty & b₁ is empty & b₂ is empty implies b₁ = b₂ ) );
;

end;

:: deftheorem Def16 defines cl_Ball METRIC_1:def 16 :
for M being MetrStruct
for p being Element of M
for r being real number
for b₄ being Subset of M holds
( ( not M is empty implies ( b₄ = cl_Ball (p,r) iff ex M9 being non empty MetrStruct ex p9 being Element of M9 st
( M9 = M & p9 = p & b₄ = { q where q is Element of M9 : dist (p9,q) <= r } ) ) ) & ( M is empty implies ( b₄ = cl_Ball (p,r) iff b₄ is empty ) ) );

definition

let M be MetrStruct ;
let p be Element of M;
let r be real number ;
func Sphere (p,r) -> Subset of M means :Def17: :: METRIC_1:def 17
ex M9 being non empty MetrStruct ex p9 being Element of M9 st
( M9 = M & p9 = p & it = { q where q is Element of M9 : dist (p9,q) = r } ) if not M is empty
otherwise it is empty ;
existence
( ( not M is empty implies ex b₁ being Subset of M ex M9 being non empty MetrStruct ex p9 being Element of M9 st
( M9 = M & p9 = p & b₁ = { q where q is Element of M9 : dist (p9,q) = r } ) ) & ( M is empty implies ex b₁ being Subset of M st b₁ is empty ) )

proof end;

correctness
consistency
for b₁ being Subset of M holds verum;
uniqueness
for b₁, b₂ being Subset of M holds
( ( not M is empty & ex M9 being non empty MetrStruct ex p9 being Element of M9 st
( M9 = M & p9 = p & b₁ = { q where q is Element of M9 : dist (p9,q) = r } ) & ex M9 being non empty MetrStruct ex p9 being Element of M9 st
( M9 = M & p9 = p & b₂ = { q where q is Element of M9 : dist (p9,q) = r } ) implies b₁ = b₂ ) & ( M is empty & b₁ is empty & b₂ is empty implies b₁ = b₂ ) );
;

end;

:: deftheorem Def17 defines Sphere METRIC_1:def 17 :
for M being MetrStruct
for p being Element of M
for r being real number
for b₄ being Subset of M holds
( ( not M is empty implies ( b₄ = Sphere (p,r) iff ex M9 being non empty MetrStruct ex p9 being Element of M9 st
( M9 = M & p9 = p & b₄ = { q where q is Element of M9 : dist (p9,q) = r } ) ) ) & ( M is empty implies ( b₄ = Sphere (p,r) iff b₄ is empty ) ) );

Lm5: for r being real number
for M being non empty MetrStruct
for p being Element of M holds Ball (p,r) = { q where q is Element of M : dist (p,q) < r }

proof end;

Lm6: for r being real number
for M being non empty MetrStruct
for p being Element of M holds cl_Ball (p,r) = { q where q is Element of M : dist (p,q) <= r }

proof end;

Lm7: for r being real number
for M being non empty MetrStruct
for p being Element of M holds Sphere (p,r) = { q where q is Element of M : dist (p,q) = r }

proof end;

theorem Th12: :: METRIC_1:12

for r being real number
for M being MetrStruct
for p, x being Element of M holds
( x in Ball (p,r) iff ( not M is empty & dist (p,x) < r ) )

proof end;

theorem Th13: :: METRIC_1:13

for r being real number
for M being MetrStruct
for p, x being Element of M holds
( x in cl_Ball (p,r) iff ( not M is empty & dist (p,x) <= r ) )

proof end;

theorem Th14: :: METRIC_1:14

for r being real number
for M being MetrStruct
for p, x being Element of M holds
( x in Sphere (p,r) iff ( not M is empty & dist (p,x) = r ) )

proof end;

theorem Th15: :: METRIC_1:15

for r being real number
for M being MetrStruct
for p being Element of M holds Ball (p,r) c= cl_Ball (p,r)

proof end;

theorem Th16: :: METRIC_1:16

for r being real number
for M being MetrStruct
for p being Element of M holds Sphere (p,r) c= cl_Ball (p,r)

proof end;

theorem :: METRIC_1:17

for r being real number
for M being MetrStruct
for p being Element of M holds (Sphere (p,r)) \/ (Ball (p,r)) = cl_Ball (p,r)

proof end;

theorem :: METRIC_1:18

for r being real number
for M being non empty MetrStruct
for p being Element of M holds Ball (p,r) = { q where q is Element of M : dist (p,q) < r } by Lm5;

theorem :: METRIC_1:19

for r being real number
for M being non empty MetrStruct
for p being Element of M holds cl_Ball (p,r) = { q where q is Element of M : dist (p,q) <= r } by Lm6;

theorem :: METRIC_1:20

for r being real number
for M being non empty MetrStruct
for p being Element of M holds Sphere (p,r) = { q where q is Element of M : dist (p,q) = r } by Lm7;

begin

Lm8: for M being MetrSpace
for x, y being Element of M st x <> y holds
0 < dist (x,y)
by Th7;

theorem :: METRIC_1:21

for x being set holds Empty^2-to-zero . (x,x) = 0

proof end;

theorem Th22: :: METRIC_1:22

for x, y being Element of 1 st x <> y holds
0 < Empty^2-to-zero . (x,y)

proof end;

theorem Th23: :: METRIC_1:23

for x, y being Element of 1 holds Empty^2-to-zero . (x,y) = Empty^2-to-zero . (y,x) by Lm3;

theorem Th24: :: METRIC_1:24

for x, y, z being Element of 1 holds Empty^2-to-zero . (x,z) <= (Empty^2-to-zero . (x,y)) + (Empty^2-to-zero . (y,z)) by Lm4;

theorem Th25: :: METRIC_1:25

for x, y, z being Element of 1 holds Empty^2-to-zero . (x,z) <= max ((Empty^2-to-zero . (x,y)),(Empty^2-to-zero . (y,z)))

proof end;

set M0 = MetrStruct(# 1,Empty^2-to-zero #);

definition

let A be non empty set ;
let f be Function of [:A,A:],REAL;
attr f is Discerning means :Def18: :: METRIC_1:def 18
for a, b being Element of A st a <> b holds
0 < f . (a,b);

end;

:: deftheorem Def18 defines Discerning METRIC_1:def 18 :
for A being non empty set
for f being Function of [:A,A:],REAL holds
( f is Discerning iff for a, b being Element of A st a <> b holds
0 < f . (a,b) );

definition

let M be non empty MetrStruct ;
attr M is Discerning means :Def19: :: METRIC_1:def 19
the distance of M is Discerning ;

end;

:: deftheorem Def19 defines Discerning METRIC_1:def 19 :
for M being non empty MetrStruct holds
( M is Discerning iff the distance of M is Discerning );

theorem Th26: :: METRIC_1:26

for M being non empty MetrStruct holds
( ( for a, b being Element of M st a <> b holds
0 < dist (a,b) ) iff M is Discerning )

proof end;

registration

cluster MetrStruct(# 1,Empty^2-to-zero #) -> non empty ;
coherence
not MetrStruct(# 1,Empty^2-to-zero #) is empty ;

end;

registration

cluster MetrStruct(# 1,Empty^2-to-zero #) -> Reflexive symmetric triangle Discerning ;
coherence
( MetrStruct(# 1,Empty^2-to-zero #) is Reflexive & MetrStruct(# 1,Empty^2-to-zero #) is symmetric & MetrStruct(# 1,Empty^2-to-zero #) is Discerning & MetrStruct(# 1,Empty^2-to-zero #) is triangle )

proof end;

end;

definition

let M be non empty MetrStruct ;
attr M is ultra means :Def20: :: METRIC_1:def 20
for a, b, c being Element of M holds dist (a,c) <= max ((dist (a,b)),(dist (b,c)));

end;

:: deftheorem Def20 defines ultra METRIC_1:def 20 :
for M being non empty MetrStruct holds
( M is ultra iff for a, b, c being Element of M holds dist (a,c) <= max ((dist (a,b)),(dist (b,c))) );

registration

cluster non empty strict Reflexive symmetric triangle Discerning ultra MetrStruct ;
existence
ex b₁ being non empty MetrStruct st
( b₁ is strict & b₁ is ultra & b₁ is Reflexive & b₁ is symmetric & b₁ is Discerning & b₁ is triangle )

proof end;

end;

theorem Th27: :: METRIC_1:27

for M being non empty Reflexive Discerning MetrStruct
for a, b being Element of M holds 0 <= dist (a,b)

proof end;

definition

mode PseudoMetricSpace is non empty Reflexive symmetric triangle MetrStruct ;
mode SemiMetricSpace is non empty Reflexive symmetric Discerning MetrStruct ;
mode NonSymmetricMetricSpace is non empty Reflexive triangle Discerning MetrStruct ;
mode UltraMetricSpace is non empty Reflexive symmetric Discerning ultra MetrStruct ;

end;

registration

cluster non empty Reflexive discerning symmetric triangle -> non empty Discerning MetrStruct ;
coherence
for b₁ being non empty MetrSpace holds b₁ is Discerning

proof end;

end;

registration

cluster non empty Reflexive symmetric Discerning ultra -> discerning triangle MetrStruct ;
coherence
for b₁ being UltraMetricSpace holds
( b₁ is triangle & b₁ is discerning )

proof end;

end;

definition

func Set_to_zero -> Function of [:2,2:],REAL equals :: METRIC_1:def 21
[:2,2:] --> 0;
coherence
[:2,2:] --> 0 is Function of [:2,2:],REAL ;

end;

:: deftheorem defines Set_to_zero METRIC_1:def 21 :
Set_to_zero = [:2,2:] --> 0;

theorem Th28: :: METRIC_1:28

for x, y being Element of 2 holds Set_to_zero . (x,y) = 0

proof end;

theorem Th29: :: METRIC_1:29

for x, y being Element of 2 holds Set_to_zero . (x,y) = Set_to_zero . (y,x)

proof end;

theorem Th30: :: METRIC_1:30

for x, y, z being Element of 2 holds Set_to_zero . (x,z) <= (Set_to_zero . (x,y)) + (Set_to_zero . (y,z))

proof end;

definition

func ZeroSpace -> MetrStruct equals :: METRIC_1:def 22
MetrStruct(# 2,Set_to_zero #);
coherence
MetrStruct(# 2,Set_to_zero #) is MetrStruct ;

end;

:: deftheorem defines ZeroSpace METRIC_1:def 22 :
ZeroSpace = MetrStruct(# 2,Set_to_zero #);

registration

cluster ZeroSpace -> non empty strict ;
coherence
( ZeroSpace is strict & not ZeroSpace is empty ) ;

end;

registration

cluster ZeroSpace -> Reflexive symmetric triangle ;
coherence
( ZeroSpace is Reflexive & ZeroSpace is symmetric & ZeroSpace is triangle )

proof end;

end;

definition

let S be MetrStruct ;
let p, q, r be Element of S;
pred q is_between p,r means :Def23: :: METRIC_1:def 23
( p <> q & p <> r & q <> r & dist (p,r) = (dist (p,q)) + (dist (q,r)) );

end;

:: deftheorem Def23 defines is_between METRIC_1:def 23 :
for S being MetrStruct
for p, q, r being Element of S holds
( q is_between p,r iff ( p <> q & p <> r & q <> r & dist (p,r) = (dist (p,q)) + (dist (q,r)) ) );

theorem :: METRIC_1:31

for S being non empty Reflexive symmetric triangle MetrStruct
for p, q, r being Element of S st q is_between p,r holds
q is_between r,p

proof end;

theorem :: METRIC_1:32

for S being MetrSpace
for p, q, r being Element of S st q is_between p,r holds
( not p is_between q,r & not r is_between p,q )

proof end;

theorem :: METRIC_1:33

for S being MetrSpace
for p, q, r, s being Element of S st q is_between p,r & r is_between p,s holds
( q is_between p,s & r is_between q,s )

proof end;

definition

let M be non empty MetrStruct ;
let p, r be Element of M;
func open_dist_Segment (p,r) -> Subset of M equals :: METRIC_1:def 24
{ q where q is Element of M : q is_between p,r } ;
coherence
{ q where q is Element of M : q is_between p,r } is Subset of M

proof end;

end;

:: deftheorem defines open_dist_Segment METRIC_1:def 24 :
for M being non empty MetrStruct
for p, r being Element of M holds open_dist_Segment (p,r) = { q where q is Element of M : q is_between p,r } ;

theorem :: METRIC_1:34

for M being non empty MetrSpace
for p, r, x being Element of M holds
( x in open_dist_Segment (p,r) iff x is_between p,r )

proof end;

definition

let M be non empty MetrStruct ;
let p, r be Element of M;
func close_dist_Segment (p,r) -> Subset of M equals :: METRIC_1:def 25
{ q where q is Element of M : q is_between p,r } \/ {p,r};
coherence
{ q where q is Element of M : q is_between p,r } \/ {p,r} is Subset of M

proof end;

end;

:: deftheorem defines close_dist_Segment METRIC_1:def 25 :
for M being non empty MetrStruct
for p, r being Element of M holds close_dist_Segment (p,r) = { q where q is Element of M : q is_between p,r } \/ {p,r};

theorem :: METRIC_1:35

for M being non empty MetrStruct
for p, r, x being Element of M holds
( x in close_dist_Segment (p,r) iff ( x is_between p,r or x = p or x = r ) )

proof end;