:: Metric Spaces
:: by Stanis{\l}awa Kanas, Adam Lecko and Mariusz Startek
::
:: Received May 3, 1990
:: Copyright (c) 1990-2016 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;
begin
definition
struct(1-sorted) MetrStruct
(# carrier -> set,
distance -> Function of [:the carrier,the carrier:],REAL #);
end;
registration
cluster non empty strict for MetrStruct;
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
:: METRIC_1:def 1
(the distance of M).(a,b);
end;
notation
synonym Empty^2-to-zero for op2;
end;
definition
redefine func Empty^2-to-zero -> Function of [:1,1:], REAL;
end;
registration
cluster op2 -> natural-valued for Function;
end;
registration
let f be natural-valued Function;
let x,y be object;
cluster f.(x,y) -> natural;
end;
definition
let A be set;
let f be PartFunc of [:A,A:], REAL;
attr f is Reflexive means
:: METRIC_1:def 2
for a being Element of A holds f.(a,a) = 0;
attr f is discerning means
:: METRIC_1:def 3
for a, b being Element of A st f.(a,b) = 0 holds a = b;
attr f is symmetric means
:: METRIC_1:def 4
for a, b being Element of A holds f.(a,b) = f.(b,a);
attr f is triangle means
:: METRIC_1:def 5
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 6
the distance of M is Reflexive;
attr M is discerning means
:: METRIC_1:def 7
the distance of M is discerning;
attr M is symmetric means
:: METRIC_1:def 8
the distance of M is symmetric;
attr M is triangle means
:: METRIC_1:def 9
the distance of M is triangle;
end;
registration
cluster strict Reflexive discerning symmetric triangle non empty for
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 st
for a, b being Element of M holds dist(a,b) = dist(b,a) holds
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;
theorem :: METRIC_1:7
for M being MetrSpace, x,y being Element of M st x <> y holds 0 < dist(x,y);
definition
let A be set;
func discrete_dist A -> Function of [:A,A:], REAL means
:: METRIC_1:def 10
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 11
MetrStruct (#A,discrete_dist A#);
end;
registration
let A be non empty set;
cluster DiscreteSpace A -> non empty;
end;
registration
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 12
for x,y being Real holds it.(x,y) = |.x-y.|;
end;
theorem :: METRIC_1:8
for x,y being Element of REAL holds real_dist.(x,y) = 0 iff x = y;
theorem :: METRIC_1:9
for x,y being Element of REAL holds real_dist.(x,y) = real_dist.(y,x);
theorem :: METRIC_1:10
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 13
MetrStruct (# REAL, real_dist #);
end;
registration
cluster RealSpace -> non empty;
end;
registration
cluster RealSpace -> Reflexive discerning symmetric triangle;
end;
definition
let M be MetrStruct, p be Element of M, r be Real;
func Ball(p,r) -> Subset of M means
:: METRIC_1:def 14
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;
func cl_Ball(p,r) -> Subset of M means
:: METRIC_1:def 15
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;
func Sphere(p,r) -> Subset of M means
:: METRIC_1:def 16
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;
theorem :: METRIC_1:11
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:12
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:13
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:14
for M being MetrStruct, p being Element of M holds Ball(p,r) c= cl_Ball(p,r);
theorem :: METRIC_1:15
for M being MetrStruct, p being Element of M holds Sphere(p,r)
c= cl_Ball(p,r);
theorem :: METRIC_1:16
for M being MetrStruct, p being Element of M holds
Sphere(p,r) \/ Ball(p,r) = cl_Ball(p,r);
theorem :: METRIC_1:17
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:18
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:19
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};
begin :: SUB_METR
theorem :: METRIC_1:20
for x being set holds Empty^2-to-zero.(x,x) = 0;
theorem :: METRIC_1:21
for x,y being Element of 1 st x <> y holds 0 < Empty^2-to-zero.(x,y);
theorem :: METRIC_1:22
for x,y being Element of 1 holds
Empty^2-to-zero.(x,y) = Empty^2-to-zero.(y,x);
theorem :: METRIC_1:23
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);
theorem :: METRIC_1:24
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));
definition
let A be non empty set;
let f be Function of [:A,A:], REAL;
attr f is Discerning means
:: METRIC_1:def 17
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
:: METRIC_1:def 18
the distance of M is Discerning;
end;
theorem :: METRIC_1:25
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;
registration
cluster MetrStruct(#1,Empty^2-to-zero#) -> non empty;
end;
registration
cluster MetrStruct(#1,Empty^2-to-zero#) -> Reflexive symmetric Discerning
triangle;
end;
definition
let M be non empty MetrStruct;
attr M is ultra means
:: METRIC_1:def 19
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;
end;
theorem :: METRIC_1:26
for M being Reflexive Discerning non empty MetrStruct,
a,b being Element of M holds 0 <= dist(a,b);
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;
end;
registration
cluster -> triangle discerning for UltraMetricSpace;
end;
definition
func Set_to_zero -> Function of [:2,2:],REAL equals
:: METRIC_1:def 20
[:2,2:] --> 0;
end;
theorem :: METRIC_1:27
for x,y being Element of 2 holds Set_to_zero.(x,y) = 0;
theorem :: METRIC_1:28
for x,y being Element of 2 holds Set_to_zero.(x,y) = Set_to_zero.(y,x);
theorem :: METRIC_1:29
for x,y,z being Element of 2 holds
Set_to_zero.(x,z) <= Set_to_zero.(x,y) + Set_to_zero.(y,z);
definition
func ZeroSpace -> MetrStruct equals
:: METRIC_1:def 21
MetrStruct(#2, Set_to_zero#);
end;
registration
cluster ZeroSpace -> strict non empty;
end;
registration
cluster ZeroSpace -> Reflexive symmetric triangle;
end;
definition
let S be MetrStruct, p,q,r be Element of S;
pred q is_between p,r means
:: METRIC_1:def 22
p <> q & p <> r & q <> r & dist(p,r) = dist(p,q) + dist(q,r);
end;
theorem :: METRIC_1:30
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;
theorem :: METRIC_1:31
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;
theorem :: METRIC_1:32
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;
definition
let M be non empty MetrStruct, p,r be Element of M;
func open_dist_Segment(p,r) -> Subset of M equals
:: METRIC_1:def 23
{q where q is Element of M : q is_between p,r};
end;
theorem :: METRIC_1:33
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;
definition
let M be non empty MetrStruct, p,r be Element of M;
func close_dist_Segment(p,r) -> Subset of M equals
:: METRIC_1:def 24
{q where q is Element of M : q is_between p,r} \/ {p,r};
end;
theorem :: METRIC_1:34
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);