Volume 2, 1990

University of Bialystok

Copyright (c) 1990 Association of Mizar Users

### The abstract of the Mizar article:

### Metric Spaces

**by****Stanislawa Kanas,****Adam Lecko, and****Mariusz Startek**- Received May 3, 1990
- 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};

Back to top