### The Mizar article:

### Metric Spaces

**by****Stanislawa Kanas,****Adam Lecko, and****Mariusz Startek**

- Received May 3, 1990
Copyright (c) 1990 Association of Mizar Users

- MML identifier: METRIC_1
- [ 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; definitions STRUCT_0, XBOOLE_0; theorems TARSKI, REAL_1, AXIOMS, BINOP_1, FUNCOP_1, ZFMISC_1, FUNCT_2, RELSET_1, RELAT_1, FUNCT_3, ABSVALUE, SUBSET_1, STRUCT_0, PARTFUN1, CARD_1, FUNCT_1, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1; schemes FUNCT_2, FRAENKEL; begin definition struct(1-sorted) MetrStruct (# carrier -> set, distance -> Function of [:the carrier,the carrier:],REAL #); end; definition cluster non empty strict MetrStruct; existence proof consider A being non empty set, r being Function of [:A,A:],REAL; take MetrStruct(#A,r#); thus the carrier of MetrStruct(#A,r#) is non empty; thus thesis; end; 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; coherence proof A1: f.(a,b) = f.[a,b] by BINOP_1:def 1; per cases; suppose [a,b] in dom f; hence thesis by A1,PARTFUN1:27; suppose not [a,b] in dom f; hence thesis by A1,CARD_1:51,FUNCT_1:def 4; end; end; definition let M be MetrStruct; let a, b be Element of M; func dist(a,b) -> Real equals :Def1: (the distance of M).(a,b); coherence; end; definition func Empty^2-to-zero -> Function of [:{{}},{{}}:], REAL equals :Def2: [:{{}},{{}}:] --> 0; coherence proof set X=[:{{}},{{}}:]; {0} c= REAL & X<>{} by ZFMISC_1:37; then X=dom (X-->0) & rng (X-->0) c= REAL by FUNCOP_1:14,19; hence thesis by FUNCT_2:def 1,RELSET_1:11; end; end; Lm1:[{},{}] in [:{{}},{{}}:] by ZFMISC_1:34; Lm2: Empty^2-to-zero.({},{}) = Empty^2-to-zero.[{},{}] by BINOP_1:def 1 .= 0 by Def2,Lm1,FUNCOP_1:13; Lm3: for x,y be Element of {{}} holds Empty^2-to-zero.(x,y)=0 iff x=y proof let x,y be Element of {{}}; x={} & y={} by TARSKI:def 1; hence thesis by Lm2; end; Lm4: for x,y be Element of {{}} holds Empty^2-to-zero.(x,y)=Empty^2-to-zero.(y,x) proof let x,y be Element of {{}}; x={} & y={} by TARSKI:def 1; hence thesis; end; Lm5: for x,y,z be Element of {{}} holds Empty^2-to-zero.(x,z) <= Empty^2-to-zero.(x,y) + Empty^2-to-zero.(y,z) proof let x,y,z be Element of {{}}; x={} & y={} & z={} by TARSKI:def 1; hence thesis by Lm2; end; definition let A be set; let f be PartFunc of [:A,A:], REAL; attr f is Reflexive means :Def3: for a being Element of A holds f.(a,a) = 0; attr f is discerning means :Def4: for a, b being Element of A holds f.(a,b) = 0 implies a = b; attr f is symmetric means :Def5: for a, b being Element of A holds f.(a,b) = f.(b,a); attr f is triangle means :Def6: 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 :Def7: the distance of M is Reflexive; attr M is discerning means :Def8: the distance of M is discerning; attr M is symmetric means :Def9: the distance of M is symmetric; attr M is triangle means :Def10: the distance of M is triangle; end; definition cluster strict Reflexive discerning symmetric triangle non empty MetrStruct; existence proof reconsider M = MetrStruct(#{{}},Empty^2-to-zero#) as strict non empty MetrStruct by STRUCT_0:def 1; take M; M is Reflexive discerning symmetric triangle proof thus the distance of M is Reflexive proof let a be Element of M; thus thesis by Lm3; end; thus the distance of M is discerning proof let a, b be Element of M; assume (the distance of M).(a,b) = 0; hence thesis by Lm3; end; thus the distance of M is symmetric proof let a, b be Element of M; thus thesis by Lm4; end; thus the distance of M is triangle proof let a, b, c be Element of M; thus thesis by Lm5; end; end; hence thesis; end; end; definition mode MetrSpace is Reflexive discerning symmetric triangle MetrStruct; end; theorem Th1: for M being MetrStruct holds ( for a being Element of M holds dist(a,a) = 0 ) iff M is Reflexive proof let M be MetrStruct; hereby assume A1: for a being Element of M holds dist(a,a) = 0; the distance of M is Reflexive proof let a be Element of M; (the distance of M).(a,a) = dist(a,a) by Def1 .= 0 by A1; hence thesis; end; hence M is Reflexive by Def7; end; assume M is Reflexive; then A2: the distance of M is Reflexive by Def7; now let a be Element of M; thus dist(a,a) = (the distance of M).(a,a) by Def1 .= 0 by A2,Def3; end; hence thesis; end; theorem 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 let M be MetrStruct; hereby assume A1: for a, b being Element of M st dist(a,b) = 0 holds a = b; the distance of M is discerning proof let a, b be Element of M; assume (the distance of M).(a,b) = 0; then dist(a,b) = 0 by Def1; hence thesis by A1; end; hence M is discerning by Def8; end; assume M is discerning; then A2: the distance of M is discerning by Def8; now let a, b be Element of M; assume dist(a,b) = 0; then (the distance of M).(a,b) = 0 by Def1; hence a = b by A2,Def4; end; hence thesis; end; theorem Th3: for M being MetrStruct holds ( for a, b being Element of M holds dist(a,b) = dist(b,a) ) iff M is symmetric proof let M be MetrStruct; hereby assume A1: for a, b being Element of M holds dist(a,b) = dist(b,a); the distance of M is symmetric proof let a, b be Element of M; thus (the distance of M).(a,b) = dist(a,b) by Def1 .= dist(b,a) by A1 .= (the distance of M).(b,a) by Def1; end; hence M is symmetric by Def9; end; assume M is symmetric; then A2: the distance of M is symmetric by Def9; now let a, b be Element of M; thus dist(a,b) = (the distance of M).(a,b) by Def1 .= (the distance of M).(b,a) by A2,Def5 .= dist(b,a) by Def1; end; hence thesis; end; theorem Th4: 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 let M be MetrStruct; hereby assume A1: for a, b, c being Element of M holds dist(a,c) <= dist(a,b) + dist(b,c); the distance of M is triangle proof let a, b, c be Element of M; A2: (the distance of M).(a,b) = dist(a,b) by Def1; A3: (the distance of M).(a,c) = dist(a,c) by Def1; (the distance of M).(b,c) = dist(b,c) by Def1; hence (the distance of M).(a,c) <= (the distance of M).(a,b) + (the distance of M).(b,c) by A1,A2,A3; end; hence M is triangle by Def10; end; assume M is triangle; then A4: the distance of M is triangle by Def10; let a, b, c be Element of M; A5: dist(a,b) = (the distance of M).(a,b) by Def1; A6: dist(a,c) = (the distance of M).(a,c) by Def1; dist(b,c) = (the distance of M).(b,c) by Def1; hence dist(a,c) <= dist(a,b) + dist(b,c) by A4,A5,A6,Def6; end; definition let M be symmetric MetrStruct; let a, b be Element of M; redefine func dist(a,b); commutativity by Th3; end; theorem for M being symmetric triangle Reflexive MetrStruct, a, b being Element of M holds 0 <= dist(a,b) proof let M be symmetric triangle Reflexive MetrStruct, a, b be Element of M; A1:dist(a,a)<=dist(a,b)+dist(b,a) by Th4; A2: dist(a,b) =(1/2)*2*dist(a,b) .=(1/2)*((1+1)*dist(a,b)) by XCMPLX_1:4 .=(1/2)*(1*dist(a,b)+1*dist(a,b)) by XCMPLX_1:8; (1/2)*dist(a,a)=(1/2)*0 by Th1; hence thesis by A1,A2,AXIOMS:25; end; theorem Th6: 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 proof let M be MetrStruct; assume A1: 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); M is Reflexive discerning symmetric triangle proof thus the distance of M is Reflexive proof let a be Element of M; (the distance of M).(a,a) = dist(a,a) by Def1 .= 0 by A1; hence thesis; end; thus the distance of M is discerning proof let a, b be Element of M; assume (the distance of M).(a,b) = 0; then dist(a,b) = 0 by Def1; hence thesis by A1; end; thus the distance of M is symmetric proof let a, b be Element of M; (the distance of M).(a,b) = dist(a,b) by Def1 .= dist(b,a) by A1 .= (the distance of M).(b,a) by Def1; hence thesis; end; thus the distance of M is triangle proof let a, b, c be Element of M; A2: (the distance of M).(a,c) = dist(a,c) by Def1; A3: (the distance of M).(a,b) = dist(a,b) by Def1; (the distance of M).(b,c) = dist(b,c) by Def1; hence thesis by A1,A2,A3; end; end; hence thesis; end; definition let A be set; func discrete_dist A -> Function of [:A,A:], REAL means :Def11: for x,y being Element of A holds it.(x,x) = 0 & (x <> y implies it.(x,y) = 1); existence proof per cases; suppose A1: A is empty; then [:A,A:] = {} by ZFMISC_1:113; then reconsider f = {} as Function of [:A,A:], REAL by FUNCT_2:55, RELAT_1:60; take f; let x, y be Element of A; A2: dom {} = {}; thus f.(x,x) = f.[x,x] by BINOP_1:def 1 .= 0 by A2,FUNCT_1:def 4; x = {} by A1,SUBSET_1:def 2 .= y by A1,SUBSET_1:def 2; hence thesis; suppose A3: A is non empty; A4:{0,1} c= REAL by ZFMISC_1:38; rng chi([:A,A:]\id A,[:A,A:]) c= {0,1} by FUNCT_3:48; then A5:rng chi([:A,A:]\id A,[:A,A:]) c= REAL by A4,XBOOLE_1:1; dom chi([:A,A:]\id A,[:A,A:]) = [:A,A:] by FUNCT_3:def 3; then reconsider char=chi([:A,A:]\id A,[:A,A:]) as Function of [:A,A:],REAL by A5,FUNCT_2:def 1,RELSET_1:11; take char; let x,y be Element of A; A6:id A c= [:A,A:] by RELSET_1:28; A7: [x,y] in [:A,A:] by A3,ZFMISC_1:def 2; [:A,A:]\([:A,A:]\id A)=[:A,A:]/\id A by XBOOLE_1:48 .=id A by A6,XBOOLE_1:28; then A8:[x,x] in [:A,A:]\([:A,A:]\id A) by A3,RELAT_1:def 10; thus char.(x,x)=char.[x,x] by BINOP_1:def 1 .=0 by A8,FUNCT_3:43; assume x<>y; then not [x,y] in id A by RELAT_1:def 10; then A9:[x,y] in [:A,A:]\id A by A7,XBOOLE_0:def 4; thus char.(x,y)=char.[x,y] by BINOP_1:def 1 .=1 by A7,A9,FUNCT_3:def 3; end; uniqueness proof let f,f' be Function of [:A,A:],REAL; assume that A10: for x,y being Element of A holds f.(x,x)=0 & (x<>y implies f.(x,y)=1) and A11: for x,y being Element of A holds f'.(x,x)=0 & (x<>y implies f'.(x,y)=1); per cases; suppose A is empty; then A12: [:A,A:] = {} by ZFMISC_1:113; hence f = {} by PARTFUN1:57 .= f' by A12,PARTFUN1:57; suppose A13: A is non empty; now let x,y be Element of A; now per cases; suppose A14:x=y; thus f.[x,y]=f.(x,y) by BINOP_1:def 1 .=0 by A10,A14 .=f'.(x,y) by A11,A14 .=f'.[x,y] by BINOP_1:def 1; suppose A15:x<>y; thus f.[x,y]=f.(x,y) by BINOP_1:def 1 .=1 by A10,A15 .=f'.(x,y) by A11,A15 .=f'.[x,y] by BINOP_1:def 1; end; hence f.[x,y]=f'.[x,y]; end; hence f=f' by A13,FUNCT_2:120; end; end; definition let A be set; func DiscreteSpace A -> strict MetrStruct equals :Def12: MetrStruct (#A,discrete_dist A#); coherence; end; definition let A be non empty set; cluster DiscreteSpace A -> non empty; coherence proof MetrStruct (#A,discrete_dist A#) is non empty by STRUCT_0:def 1; hence thesis by Def12; end; end; definition let A be set; cluster DiscreteSpace A -> Reflexive discerning symmetric triangle; coherence proof set M = MetrStruct (#A,discrete_dist A#); M is Reflexive discerning symmetric triangle proof thus the distance of M is Reflexive proof let a be Element of M; thus thesis by Def11; end; thus the distance of M is discerning proof let a, b be Element of M; assume (the distance of M).(a,b) = 0; hence thesis by Def11; end; thus the distance of M is symmetric proof let a, b be Element of M; now per cases; suppose A1: a <> b; hence (the distance of M).(a,b) = 1 by Def11 .= (the distance of M).(b,a) by A1,Def11; suppose a = b; hence (the distance of M).(a,b) = (the distance of M).(b,a); end; hence thesis; end; thus the distance of M is triangle proof let a, b, c be Element of M; A2:(the distance of M).(a,b) = 0 iff a=b by Def11; per cases; suppose a=b & a=c; hence (the distance of M).(a,c)<=(the distance of M).(a,b)+ (the distance of M).(b,c) by A2; suppose a=b & a<>c; hence (the distance of M).(a,c)<=(the distance of M).(a,b) +(the distance of M).(b,c) by A2; suppose A3:a=c & a<>b; then A4:(the distance of M).(a,c)=0 by Def11; A5:(the distance of M).(a,b)=1 by A3,Def11; (the distance of M).(b,c)=1 by A3,Def11; hence (the distance of M).(a,c)<=(the distance of M).(a,b)+ (the distance of M).(b,c) by A4,A5; suppose A6:b=c & a<>c; then (the distance of M).(b,c)=0 by Def11; hence (the distance of M).(a,c)<=(the distance of M).(a,b)+ (the distance of M).(b,c) by A6; suppose a<>b & a<>c & b<>c; then (the distance of M).(a,c)=1 & (the distance of M).(a,b)=1 & (the distance of M).(b,c)=1 by Def11; hence (the distance of M).(a,c)<=(the distance of M).(a,b)+ (the distance of M).(b,c); thus thesis; end; thus thesis; end; hence thesis by Def12; end; end; definition func real_dist -> Function of [:REAL,REAL:], REAL means :Def13: for x,y being Element of REAL holds it.(x,y) = abs(x-y); existence proof deffunc G(Element of REAL,Element of REAL)= abs($1-$2); consider F being Function of [:REAL,REAL:],REAL such that A1: for x,y being Element of REAL holds F.[x,y] = G(x,y) from Lambda2D; take F; let x,y be Element of REAL; thus F.(x,y)=F.[x,y] by BINOP_1:def 1 .=abs(x-y) by A1; end; uniqueness proof let F1,F2 be Function of [:REAL,REAL:],REAL; assume that A2:for x,y being Element of REAL holds F1.(x,y) = abs(x-y) and A3:for x,y being Element of REAL holds F2.(x,y) = abs(x-y); for x,y being Element of REAL holds F1.(x,y)=F2.(x,y) proof let x,y be Element of REAL; thus F1.(x,y)=abs(x-y) by A2 .=F2.(x,y) by A3; end; hence thesis by BINOP_1:2; end; end; canceled 2; theorem Th9: for x,y being Element of REAL holds real_dist.(x,y) = 0 iff x = y proof let x,y be Element of REAL; thus real_dist.(x,y)=0 implies x=y proof assume real_dist.(x,y)=0; then 0=abs(x-y) by Def13; then x-y = 0 by ABSVALUE:7; hence thesis by XCMPLX_1:15; end; assume x=y; then x-y=0 by XCMPLX_1:14; then abs(x-y)=0 by ABSVALUE:7; hence thesis by Def13; end; theorem Th10: for x,y being Element of REAL holds real_dist.(x,y) = real_dist.(y,x) proof let x,y be Element of REAL; thus real_dist.(x,y)=abs(x-y) by Def13 .=abs(-(x-y)) by ABSVALUE:17 .=abs(y-x) by XCMPLX_1:143 .=real_dist.(y,x) by Def13; end; theorem Th11: for x,y,z being Element of REAL holds real_dist.(x,y) <= real_dist.(x,z) + real_dist.(z,y) proof let x,y,z be Element of REAL; A1:abs(x-y)<=abs(x-z)+abs(z-y) proof abs(x-y)=abs((x+0)-y) .=abs((x+(z-z))-y) by XCMPLX_1:14 .=abs((x+-(z-z))-y) by XCMPLX_1:143 .=abs((x-(z-z))-y) by XCMPLX_0:def 8 .=abs((x-z+z)-y) by XCMPLX_1:37 .=abs((x+-z+z)-y) by XCMPLX_0:def 8 .=abs(((x+-z)+z)+-y) by XCMPLX_0:def 8 .=abs((x+-z)+(z+-y)) by XCMPLX_1:1 .=abs((x+-z)+(z-y)) by XCMPLX_0:def 8 .=abs((x-z)+(z-y)) by XCMPLX_0:def 8; hence thesis by ABSVALUE:13; end; real_dist.(x,y)=abs(x-y) & real_dist.(x,z)=abs(x-z) & real_dist.(z,y)=abs(z-y) by Def13; hence thesis by A1; end; definition func RealSpace -> strict MetrStruct equals :Def14: MetrStruct (# REAL, real_dist #); coherence; end; definition cluster RealSpace -> non empty; coherence by Def14,STRUCT_0:def 1; end; definition cluster RealSpace -> Reflexive discerning symmetric triangle; coherence proof reconsider M = MetrStruct(#REAL,real_dist#) as non empty MetrStruct by STRUCT_0:def 1; M is MetrSpace proof now let a,b,c be Element of M; reconsider a'=a,b'=b,c'=c as Element of REAL; A1:dist(a,b)=real_dist.(a',b') by Def1; A2:dist(b,a)=real_dist.(b',a') by Def1; A3:dist(a,c)=real_dist.(a',c') by Def1; A4:dist(b,c)=real_dist.(b',c') by Def1; thus dist(a,b)=0 iff a=b by A1,Th9; thus dist(a,b)=dist(b,a) by A1,A2,Th10; thus dist(a,c)<=dist(a,b)+dist(b,c) by A1,A3,A4,Th11; end; hence thesis by Th6; end; hence thesis by Def14; end; end; definition let M be MetrStruct, p be Element of M, r be real number; func Ball(p,r) -> Subset of M means :Def15: 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; existence proof thus M is non empty implies ex X being Subset of M st ex M' being non empty MetrStruct, p' being Element of M' st M' = M & p' = p & X = {q where q is Element of M' : dist(p',q) < r} proof assume M is non empty; then reconsider M' = M as non empty MetrStruct; reconsider p' = p as Element of M'; defpred P[Element of M'] means dist(p',$1)<r; set X = {q where q is Element of M': P[q]}; X c= the carrier of M' from Fr_Set0; then reconsider X as Subset of M; take X, M', p'; thus thesis; end; assume M is empty; {} c= the carrier of M by XBOOLE_1:2; then reconsider X = {} as Subset of M; take X; thus thesis; end; correctness; end; definition let M be MetrStruct, p be Element of M, r be real number; func cl_Ball(p,r) -> Subset of M means :Def16: 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; existence proof thus M is non empty implies ex X being Subset of M st ex M' being non empty MetrStruct, p' being Element of M' st M' = M & p' = p & X = {q where q is Element of M' : dist(p',q) <= r} proof assume M is non empty; then reconsider M' = M as non empty MetrStruct; reconsider p' = p as Element of M'; defpred P[Element of M'] means dist(p',$1)<=r; set X = {q where q is Element of M': P[q]}; X c= the carrier of M' from Fr_Set0; then reconsider X as Subset of M; take X, M', p'; thus thesis; end; assume M is empty; {} c= the carrier of M by XBOOLE_1:2; then reconsider X = {} as Subset of M; take X; thus thesis; end; correctness; end; definition let M be MetrStruct, p be Element of M, r be real number; func Sphere(p,r) -> Subset of M means :Def17: 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; existence proof thus M is non empty implies ex X being Subset of M st ex M' being non empty MetrStruct, p' being Element of M' st M' = M & p' = p & X = {q where q is Element of M' : dist(p',q) = r} proof assume M is non empty; then reconsider M' = M as non empty MetrStruct; reconsider p' = p as Element of M'; defpred P[Element of M'] means dist(p',$1)=r; set X = {q where q is Element of M': P[q]}; X c= the carrier of M' from Fr_Set0; then reconsider X as Subset of M; take X, M', p'; thus thesis; end; assume M is empty; {} c= the carrier of M by XBOOLE_1:2; then reconsider X = {} as Subset of M; take X; thus thesis; end; correctness; end; reserve r for real number; Lm6: 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} proof let M be non empty MetrStruct, p be Element of M; ex M' being non empty MetrStruct, p' being Element of M' st M' = M & p' = p & Ball(p,r) = {q where q is Element of M' : dist(p',q) < r} by Def15; hence thesis; end; Lm7: 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} proof let M be non empty MetrStruct, p be Element of M; ex M' being non empty MetrStruct, p' being Element of M' st M' = M & p' = p & cl_Ball(p,r) = {q where q is Element of M' : dist(p',q) <= r} by Def16; hence thesis; end; Lm8: 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} proof let M be non empty MetrStruct, p be Element of M; ex M' being non empty MetrStruct, p' being Element of M' st M' = M & p' = p & Sphere(p,r) = {q where q is Element of M' : dist(p',q) = r} by Def17; hence thesis; end; theorem Th12: 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 proof let M be MetrStruct,p,x be Element of M; hereby assume A1: x in Ball(p,r); A2: M is non empty proof thus the carrier of M is non empty by A1; end; then reconsider M' = M as non empty MetrStruct; reconsider p' = p as Element of M'; x in {q where q is Element of M':dist(p',q)<r} by A1,Lm6; then ex q be Element of M st x=q & dist(p,q)<r; hence M is non empty & dist(p,x)<r by A2; end; assume M is non empty; then reconsider M' = M as non empty MetrStruct; reconsider p' = p as Element of M'; assume dist(p,x)<r; then x in {q where q is Element of M':dist(p',q)<r}; hence x in Ball(p,r) by Lm6; end; theorem Th13: 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 proof let M be MetrStruct,p,x be Element of M; hereby assume A1: x in cl_Ball(p,r); A2: M is non empty proof thus the carrier of M is non empty by A1; end; then reconsider M' = M as non empty MetrStruct; reconsider p' = p as Element of M'; x in {q where q is Element of M':dist(p',q)<=r} by A1,Lm7; then ex q be Element of M st x=q & dist(p,q)<=r; hence M is non empty & dist(p,x)<=r by A2; end; assume M is non empty; then reconsider M' = M as non empty MetrStruct; reconsider p' = p as Element of M'; assume dist(p,x)<=r; then x in {q where q is Element of M':dist(p',q)<=r}; hence x in cl_Ball(p,r) by Lm7; end; theorem Th14: 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 proof let M be MetrStruct,p,x be Element of M; hereby assume A1: x in Sphere(p,r); A2: M is non empty proof thus the carrier of M is non empty by A1; end; then reconsider M' = M as non empty MetrStruct; reconsider p' = p as Element of M'; x in {q where q is Element of M':dist(p',q)=r} by A1,Lm8; then ex q be Element of M st x=q & dist(p,q)=r; hence M is non empty & dist(p,x)=r by A2; end; assume M is non empty; then reconsider M' = M as non empty MetrStruct; reconsider p' = p as Element of M'; assume dist(p,x)=r; then x in {q where q is Element of M':dist(p',q)=r}; hence x in Sphere(p,r) by Lm8; end; theorem Th15: for M being MetrStruct, p being Element of M holds Ball(p,r) c= cl_Ball(p,r) proof let M be MetrStruct,p be Element of M; per cases; suppose M is non empty; then consider M' being non empty MetrStruct, p' being Element of M' such that A1: M' = M & p' = p and Ball(p,r) = {q where q is Element of M' : dist(p',q) < r} by Def15; now let x be Element of M'; assume x in Ball(p',r); then dist(p',x)<=r by Th12; then x in {q where q is Element of M':dist(p',q)<=r}; hence x in cl_Ball(p',r) by Lm7; end; hence thesis by A1,SUBSET_1:7; suppose M is empty; then Ball(p,r) is empty & cl_Ball(p,r) is empty by Def15,Def16; hence thesis; end; theorem Th16: for M being MetrStruct, p being Element of M holds Sphere(p,r) c= cl_Ball(p,r) proof let M be MetrStruct,p be Element of M; per cases; suppose M is non empty; then consider M' being non empty MetrStruct, p' being Element of M' such that A1: M' = M & p' = p and Sphere(p,r) = {q where q is Element of M' : dist(p',q) = r} by Def17; now let x be Element of M'; assume x in Sphere(p',r); then dist(p',x)=r by Th14; then x in {q where q is Element of M':dist(p',q)<=r}; hence x in cl_Ball(p',r) by Lm7; end; hence thesis by A1,SUBSET_1:7; suppose M is empty; then Sphere(p,r) is empty & cl_Ball(p,r) is empty by Def16,Def17; hence thesis; end; theorem for M being MetrStruct, p being Element of M holds Sphere(p,r) \/ Ball(p,r) = cl_Ball(p,r) proof let M be MetrStruct,p be Element of M; Sphere(p,r) c= cl_Ball(p,r) & Ball(p,r) c= cl_Ball(p,r) by Th15,Th16; hence Sphere(p,r) \/ Ball(p,r) c= cl_Ball(p,r) by XBOOLE_1:8; per cases; suppose M is non empty; then consider M' being non empty MetrStruct, p' being Element of M' such that A1: M' = M & p' = p and Sphere(p,r) = {q where q is Element of M' : dist(p',q) = r} by Def17; now let x be Element of M'; assume x in cl_Ball(p',r); then A2:dist(p',x)<=r by Th13; now per cases by A2,REAL_1:def 5; case dist(p',x)<r; hence x in Ball(p',r) by Th12; case dist(p',x)=r; hence x in Sphere(p',r) by Th14; end; hence x in Sphere(p',r) \/ Ball(p',r) by XBOOLE_0:def 2; end; hence thesis by A1,SUBSET_1:7; suppose M is empty; then Ball(p,r) is empty & cl_Ball(p,r) is empty & Sphere(p,r) is empty by Def15,Def16,Def17; hence thesis; end; theorem 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} by Lm6; theorem 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} by Lm7; theorem 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} by Lm8;

Back to top