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



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

registration
cluster non empty strict MetrStruct ;
existence
ex b1 being MetrStruct st
( not b1 is empty & b1 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 b1 being Function st b1 = op2 holds
b1 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 b1 being MetrStruct st
( b1 is strict & b1 is Reflexive & b1 is discerning & b1 is symmetric & b1 is triangle & not b1 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 :: 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 holds
( ( for a, b being Element of M holds dist a,b = dist b,a ) iff 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 by Th3;
end;

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

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 b1 being Function of [:A,A:],REAL st
for x, y being Element of A holds
( b1 . x,x = 0 & ( x <> y implies b1 . x,y = 1 ) )
proof end;
uniqueness
for b1, b2 being Function of [:A,A:],REAL st ( for x, y being Element of A holds
( b1 . x,x = 0 & ( x <> y implies b1 . x,y = 1 ) ) ) & ( for x, y being Element of A holds
( b2 . x,x = 0 & ( x <> y implies b2 . x,y = 1 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines discrete_dist METRIC_1:def 11 :
for A being set
for b2 being Function of [:A,A:],REAL holds
( b2 = discrete_dist A iff for x, y being Element of A holds
( b2 . x,x = 0 & ( x <> y implies b2 . 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 b1 being Function of [:REAL ,REAL :],REAL st
for x, y being Element of REAL holds b1 . x,y = abs (x - y)
proof end;
uniqueness
for b1, b2 being Function of [:REAL ,REAL :],REAL st ( for x, y being Element of REAL holds b1 . x,y = abs (x - y) ) & ( for x, y being Element of REAL holds b2 . x,y = abs (x - y) ) holds
b1 = b2
proof end;
end;

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

theorem :: METRIC_1:7
canceled;

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 M' being non empty MetrStruct ex p' being Element of M' st
( M' = M & p' = p & it = { q where q is Element of M' : dist p',q < r } ) if not M is empty
otherwise it is empty ;
existence
( ( not M is empty implies ex b1 being Subset of M ex M' being non empty MetrStruct ex p' being Element of M' st
( M' = M & p' = p & b1 = { q where q is Element of M' : dist p',q < r } ) ) & ( M is empty implies ex b1 being Subset of M st b1 is empty ) )
proof end;
correctness
consistency
for b1 being Subset of M holds verum;
uniqueness
for b1, b2 being Subset of M holds
( ( not M is empty & ex M' being non empty MetrStruct ex p' being Element of M' st
( M' = M & p' = p & b1 = { q where q is Element of M' : dist p',q < r } ) & ex M' being non empty MetrStruct ex p' being Element of M' st
( M' = M & p' = p & b2 = { q where q is Element of M' : dist p',q < r } ) implies b1 = b2 ) & ( M is empty & b1 is empty & b2 is empty implies b1 = b2 ) );
;
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 b4 being Subset of M holds
( ( not M is empty implies ( b4 = Ball p,r iff ex M' being non empty MetrStruct ex p' being Element of M' st
( M' = M & p' = p & b4 = { q where q is Element of M' : dist p',q < r } ) ) ) & ( M is empty implies ( b4 = Ball p,r iff b4 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 M' being non empty MetrStruct ex p' being Element of M' st
( M' = M & p' = p & it = { q where q is Element of M' : dist p',q <= r } ) if not M is empty
otherwise it is empty ;
existence
( ( not M is empty implies ex b1 being Subset of M ex M' being non empty MetrStruct ex p' being Element of M' st
( M' = M & p' = p & b1 = { q where q is Element of M' : dist p',q <= r } ) ) & ( M is empty implies ex b1 being Subset of M st b1 is empty ) )
proof end;
correctness
consistency
for b1 being Subset of M holds verum;
uniqueness
for b1, b2 being Subset of M holds
( ( not M is empty & ex M' being non empty MetrStruct ex p' being Element of M' st
( M' = M & p' = p & b1 = { q where q is Element of M' : dist p',q <= r } ) & ex M' being non empty MetrStruct ex p' being Element of M' st
( M' = M & p' = p & b2 = { q where q is Element of M' : dist p',q <= r } ) implies b1 = b2 ) & ( M is empty & b1 is empty & b2 is empty implies b1 = b2 ) );
;
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 b4 being Subset of M holds
( ( not M is empty implies ( b4 = cl_Ball p,r iff ex M' being non empty MetrStruct ex p' being Element of M' st
( M' = M & p' = p & b4 = { q where q is Element of M' : dist p',q <= r } ) ) ) & ( M is empty implies ( b4 = cl_Ball p,r iff b4 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 M' being non empty MetrStruct ex p' being Element of M' st
( M' = M & p' = p & it = { q where q is Element of M' : dist p',q = r } ) if not M is empty
otherwise it is empty ;
existence
( ( not M is empty implies ex b1 being Subset of M ex M' being non empty MetrStruct ex p' being Element of M' st
( M' = M & p' = p & b1 = { q where q is Element of M' : dist p',q = r } ) ) & ( M is empty implies ex b1 being Subset of M st b1 is empty ) )
proof end;
correctness
consistency
for b1 being Subset of M holds verum;
uniqueness
for b1, b2 being Subset of M holds
( ( not M is empty & ex M' being non empty MetrStruct ex p' being Element of M' st
( M' = M & p' = p & b1 = { q where q is Element of M' : dist p',q = r } ) & ex M' being non empty MetrStruct ex p' being Element of M' st
( M' = M & p' = p & b2 = { q where q is Element of M' : dist p',q = r } ) implies b1 = b2 ) & ( M is empty & b1 is empty & b2 is empty implies b1 = b2 ) );
;
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 b4 being Subset of M holds
( ( not M is empty implies ( b4 = Sphere p,r iff ex M' being non empty MetrStruct ex p' being Element of M' st
( M' = M & p' = p & b4 = { q where q is Element of M' : dist p',q = r } ) ) ) & ( M is empty implies ( b4 = Sphere p,r iff b4 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;