:: by Stanis{\l}awa Kanas, Adam Lecko and Mariusz Startek

::

:: Received May 3, 1990

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

definition

attr c_{1} is strict ;

struct MetrStruct -> 1-sorted ;

aggr MetrStruct(# carrier, distance #) -> MetrStruct ;

sel distance c_{1} -> Function of [: the carrier of c_{1}, the carrier of c_{1}:],REAL;

end;
struct MetrStruct -> 1-sorted ;

aggr MetrStruct(# carrier, distance #) -> MetrStruct ;

sel distance c

registration
end;

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

for M being MetrStruct

for a, b being Element of M holds dist (a,b) = the distance of M . (a,b);

Lm1: 0 in REAL

by XREAL_0:def 1;

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

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

coherence

Empty^2-to-zero is Function of [:1,1:],REAL

proof end;

Lm2: op2 . (0,0) = 0

proof end;

Lm3: for x, y being Element of 1 holds

( op2 . (x,y) = 0 iff x = y )

proof end;

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

proof end;

registration
end;

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

proof end;

definition

let A be set ;

let f be PartFunc of [:A,A:],REAL;

end;
let f be PartFunc of [:A,A:],REAL;

attr f is discerning means :: METRIC_1:def 3

for a, b being Element of A st f . (a,b) = 0 holds

a = b;

for a, b being Element of A st f . (a,b) = 0 holds

a = b;

:: deftheorem defines Reflexive METRIC_1:def 2 :

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

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 defines discerning METRIC_1:def 3 :

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

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 defines symmetric METRIC_1:def 4 :

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

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 defines triangle METRIC_1:def 5 :

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

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

:: deftheorem Def6 defines Reflexive METRIC_1:def 6 :

for M being MetrStruct holds

( M is Reflexive iff the distance of M is Reflexive );

for M being MetrStruct holds

( M is Reflexive iff the distance of M is Reflexive );

:: deftheorem Def7 defines discerning METRIC_1:def 7 :

for M being MetrStruct holds

( M is discerning iff the distance of M is discerning );

for M being MetrStruct holds

( M is discerning iff the distance of M is discerning );

:: deftheorem Def8 defines symmetric METRIC_1:def 8 :

for M being MetrStruct holds

( M is symmetric iff the distance of M is symmetric );

for M being MetrStruct holds

( M is symmetric iff the distance of M is symmetric );

:: deftheorem Def9 defines triangle METRIC_1:def 9 :

for M being MetrStruct holds

( M is triangle iff the distance of M is triangle );

for M being MetrStruct holds

( M is triangle iff the distance of M is triangle );

registration

existence

ex b_{1} being MetrStruct st

( b_{1} is strict & b_{1} is Reflexive & b_{1} is discerning & b_{1} is symmetric & b_{1} is triangle & not b_{1} is empty )

end;
ex b

( b

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

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

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

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 )

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

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

theorem Th5: :: METRIC_1:5

for M being Reflexive symmetric triangle MetrStruct

for a, b being Element of M holds 0 <= dist (a,b)

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

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

definition

let A be set ;

ex b_{1} being Function of [:A,A:],REAL st

for x, y being Element of A holds

( b_{1} . (x,x) = 0 & ( x <> y implies b_{1} . (x,y) = 1 ) )

for b_{1}, b_{2} being Function of [:A,A:],REAL st ( for x, y being Element of A holds

( b_{1} . (x,x) = 0 & ( x <> y implies b_{1} . (x,y) = 1 ) ) ) & ( for x, y being Element of A holds

( b_{2} . (x,x) = 0 & ( x <> y implies b_{2} . (x,y) = 1 ) ) ) holds

b_{1} = b_{2}

end;
func discrete_dist A -> Function of [:A,A:],REAL means :Def10: :: METRIC_1:def 10

for x, y being Element of A holds

( it . (x,x) = 0 & ( x <> y implies it . (x,y) = 1 ) );

existence for x, y being Element of A holds

( it . (x,x) = 0 & ( x <> y implies it . (x,y) = 1 ) );

ex b

for x, y being Element of A holds

( b

proof end;

uniqueness for b

( b

( b

b

proof end;

:: deftheorem Def10 defines discrete_dist METRIC_1:def 10 :

for A being set

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

( b_{2} = discrete_dist A iff for x, y being Element of A holds

( b_{2} . (x,x) = 0 & ( x <> y implies b_{2} . (x,y) = 1 ) ) );

for A being set

for b

( b

( b

definition

let A be set ;

MetrStruct(# A,(discrete_dist A) #) is strict MetrStruct ;

end;
func DiscreteSpace A -> strict MetrStruct equals :: METRIC_1:def 11

MetrStruct(# A,(discrete_dist A) #);

coherence MetrStruct(# A,(discrete_dist A) #);

MetrStruct(# A,(discrete_dist A) #) is strict MetrStruct ;

:: deftheorem defines DiscreteSpace METRIC_1:def 11 :

for A being set holds DiscreteSpace A = MetrStruct(# A,(discrete_dist A) #);

for A being set holds DiscreteSpace A = MetrStruct(# A,(discrete_dist A) #);

registration

let A be set ;

coherence

( DiscreteSpace A is Reflexive & DiscreteSpace A is discerning & DiscreteSpace A is symmetric & DiscreteSpace A is triangle )

end;
coherence

( DiscreteSpace A is Reflexive & DiscreteSpace A is discerning & DiscreteSpace A is symmetric & DiscreteSpace A is triangle )

proof end;

definition

ex b_{1} being Function of [:REAL,REAL:],REAL st

for x, y being Real holds b_{1} . (x,y) = |.(x - y).|

for b_{1}, b_{2} being Function of [:REAL,REAL:],REAL st ( for x, y being Real holds b_{1} . (x,y) = |.(x - y).| ) & ( for x, y being Real holds b_{2} . (x,y) = |.(x - y).| ) holds

b_{1} = b_{2}
end;

func real_dist -> Function of [:REAL,REAL:],REAL means :Def12: :: METRIC_1:def 12

for x, y being Real holds it . (x,y) = |.(x - y).|;

existence for x, y being Real holds it . (x,y) = |.(x - y).|;

ex b

for x, y being Real holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def12 defines real_dist METRIC_1:def 12 :

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

( b_{1} = real_dist iff for x, y being Real holds b_{1} . (x,y) = |.(x - y).| );

for b

( b

theorem Th10: :: METRIC_1:10

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

proof end;

registration

coherence

( RealSpace is Reflexive & RealSpace is discerning & RealSpace is symmetric & RealSpace is triangle )

end;
( RealSpace is Reflexive & RealSpace is discerning & RealSpace is symmetric & RealSpace is triangle )

proof end;

definition

let M be MetrStruct ;

let p be Element of M;

let r be Real;

( ( not M is empty implies ex b_{1} being Subset of M st b_{1} = { q where q is Element of M : dist (p,q) < r } ) & ( M is empty implies ex b_{1} being Subset of M st b_{1} is empty ) )

consistency

for b_{1} being Subset of M holds verum;

uniqueness

for b_{1}, b_{2} being Subset of M holds

( ( not M is empty & b_{1} = { q where q is Element of M : dist (p,q) < r } & b_{2} = { q where q is Element of M : dist (p,q) < r } implies b_{1} = b_{2} ) & ( M is empty & b_{1} is empty & b_{2} is empty implies b_{1} = b_{2} ) );

;

end;
let p be Element of M;

let r be Real;

func Ball (p,r) -> Subset of M means :Def14: :: METRIC_1:def 14

it = { q where q is Element of M : dist (p,q) < r } if not M is empty

otherwise it is empty ;

existence it = { q where q is Element of M : dist (p,q) < r } if not M is empty

otherwise it is empty ;

( ( not M is empty implies ex b

proof end;

correctness consistency

for b

uniqueness

for b

( ( not M is empty & b

;

:: deftheorem Def14 defines Ball METRIC_1:def 14 :

for M being MetrStruct

for p being Element of M

for r being Real

for b_{4} being Subset of M holds

( ( not M is empty implies ( b_{4} = Ball (p,r) iff b_{4} = { q where q is Element of M : dist (p,q) < r } ) ) & ( M is empty implies ( b_{4} = Ball (p,r) iff b_{4} is empty ) ) );

for M being MetrStruct

for p being Element of M

for r being Real

for b

( ( not M is empty implies ( b

definition

let M be MetrStruct ;

let p be Element of M;

let r be Real;

( ( not M is empty implies ex b_{1} being Subset of M st b_{1} = { q where q is Element of M : dist (p,q) <= r } ) & ( M is empty implies ex b_{1} being Subset of M st b_{1} is empty ) )

consistency

for b_{1} being Subset of M holds verum;

uniqueness

for b_{1}, b_{2} being Subset of M holds

( ( not M is empty & b_{1} = { q where q is Element of M : dist (p,q) <= r } & b_{2} = { q where q is Element of M : dist (p,q) <= r } implies b_{1} = b_{2} ) & ( M is empty & b_{1} is empty & b_{2} is empty implies b_{1} = b_{2} ) );

;

end;
let p be Element of M;

let r be Real;

func cl_Ball (p,r) -> Subset of M means :Def15: :: METRIC_1:def 15

it = { q where q is Element of M : dist (p,q) <= r } if not M is empty

otherwise it is empty ;

existence it = { q where q is Element of M : dist (p,q) <= r } if not M is empty

otherwise it is empty ;

( ( not M is empty implies ex b

proof end;

correctness consistency

for b

uniqueness

for b

( ( not M is empty & b

;

:: deftheorem Def15 defines cl_Ball METRIC_1:def 15 :

for M being MetrStruct

for p being Element of M

for r being Real

for b_{4} being Subset of M holds

( ( not M is empty implies ( b_{4} = cl_Ball (p,r) iff b_{4} = { q where q is Element of M : dist (p,q) <= r } ) ) & ( M is empty implies ( b_{4} = cl_Ball (p,r) iff b_{4} is empty ) ) );

for M being MetrStruct

for p being Element of M

for r being Real

for b

( ( not M is empty implies ( b

definition

let M be MetrStruct ;

let p be Element of M;

let r be Real;

( ( not M is empty implies ex b_{1} being Subset of M st b_{1} = { q where q is Element of M : dist (p,q) = r } ) & ( M is empty implies ex b_{1} being Subset of M st b_{1} is empty ) )

consistency

for b_{1} being Subset of M holds verum;

uniqueness

for b_{1}, b_{2} being Subset of M holds

( ( not M is empty & b_{1} = { q where q is Element of M : dist (p,q) = r } & b_{2} = { q where q is Element of M : dist (p,q) = r } implies b_{1} = b_{2} ) & ( M is empty & b_{1} is empty & b_{2} is empty implies b_{1} = b_{2} ) );

;

end;
let p be Element of M;

let r be Real;

func Sphere (p,r) -> Subset of M means :Def16: :: METRIC_1:def 16

it = { q where q is Element of M : dist (p,q) = r } if not M is empty

otherwise it is empty ;

existence it = { q where q is Element of M : dist (p,q) = r } if not M is empty

otherwise it is empty ;

( ( not M is empty implies ex b

proof end;

correctness consistency

for b

uniqueness

for b

( ( not M is empty & b

;

:: deftheorem Def16 defines Sphere METRIC_1:def 16 :

for M being MetrStruct

for p being Element of M

for r being Real

for b_{4} being Subset of M holds

( ( not M is empty implies ( b_{4} = Sphere (p,r) iff b_{4} = { q where q is Element of M : dist (p,q) = r } ) ) & ( M is empty implies ( b_{4} = Sphere (p,r) iff b_{4} is empty ) ) );

for M being MetrStruct

for p being Element of M

for r being Real

for b

( ( not M is empty implies ( b

theorem Th11: :: METRIC_1:11

for r being Real

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

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 Th12: :: METRIC_1:12

for r being Real

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

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 Th13: :: METRIC_1:13

for r being Real

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

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

for M being MetrStruct

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

for M being MetrStruct

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

proof end;

theorem :: METRIC_1:16

for r being Real

for M being MetrStruct

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

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:17

theorem :: METRIC_1:18

theorem :: METRIC_1:19

theorem Th23: :: METRIC_1:23

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

theorem Th24: :: METRIC_1:24

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;

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

attr f is Discerning means :: METRIC_1:def 17

for a, b being Element of A st a <> b holds

0 < f . (a,b);

for a, b being Element of A st a <> b holds

0 < f . (a,b);

:: deftheorem defines Discerning METRIC_1:def 17 :

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

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

:: deftheorem defines Discerning METRIC_1:def 18 :

for M being non empty MetrStruct holds

( M is Discerning iff the distance of M is Discerning );

for M being non empty MetrStruct holds

( M is Discerning iff the distance of M is Discerning );

theorem Th25: :: METRIC_1:25

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 )

( ( for a, b being Element of M st a <> b holds

0 < dist (a,b) ) iff M is Discerning )

proof end;

registration

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 )

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

:: deftheorem Def19 defines ultra METRIC_1:def 19 :

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

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

existence

ex b_{1} being non empty MetrStruct st

( b_{1} is strict & b_{1} is ultra & b_{1} is Reflexive & b_{1} is symmetric & b_{1} is Discerning & b_{1} is triangle )

end;
ex b

( b

proof end;

theorem Th26: :: METRIC_1:26

for M being non empty Reflexive Discerning MetrStruct

for a, b being Element of M holds 0 <= dist (a,b)

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

registration
end;

registration

coherence

for b_{1} being UltraMetricSpace holds

( b_{1} is triangle & b_{1} is discerning )

end;
for b

( b

proof end;

theorem Th29: :: METRIC_1:29

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;

registration
end;

:: deftheorem defines is_between METRIC_1:def 22 :

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

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:30

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

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:31

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 )

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:32

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 )

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;

{ q where q is Element of M : q is_between p,r } is Subset of M

end;
let p, r be Element of M;

func open_dist_Segment (p,r) -> Subset of M equals :: METRIC_1:def 23

{ 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 } ;

{ q where q is Element of M : q is_between p,r } is Subset of M

proof end;

:: deftheorem defines open_dist_Segment METRIC_1:def 23 :

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

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:33

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 )

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;

{ q where q is Element of M : q is_between p,r } \/ {p,r} is Subset of M

end;
let p, r be Element of M;

func close_dist_Segment (p,r) -> Subset of M equals :: METRIC_1:def 24

{ 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};

{ q where q is Element of M : q is_between p,r } \/ {p,r} is Subset of M

proof end;

:: deftheorem defines close_dist_Segment METRIC_1:def 24 :

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

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:34

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

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;

:: let A,B be set, f be PartFunc of [:A,B:],REAL;

:: let a be Element of A;

:: let b be Element of B;

:: cluster f.(a,b) -> real;

:: coherence

:: proof

:: per cases;

:: suppose

:: [a,b] in dom f;

:: hence thesis by PARTFUN1:4;

:: end;

:: suppose

:: not [a,b] in dom f;

:: then f.(a,b) = 0 by FUNCT_1:def 2;

:: hence thesis;

:: end;

:: end;

:: end;