:: Metric Spaces
:: by Stanis{\l}awa Kanas, Adam Lecko and Mariusz Startek
::
:: Received May 3, 1990
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, STRUCT_0, FUNCT_1, ZFMISC_1, XBOOLE_0, PARTFUN1,
SUBSET_1, REAL_1, RELAT_1, CARD_1, FUNCT_5, TARSKI, VALUED_0, ORDINAL1,
XXREAL_0, ARYTM_3, RELAT_2, FUNCT_3, COMPLEX1, ARYTM_1, METRIC_1,
FUNCOP_1, FUNCT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
XXREAL_0, XREAL_0, COMPLEX1, REAL_1, RELAT_1, FUNCOP_1, FUNCT_1,
RELSET_1, PARTFUN1, FUNCT_2, FUNCT_3, BINOP_1, FUNCT_5, VALUED_0,
STRUCT_0;
constructors BINOP_1, FUNCT_3, XXREAL_0, REAL_1, COMPLEX1, STRUCT_0, VALUED_1,
FUNCT_5, PARTFUN1, RELSET_1, FUNCOP_1, NUMBERS;
registrations XBOOLE_0, RELAT_1, FUNCT_1, NUMBERS, XREAL_0, MEMBERED,
STRUCT_0, VALUED_0, FUNCT_2, PARTFUN1, RELSET_1, ORDINAL1, BINOP_2;
requirements BOOLE, REAL, NUMERALS, SUBSET, ARITHM;
definitions STRUCT_0, XBOOLE_0;
equalities BINOP_1, FUNCT_5, ORDINAL1;
expansions XBOOLE_0, BINOP_1;
theorems TARSKI, ZFMISC_1, FUNCT_2, RELSET_1, RELAT_1, FUNCT_3, ABSVALUE,
SUBSET_1, CARD_1, FUNCT_1, XBOOLE_0, XBOOLE_1, XREAL_1, COMPLEX1,
XXREAL_0, SQUARE_1, FUNCOP_1, XREAL_0;
schemes FRAENKEL, BINOP_1;
begin
definition
struct(1-sorted) MetrStruct
(# carrier -> set,
distance -> Function of [:the carrier,the carrier:],REAL #);
end;
registration
cluster non empty strict for MetrStruct;
existence
proof
set A = the non empty set,r = the Function of [:A,A:],REAL;
take MetrStruct(#A,r#);
thus the carrier of MetrStruct(#A,r#) is non empty;
thus thesis;
end;
end;
:: registration
:: 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;
definition
let M be MetrStruct;
let a, b be Element of M;
func dist(a,b) -> Real equals
(the distance of M).(a,b);
coherence;
end;
notation
synonym Empty^2-to-zero for op2;
end;
Lm1: 0 in REAL by XREAL_0:def 1;
definition
redefine func Empty^2-to-zero -> Function of [:1,1:], REAL; :: redefines Empty^2-to-zero (METRIC_1, synonym) → op2 (FUNCT_5, definition)
coherence
proof
op2 is Function of [:1,1:], 1 & 1 c= REAL by CARD_1:49,ZFMISC_1:31,Lm1;
hence thesis by FUNCT_2:7;
end;
end;
Lm2: op2.(0,0) = 0
proof
[0,0] in [:{0},{0}:] by ZFMISC_1:28;
hence thesis by FUNCT_2:50;
end;
Lm3: for x,y be Element of 1 holds op2.(x,y)=0 iff x=y
proof
let x,y be Element of 1;
A1: x={} & y = {} by CARD_1:49,TARSKI:def 1;
hence op2.(x,y)=0 implies x=y;
thus thesis by A1,Lm2;
end;
Lm4: for x,y be Element of 1 holds op2.(x,y)=op2.(y,x)
proof
let x,y be Element of 1;
x={} & y={} by CARD_1:49,TARSKI:def 1;
hence thesis;
end;
registration
cluster op2 -> natural-valued for Function;
coherence;
end;
registration
let f be natural-valued Function;
let x,y be object;
cluster f.(x,y) -> natural;
coherence;
end;
Lm5: for x,y,z be Element of 1 holds op2.(x,z) <= op2.(x,y) + op2.(y,z)
proof
let x,y,z be Element of 1;
x={} & y={} by CARD_1:49,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
for a being Element of A holds f.(a,a) = 0;
attr f is discerning means
for a, b being Element of A st f.(a,b) = 0 holds a = b;
attr f is symmetric means
for a, b being Element of A holds f.(a,b) = f.(b,a);
attr f is triangle means
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
:Def6:
the distance of M is Reflexive;
attr M is discerning means
:Def7:
the distance of M is discerning;
attr M is symmetric means
:Def8:
the distance of M is symmetric;
attr M is triangle means
:Def9:
the distance of M is triangle;
end;
registration
cluster strict Reflexive discerning symmetric triangle non empty for
MetrStruct;
existence
proof
reconsider M = MetrStruct(#1,Empty^2-to-zero#) as strict non empty
MetrStruct;
take M;
A1: the distance of M is discerning
by Lm3;
A2: the distance of M is symmetric
by Lm4;
A3: the distance of M is triangle
by Lm5;
the distance of M is Reflexive
by Lm3;
hence thesis by A1,A2,A3;
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) .= 0 by A1;
hence thesis;
end;
hence M is Reflexive;
end;
assume M is Reflexive;
then the distance of M is Reflexive;
hence thesis;
end;
theorem Th2:
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;
hence thesis by A1;
end;
hence M is discerning;
end;
assume M is discerning;
then the distance of M is discerning;
hence thesis;
end;
theorem Th3:
for M being MetrStruct st
for a, b being Element of M holds dist(a,b) = dist(b,a) holds
M is symmetric
proof
let M be MetrStruct;
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) .= dist(b,a) by A1
.= (the distance of M).(b,a);
end;
hence M is symmetric;
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).(b,c) = dist(b,c);
(the distance of M).(a,b) = dist(a,b) &
(the distance of M).(a,c) = dist(a,c);
hence thesis by A1,A2;
end;
hence M is triangle;
end;
assume
A3: M is triangle;
let a, b, c be Element of M;
the distance of M is triangle by A3;
hence thesis;
end;
definition
let M be symmetric MetrStruct;
let a, b be Element of M;
redefine func dist(a,b); :: redefines dist (METRIC_1, definition)
commutativity
proof
the distance of M is symmetric by Def8;
hence thesis;
end;
end;
theorem Th5:
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: (1/2)*dist(a,a)=(1/2)*0 by Th1;
dist(a,a)<=dist(a,b)+dist(b,a) & dist(a,b) =(1/2)*(1*dist(a,b)+1*dist(a,
b)) by Th4;
hence thesis by A1,XREAL_1:64;
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);
A2: the distance of M is symmetric
proof
let a, b be Element of M;
(the distance of M).(a,b) = dist(a,b) .= dist(b,a) by A1
.= (the distance of M).(b,a);
hence thesis;
end;
A3: the distance of M is triangle
proof
let a, b, c be Element of M;
A4: (the distance of M).(b,c) = dist(b,c);
(the distance of M).(a,c) = dist(a,c) &
(the distance of M).(a,b) = dist(a,b);
hence thesis by A1,A4;
end;
A5: 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;
hence thesis by A1;
end;
the distance of M is Reflexive
proof
let a be Element of M;
(the distance of M).(a,a) = dist(a,a) .= 0 by A1;
hence thesis;
end;
hence thesis by A5,A2,A3,Def6,Def7,Def8,Def9;
end;
theorem Th7:
for M being MetrSpace, x,y being Element of M st x <> y holds 0 < dist(x,y)
proof
let M be MetrSpace;
let x,y be Element of M;
A1: dist(x,y) >= 0 by Th5;
assume x <> y;
then dist(x,y) <> 0 by Th2;
hence thesis by A1,XXREAL_0:1;
end;
definition
let A be set;
func discrete_dist A -> Function of [:A,A:], REAL means
:Def10:
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:90;
then reconsider f = {} as Function of [:A,A:], REAL by RELSET_1:12;
take f;
let x, y be Element of A;
thus f.(x,x) = 0;
x = {} by A1,SUBSET_1:def 1
.= y by A1,SUBSET_1:def 1;
hence thesis;
end;
suppose
A2: A is non empty;
0 in REAL & 1 in REAL by XREAL_0:def 1;
then {0,1} c= REAL & rng chi([:A,A:]\id A,[:A,A:]) c= {0,1}
by ZFMISC_1:32;
then
A3: rng chi([:A,A:]\id A,[:A,A:]) c= REAL by 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 A3,
RELSET_1:4;
take char;
let x,y be Element of A;
[:A,A:]\([:A,A:]\id A)=[:A,A:]/\id A by XBOOLE_1:48
.=id A by XBOOLE_1:28;
then [x,x] in [:A,A:]\([:A,A:]\id A) by A2,RELAT_1:def 10;
hence char.(x,x)=0 by FUNCT_3:37;
assume x<>y; then
A4: not [x,y] in id A by RELAT_1:def 10;
[x,y] in [:A,A:] by A2,ZFMISC_1:def 2;
then [x,y] in [:A,A:]\id A by A4,XBOOLE_0:def 5;
hence thesis by FUNCT_3:def 3;
end;
end;
uniqueness
proof
let f,f9 be Function of [:A,A:],REAL;
assume that
A5: for x,y being Element of A holds f.(x,x)=0 & (x<>y implies f.(x,y)=1) and
A6: for x,y being Element of A holds f9.(x,x)=0 & (x<>y implies f9.(x,y)=1);
now
let x,y be Element of A;
now
per cases;
suppose
A7: x=y;
hence f.(x,y) =0 by A5
.=f9.(x,y) by A6,A7;
end;
suppose
A8: x<>y;
hence f.(x,y) =1 by A5
.=f9.(x,y) by A6,A8;
end;
end;
hence f.(x,y)=f9.(x,y);
end;
hence thesis;
end;
end;
definition
let A be set;
func DiscreteSpace A -> strict MetrStruct equals
MetrStruct (#A,discrete_dist A#);
coherence;
end;
registration
let A be non empty set;
cluster DiscreteSpace A -> non empty;
coherence;
end;
registration
let A be set;
cluster DiscreteSpace A -> Reflexive discerning symmetric triangle;
coherence
proof
set M = MetrStruct (#A,discrete_dist A#);
A1: the distance of M is discerning
by Def10;
A2: the distance of M is symmetric
proof
let a, b be Element of M;
now
per cases;
suppose
A3: a <> b;
hence (the distance of M).(a,b) = 1 by Def10
.= (the distance of M).(b,a) by A3,Def10;
end;
suppose a = b;
hence thesis;
end;
end;
hence thesis;
end;
A4: the distance of M is triangle
proof
let a, b, c be Element of M;
A5: (the distance of M).(a,b) = 0 iff a=b by Def10;
per cases;
suppose
a=b & a=c;
hence thesis by A5;
end;
suppose
a=b & a<>c;
hence thesis by A5;
end;
suppose
A6: a=c & a<>b;
then
A7: (the distance of M).(b,c)=1 by Def10;
(the distance of M).(a,c)=0 & (the distance of M).(a,b)=1 by A6,Def10;
hence thesis by A7;
end;
suppose
A8: b=c & a<>c;
then (the distance of M).(b,c)=0 by Def10;
hence thesis by A8;
end;
suppose
A9: a<>b & a<>c & b<>c; then
A10: (the distance of M).(b,c)=1 by Def10;
(the distance of M).(a,c)=1 & (the distance of M).(a,b)=1 by A9,Def10;
hence thesis by A10;
end;
end;
the distance of M is Reflexive
by Def10;
hence thesis by A1,A2,A4;
end;
end;
definition
func real_dist -> Function of [:REAL,REAL:], REAL means
:Def12:
for x,y being Real holds it.(x,y) = |.x-y.|;
existence
proof
deffunc G(Real,Real)= In(|.$1-$2.|,REAL);
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 BINOP_1:
sch 4;
take F;
let x,y be Real;
reconsider x,y as Element of REAL by XREAL_0:def 1;
F.(x,y) = G(x,y) by A1;
hence thesis;
end;
uniqueness
proof
let F1,F2 be Function of [:REAL,REAL:],REAL;
assume that
A2: for x,y being Real holds F1.(x,y) = |.x-y.| and
A3: for x,y being Real holds F2.(x,y) = |.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)=|.x-y.| by A2
.=F2.(x,y) by A3;
end;
hence thesis;
end;
end;
theorem Th8:
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=|.x-y.| by Def12;
then x-y = 0 by ABSVALUE:2;
hence thesis;
end;
assume x=y;
then |.x-y.|=0 by ABSVALUE:2;
hence thesis by Def12;
end;
theorem Th9:
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)=|.x-y.| by Def12
.=|.-(x-y).| by COMPLEX1:52
.=|.y-x.|
.=real_dist.(y,x) by Def12;
end;
theorem Th10:
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;
|.x-y.|=|.(x-z)+(z-y).|;
then
A1: |.x-y.|<=|.x-z.|+|.z-y.| by COMPLEX1:56;
real_dist.(x,y)=|.x-y.| & real_dist.(x,z)=|.x-z.| by Def12;
hence thesis by A1,Def12;
end;
definition
func RealSpace -> strict MetrStruct equals
MetrStruct (# REAL, real_dist #);
coherence;
end;
registration
cluster RealSpace -> non empty;
coherence;
end;
registration
cluster RealSpace -> Reflexive discerning symmetric triangle;
coherence
proof
reconsider M = MetrStruct(#REAL,real_dist#) as non empty MetrStruct;
for a,b,c be 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) by Th8,Th9,Th10;
hence thesis by Th6;
end;
end;
definition
let M be MetrStruct, p be Element of M, r be Real;
func Ball(p,r) -> Subset of M means
:Def14:
it = {q where q is Element of M : dist(p,q) < r} if M is non empty
otherwise it is empty;
existence
proof
reconsider X = {} as Subset of M by XBOOLE_1:2;
thus M is non empty implies ex X being Subset of M st
X = {q where q is Element of M : dist(p,q) < r}
proof
assume M is non empty;
then reconsider M9 = M as non empty MetrStruct;
reconsider p9 = p as Element of M9;
defpred P[Element of M9] means dist(p9,$1)<r;
set X = {q where q is Element of M9: P[q]};
X c= the carrier of M9 from FRAENKEL:sch 10;
then reconsider X as Subset of M;
take X;
thus thesis;
end;
assume M is empty;
take X;
thus thesis;
end;
correctness;
end;
definition
let M be MetrStruct, p be Element of M, r be Real;
func cl_Ball(p,r) -> Subset of M means
:Def15:
it = {q where q is Element of M : dist(p,q) <= r} if M is non empty
otherwise it is empty;
existence
proof
reconsider X = {} as Subset of M by XBOOLE_1:2;
thus M is non empty implies ex X being Subset of M st
X = {q where q is Element of M : dist(p,q) <= r}
proof
assume M is non empty;
then reconsider M9 = M as non empty MetrStruct;
reconsider p9 = p as Element of M9;
defpred P[Element of M9] means dist(p9,$1)<=r;
set X = {q where q is Element of M9: P[q]};
X c= the carrier of M9 from FRAENKEL:sch 10;
then reconsider X as Subset of M;
take X;
thus thesis;
end;
assume M is empty;
take X;
thus thesis;
end;
correctness;
end;
definition
let M be MetrStruct, p be Element of M, r be Real;
func Sphere(p,r) -> Subset of M means
:Def16:
it = {q where q is Element of M : dist(p,q) = r} if M is non empty
otherwise it is empty;
existence
proof
reconsider X = {} as Subset of M by XBOOLE_1:2;
thus M is non empty implies ex X being Subset of M st
X = {q where q is Element of M : dist(p,q) = r}
proof
assume M is non empty;
then reconsider M9 = M as non empty MetrStruct;
reconsider p9 = p as Element of M9;
defpred P[Element of M9] means dist(p9,$1)=r;
set X = {q where q is Element of M9: P[q]};
X c= the carrier of M9 from FRAENKEL:sch 10;
then reconsider X as Subset of M;
take X;
thus thesis;
end;
assume M is empty;
take X;
thus thesis;
end;
correctness;
end;
reserve r for Real;
theorem Th11:
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);
then reconsider M9 = M as non empty MetrStruct;
reconsider p9 = p as Element of M9;
x in {q where q is Element of M9:dist(p9,q)<r} by A1,Def14;
then ex q be Element of M st x=q & dist(p,q)<r;
hence M is non empty & dist(p,x)<r by A1;
end;
assume M is non empty;
then reconsider M9 = M as non empty MetrStruct;
reconsider p9 = p as Element of M9;
assume dist(p,x)<r;
then x in {q where q is Element of M9:dist(p9,q)<r};
hence thesis by Def14;
end;
theorem Th12:
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);
then reconsider M9 = M as non empty MetrStruct;
reconsider p9 = p as Element of M9;
x in {q where q is Element of M9:dist(p9,q)<=r} by A1,Def15;
then ex q be Element of M st x=q & dist(p,q)<=r;
hence M is non empty & dist(p,x)<=r by A1;
end;
assume M is non empty;
then reconsider M9 = M as non empty MetrStruct;
reconsider p9 = p as Element of M9;
assume dist(p,x)<=r;
then x in {q where q is Element of M9:dist(p9,q)<=r};
hence thesis by Def15;
end;
theorem Th13:
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);
then reconsider M9 = M as non empty MetrStruct;
reconsider p9 = p as Element of M9;
x in {q where q is Element of M9:dist(p9,q)=r} by A1,Def16;
then ex q be Element of M st x=q & dist(p,q)=r;
hence M is non empty & dist(p,x)=r by A1;
end;
assume M is non empty;
then reconsider M9 = M as non empty MetrStruct;
reconsider p9 = p as Element of M9;
assume dist(p,x)=r;
then x in {q where q is Element of M9:dist(p9,q)=r};
hence thesis by Def16;
end;
theorem Th14:
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
A1: M is non empty;
now
let x be Element of M;
assume x in Ball(p,r);
then dist(p,x)<=r by Th11;
then x in {q where q is Element of M:dist(p,q)<=r};
hence x in cl_Ball(p,r) by A1,Def15;
end;
hence thesis by SUBSET_1:2;
end;
suppose
A2: M is empty;
then Ball(p,r) is empty;
hence thesis by A2,Def15;
end;
end;
theorem Th15:
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
A1: M is non empty;
now
let x be Element of M;
assume x in Sphere(p,r);
then dist(p,x)=r by Th13;
then x in {q where q is Element of M:dist(p,q)<=r};
hence x in cl_Ball(p,r) by Def15,A1;
end;
hence thesis by SUBSET_1:2;
end;
suppose
A2: M is empty;
then Sphere(p,r) is empty;
hence thesis by A2,Def15;
end;
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 Th14,Th15;
hence Sphere(p,r) \/ Ball(p,r) c= cl_Ball(p,r) by XBOOLE_1:8;
per cases;
suppose
A1: M is non empty;
now
let x be Element of M;
assume x in cl_Ball(p,r);
then
A2: dist(p,x)<=r by Th12;
now
per cases by A2,XXREAL_0:1;
case
dist(p,x)<r;
hence x in Ball(p,r) by A1,Th11;
end;
case
dist(p,x)=r;
hence x in Sphere(p,r) by A1,Th13;
end;
end;
hence x in Sphere(p,r) \/ Ball(p,r) by XBOOLE_0:def 3;
end;
hence thesis by SUBSET_1:2;
end;
suppose
A3: M is empty;
then Ball(p,r) is empty & cl_Ball(p,r) is empty;
hence thesis by A3,Def16;
end;
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 Def14;
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 Def15;
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 Def16;
begin :: SUB_METR
theorem
for x being set holds Empty^2-to-zero.(x,x) = 0
proof
let x be set;
per cases;
suppose [x,x] in [:1,1:];
hence thesis by CARD_1:49,FUNCT_2:50;
end;
suppose not [x,x] in [:1,1:]; then
not [x,x] in dom Empty^2-to-zero;
hence thesis by FUNCT_1:def 2;
end;
end;
theorem Th21:
for x,y being Element of 1 st x <> y holds 0 < Empty^2-to-zero.(x,y)
proof
let x,y be Element of 1;
x={} by CARD_1:49,TARSKI:def 1;
hence thesis by CARD_1:49,TARSKI:def 1;
end;
theorem Th22:
for x,y being Element of 1 holds
Empty^2-to-zero.(x,y) = Empty^2-to-zero.(y,x) by Lm4;
theorem Th23:
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:
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
let x,y,z be Element of 1;
A1: z={} by CARD_1:49,TARSKI:def 1;
x={} & y={} by CARD_1:49,TARSKI:def 1;
hence thesis by A1;
end;
set M0=MetrStruct(#1,Empty^2-to-zero#);
definition
let A be non empty set;
let f be Function of [:A,A:], REAL;
attr f is Discerning means
for a, b being Element of A holds a <> b implies 0 < f.(a,b);
end;
definition
let M be non empty MetrStruct;
attr M is Discerning means
the distance of M is Discerning;
end;
theorem Th25:
for M being non empty MetrStruct holds
( for a, b being Element of M holds a <> b implies 0 < dist(a,b)) iff
M is Discerning
proof
let M be non empty MetrStruct;
hereby
assume
A1: for a, b being Element of M st a <> b holds 0 < dist(a,b);
the distance of M is Discerning
proof
let a, b be Element of M;
assume a <> b;
then 0 < dist(a,b) by A1;
hence thesis;
end;
hence M is Discerning;
end;
assume M is Discerning;
then the distance of M is Discerning;
hence thesis;
end;
registration
cluster MetrStruct(#1,Empty^2-to-zero#) -> non empty;
coherence;
end;
registration
cluster MetrStruct(#1,Empty^2-to-zero#) -> Reflexive symmetric Discerning
triangle;
coherence
proof
A1: for x being Element of M0 holds dist(x,x) = 0 by Lm3;
A2: for x,y being Element of M0 holds dist(x,y) = dist(y,x) by Th22;
A3: for x,y being Element of M0 st x <> y holds 0 < dist(x,y) by Th21;
for x,y,z being Element of M0 holds dist(x,z) <= dist(x,y) + dist(y,z)
by Th23;
hence thesis by A2,A1,A3,Th25,Th1,Th3,Th4;
end;
end;
definition
let M be non empty MetrStruct;
attr M is ultra means :Def19:
for a, b, c being Element of M holds dist(a,c) <= max (dist(a,b),dist(b,c));
end;
registration
cluster strict ultra Reflexive symmetric Discerning triangle
for non empty MetrStruct;
existence
proof
take M0 = MetrStruct(#1,Empty^2-to-zero#);
M0 is ultra
by Th24;
hence thesis;
end;
end;
theorem Th26:
for M being Reflexive Discerning non empty MetrStruct,
a,b being Element of M holds 0 <= dist(a,b)
proof
let M be Reflexive Discerning non empty MetrStruct;
let a,b be Element of M;
now
per cases;
suppose a = b;
hence thesis by Th1;
end;
suppose a <> b;
hence thesis by Th25;
end;
end;
hence thesis;
end;
definition
mode PseudoMetricSpace is Reflexive symmetric triangle
non empty MetrStruct;
mode SemiMetricSpace is Reflexive Discerning symmetric
non empty MetrStruct;
mode NonSymmetricMetricSpace is Reflexive Discerning triangle
non empty MetrStruct;
mode UltraMetricSpace is ultra Reflexive symmetric Discerning
non empty MetrStruct;
end;
registration
cluster -> Discerning for non empty MetrSpace;
coherence
proof
let M be non empty MetrSpace;
for a, b being Element of M holds a <> b implies 0 < dist(a,b) by Th7;
hence thesis by Th25;
end;
end;
registration
cluster -> triangle discerning for UltraMetricSpace;
coherence
proof
let M be UltraMetricSpace;
now
let x,y,z be Element of M;
thus dist(x,y) = 0 iff x = y by Th25,Th1;
thus dist(x,y) = dist(y,x);
0 <= dist(x,y) & 0 <= dist(y,z) by Th26; then
A1: max(dist(x,y),dist(y,z)) <= dist(x,y) + dist(y,z) by SQUARE_1:2;
dist(x,z) <= max(dist(x,y),dist(y,z)) by Def19;
hence dist(x,z) <= dist(x,y) + dist(y,z) by A1,XXREAL_0:2;
end;
hence thesis by Th6;
end;
end;
definition
func Set_to_zero -> Function of [:2,2:],REAL equals
[:2,2:] --> 0;
coherence
proof
[:2,2:]--> In(0,REAL) is Function of [:2,2:],REAL;
hence thesis;
end;
end;
theorem Th27:
for x,y being Element of 2 holds Set_to_zero.(x,y) = 0
by ZFMISC_1:87,FUNCOP_1:7;
theorem Th28:
for x,y being Element of 2 holds Set_to_zero.(x,y) = Set_to_zero.(y,x)
proof
let x,y be Element of 2;
Set_to_zero.(x,y)=0 by Th27
.=Set_to_zero.(y,x) by Th27;
hence thesis;
end;
theorem Th29:
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
let x,y,z be Element of 2;
Set_to_zero.(x,y) = 0 & Set_to_zero.(y,z) = 0 by Th27;
hence thesis by Th27;
end;
definition
func ZeroSpace -> MetrStruct equals
MetrStruct(#2, Set_to_zero#);
coherence;
end;
registration
cluster ZeroSpace -> strict non empty;
coherence;
end;
registration
cluster ZeroSpace -> Reflexive symmetric triangle;
coherence
proof
set M = MetrStruct(#2,Set_to_zero#);
A1: for x,y,z being Element of M
holds dist(x,y) = dist(y,x) & dist(x,z) <= dist(x,y) + dist(y,z)
by Th28,Th29;
for x being Element of M holds dist(x,x) = 0 by Th27;
hence thesis by A1,Th1,Th3,Th4;
end;
end;
definition
let S be MetrStruct, p,q,r be Element of S;
pred q is_between p,r means
p <> q & p <> r & q <> r & dist(p,r) = dist(p,q) + dist(q,r);
end;
theorem
for S being symmetric triangle Reflexive non empty MetrStruct,
p, q, r being Element of S holds
q is_between p,r implies q is_between r,p
proof
let S be symmetric triangle Reflexive non empty MetrStruct,
p,q,r be Element of S;
assume
A1: q is_between p,r;
hence r <> q & r <> p & q <> p;
dist(p,r) = dist(p,q) + dist(q,r) by A1;
hence thesis;
end;
theorem
for S being MetrSpace, 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
let S be MetrSpace, p,q,r be Element of S;
assume
A1: q is_between p,r; then
A2: dist(p,r) = dist(p,q) + dist(q,r);
thus not p is_between q,r
by A2,Th7;
assume r is_between p,q; then
A3: dist(p,q) = dist(p,q) + dist(q,r) + dist(r,q) by A2;
q <> r by A1;
hence contradiction by A3,Th7;
end;
theorem
for S being MetrSpace, 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
let S be MetrSpace, p,q,r,s be Element of S;
assume
A1: q is_between p,r; then
A2: p<>q;
assume
A3: r is_between p,s; then
A4: p <> s & r <> s;
dist(p,r) = dist(p,q) + dist(q,r) by A1; then
A5: dist(p,s) = dist(p,q) + dist(q,r) + dist(r,s) by A3;
dist(p,s) <= dist(p,q) + dist(q,s) & dist(p,q) + dist(q,s) <=
(dist(q,r) + dist(r,s)) + dist(p,q) by Th4,XREAL_1:6; then
A6: dist(p,q) + dist(q,s) = dist(p,q) + (dist(q,r) + dist(r,s)) by A5,
XXREAL_0:1;
A7: q<>r by A1;
then q <> s by A5,Th7;
hence thesis by A2,A7,A4,A5,A6;
end;
definition
let M be non empty MetrStruct, p,r be Element of M;
func open_dist_Segment(p,r) -> Subset of M equals
{q where q is Element of M : q is_between p,r};
coherence
proof
defpred X[Element of M] means $1 is_between p,r;
{q where q is Element of M: X[q]} c= the carrier of M from FRAENKEL:
sch 10;
hence thesis;
end;
end;
theorem
for M being non empty MetrSpace, p,r,x being Element of M holds
x in open_dist_Segment(p,r) iff x is_between p,r
proof
let M be non empty MetrSpace, p,r,x be Element of M;
x in open_dist_Segment(p,r) implies x is_between p,r
proof
assume x in open_dist_Segment(p,r);
then ex q be Element of M st x = q & q is_between p,r;
hence thesis;
end;
hence thesis;
end;
definition
let M be non empty MetrStruct, p,r be Element of M;
func close_dist_Segment(p,r) -> Subset of M equals
{q where q is Element of M : q is_between p,r} \/ {p,r};
coherence
proof
defpred X[Element of M] means $1 is_between p,r;
A1: {p,r} c= the carrier of M by ZFMISC_1:32;
{q where q is Element of M : X[q] } c= the carrier of M
from FRAENKEL:sch 10;
hence thesis by A1,XBOOLE_1:8;
end;
end;
theorem
for M being non empty MetrStruct, 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
let M be non empty MetrStruct, p,r,x be Element of M;
A1: x in close_dist_Segment(p,r) implies (x is_between p,r or x = p or x = r)
proof
assume x in close_dist_Segment(p,r);
then x in {q where q is Element of M: q is_between p,r} or x in {p,r}
by XBOOLE_0:def 3; then
(ex q be Element of M st x = q & q is_between p,r) or (x = p or x = r)
by TARSKI:def 2;
hence thesis;
end;
now
assume x is_between p,r or x = p or x = r;
then x in {q where q is Element of M: q is_between p,r} or x in {p,r}
by TARSKI:def 2;
hence x in close_dist_Segment(p,r) by XBOOLE_0:def 3;
end;
hence thesis by A1;
end;