Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### Metric Spaces

by
Stanislawa Kanas,
Mariusz Startek

MML identifier: METRIC_1
[ Mizar article, MML identifier index ]

```environ

vocabulary FUNCT_1, PARTFUN1, RELAT_1, BOOLE, FUNCOP_1, RELAT_2, ARYTM_3,
FUNCT_3, ABSVALUE, ARYTM_1, ARYTM, METRIC_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0,
REAL_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_3, BINOP_1, FUNCOP_1, RELAT_1,
ABSVALUE, STRUCT_0;
constructors REAL_1, FUNCT_3, BINOP_1, FUNCOP_1, ABSVALUE, STRUCT_0, MEMBERED,
XBOOLE_0;
clusters SUBSET_1, STRUCT_0, XREAL_0, FUNCOP_1, RELSET_1, RELAT_1, FUNCT_1,
MEMBERED, ZFMISC_1, XBOOLE_0, ORDINAL2;
requirements BOOLE, REAL, NUMERALS, SUBSET, ARITHM;

begin

definition
struct(1-sorted) MetrStruct
(# carrier -> set,
distance -> Function of [:the carrier,the carrier:],REAL #);
end;

definition
cluster non empty strict MetrStruct;
end;

definition let A,B be set, f be PartFunc of [:A,B:],REAL;
let a be Element of A; let b be Element of B;
redefine func f.(a,b) -> Real;
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);
end;

definition
func Empty^2-to-zero -> Function of [:{{}},{{}}:], REAL equals
:: METRIC_1:def 2
[:{{}},{{}}:] --> 0;
end;

definition let A be set; let f be PartFunc of [:A,A:], REAL;
attr f is Reflexive means
:: METRIC_1:def 3
for a being Element of A holds f.(a,a) = 0;

attr f is discerning means
:: METRIC_1:def 4
for a, b being Element of A holds
f.(a,b) = 0 implies a = b;

attr f is symmetric means
:: METRIC_1:def 5
for a, b being Element of A holds f.(a,b) = f.(b,a);

attr f is triangle means
:: METRIC_1:def 6
for a, b, c being Element of A holds
f.(a,c) <= f.(a,b) + f.(b,c);
end;

definition let M be MetrStruct;
attr M is Reflexive means
:: METRIC_1:def 7
the distance of M is Reflexive;

attr M is discerning means
:: METRIC_1:def 8
the distance of M is discerning;

attr M is symmetric means
:: METRIC_1:def 9
the distance of M is symmetric;

attr M is triangle means
:: METRIC_1:def 10
the distance of M is triangle;
end;

definition
cluster strict Reflexive discerning symmetric triangle non empty MetrStruct;
end;

definition
mode MetrSpace is Reflexive discerning symmetric triangle MetrStruct;
end;

theorem :: METRIC_1:1
for M being MetrStruct holds
( for a being Element of M holds dist(a,a) = 0 ) iff
M is Reflexive;

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;

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

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

definition let M be symmetric MetrStruct;
let a, b be Element of M;
redefine func dist(a,b);
commutativity;
end;

theorem :: METRIC_1:5
for M being symmetric triangle Reflexive MetrStruct,
a, b being Element of M holds
0 <= dist(a,b);

theorem :: METRIC_1:6
for M being MetrStruct st
(for a, b, c being Element of M holds
(dist(a,b) = 0 iff a=b) &
dist(a,b) = dist(b,a) &
dist(a,c) <= dist(a,b) + dist(b,c)) holds
M is MetrSpace;

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

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

definition let A be non empty set;
cluster DiscreteSpace A -> non empty;
end;

definition let A be set;
cluster DiscreteSpace A -> Reflexive discerning symmetric triangle;
end;

definition
func real_dist -> Function of [:REAL,REAL:], REAL means
:: METRIC_1:def 13
for x,y being Element of REAL holds it.(x,y) = abs(x-y);
end;

canceled 2;

theorem :: METRIC_1:9
for x,y being Element of REAL holds real_dist.(x,y) = 0 iff x = y;

theorem :: METRIC_1:10
for x,y being Element of REAL holds real_dist.(x,y) = real_dist.(y,x);

theorem :: METRIC_1:11
for x,y,z being Element of REAL holds
real_dist.(x,y) <= real_dist.(x,z) + real_dist.(z,y);

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

definition
cluster RealSpace -> non empty;
end;

definition
cluster RealSpace -> Reflexive discerning symmetric triangle;
end;

definition let M be MetrStruct, p be Element of M,
r be real number;
func Ball(p,r) -> Subset of M means
:: METRIC_1:def 15
ex M' being non empty MetrStruct, p' being Element of M' st
M' = M & p' = p &
it = {q where q is Element of M' : dist(p',q) < r}
if M is non empty
otherwise it is empty;
end;

definition let M be MetrStruct, p be Element of M,
r be real number;
func cl_Ball(p,r) -> Subset of M means
:: METRIC_1:def 16
ex M' being non empty MetrStruct, p' being Element of M' st
M' = M & p' = p &
it = {q where q is Element of M' : dist(p',q) <= r}
if M is non empty
otherwise it is empty;
end;

definition let M be MetrStruct, p be Element of M,
r be real number;
func Sphere(p,r) -> Subset of M means
:: METRIC_1:def 17
ex M' being non empty MetrStruct, p' being Element of M' st
M' = M & p' = p &
it = {q where q is Element of M' : dist(p',q) = r}
if M is non empty
otherwise it is empty;
end;

reserve r for real number;

theorem :: METRIC_1:12
for M being MetrStruct, p, x being Element of M holds
x in Ball(p,r) iff M is non empty & dist(p,x) < r;

theorem :: METRIC_1:13
for M being MetrStruct, p, x being Element of M holds
x in cl_Ball(p,r) iff M is non empty & dist(p,x) <= r;

theorem :: METRIC_1:14
for M being MetrStruct, p, x being Element of M holds
x in Sphere(p,r) iff M is non empty & dist(p,x) = r;

theorem :: METRIC_1:15
for M being MetrStruct, p being Element of M holds
Ball(p,r) c= cl_Ball(p,r);

theorem :: METRIC_1:16
for M being MetrStruct, p being Element of M holds
Sphere(p,r) c= cl_Ball(p,r);

theorem :: METRIC_1:17
for M being MetrStruct, p being Element of M holds
Sphere(p,r) \/ Ball(p,r) = cl_Ball(p,r);

theorem :: METRIC_1:18
for M being non empty MetrStruct, p being Element of M holds
Ball(p,r) = {q where q is Element of M: dist(p,q) < r};

theorem :: METRIC_1:19
for M being non empty MetrStruct, p being Element of M holds
cl_Ball(p,r) = {q where q is Element of M: dist(p,q) <= r};

theorem :: METRIC_1:20
for M being non empty MetrStruct, p being Element of M holds
Sphere(p,r) = {q where q is Element of M: dist(p,q) = r};
```