:: Metric Spaces
:: by Stanis{\l}awa Kanas, Adam Lecko and Mariusz Startek
::
:: Received May 3, 1990
:: Copyright (c) 1990 Association of Mizar Users
:: deftheorem defines dist METRIC_1:def 1 :
Lm2:
op2 . {} ,{} = 0
Lm3:
for x, y being Element of 1 holds
( op2 . x,y = 0 iff x = y )
Lm4:
for x, y being Element of 1 holds op2 . x,y = op2 . y,x
Lm5:
for x, y, z being Element of 1 holds op2 . x,z <= (op2 . x,y) + (op2 . y,z)
definition
canceled;let A be
set ;
let f be
PartFunc of
[:A,A:],
REAL ;
attr f is
Reflexive means :
Def3:
:: METRIC_1:def 3
for
a being
Element of
A holds
f . a,
a = 0 ;
attr f is
discerning means :
Def4:
:: METRIC_1:def 4
for
a,
b being
Element of
A st
f . a,
b = 0 holds
a = b;
attr f is
symmetric means :
Def5:
:: METRIC_1:def 5
for
a,
b being
Element of
A holds
f . a,
b = f . b,
a;
attr f is
triangle means :
Def6:
:: METRIC_1:def 6
for
a,
b,
c being
Element of
A holds
f . a,
c <= (f . a,b) + (f . b,c);
end;
:: deftheorem METRIC_1:def 2 :
canceled;
:: deftheorem Def3 defines Reflexive METRIC_1:def 3 :
:: deftheorem Def4 defines discerning METRIC_1:def 4 :
:: deftheorem Def5 defines symmetric METRIC_1:def 5 :
:: deftheorem Def6 defines triangle METRIC_1:def 6 :
:: deftheorem Def7 defines Reflexive METRIC_1:def 7 :
:: deftheorem Def8 defines discerning METRIC_1:def 8 :
:: deftheorem Def9 defines symmetric METRIC_1:def 9 :
:: deftheorem Def10 defines triangle METRIC_1:def 10 :
theorem Th1: :: METRIC_1:1
theorem :: METRIC_1:2
theorem Th3: :: METRIC_1:3
theorem Th4: :: METRIC_1:4
theorem :: METRIC_1:5
theorem Th6: :: METRIC_1:6
definition
let A be
set ;
func discrete_dist A -> Function of
[:A,A:],
REAL means :
Def11:
:: METRIC_1:def 11
for
x,
y being
Element of
A holds
(
it . x,
x = 0 & (
x <> y implies
it . x,
y = 1 ) );
existence
ex b1 being Function of [:A,A:], REAL st
for x, y being Element of A holds
( b1 . x,x = 0 & ( x <> y implies b1 . x,y = 1 ) )
uniqueness
for b1, b2 being Function of [:A,A:], REAL st ( for x, y being Element of A holds
( b1 . x,x = 0 & ( x <> y implies b1 . x,y = 1 ) ) ) & ( for x, y being Element of A holds
( b2 . x,x = 0 & ( x <> y implies b2 . x,y = 1 ) ) ) holds
b1 = b2
end;
:: deftheorem Def11 defines discrete_dist METRIC_1:def 11 :
:: deftheorem defines DiscreteSpace METRIC_1:def 12 :
definition
func real_dist -> Function of
[:REAL ,REAL :],
REAL means :
Def13:
:: METRIC_1:def 13
for
x,
y being
Element of
REAL holds
it . x,
y = abs (x - y);
existence
ex b1 being Function of [:REAL ,REAL :], REAL st
for x, y being Element of REAL holds b1 . x,y = abs (x - y)
uniqueness
for b1, b2 being Function of [:REAL ,REAL :], REAL st ( for x, y being Element of REAL holds b1 . x,y = abs (x - y) ) & ( for x, y being Element of REAL holds b2 . x,y = abs (x - y) ) holds
b1 = b2
end;
:: deftheorem Def13 defines real_dist METRIC_1:def 13 :
theorem :: METRIC_1:7
canceled;
theorem :: METRIC_1:8
canceled;
theorem Th9: :: METRIC_1:9
theorem Th10: :: METRIC_1:10
theorem Th11: :: METRIC_1:11
:: deftheorem defines RealSpace METRIC_1:def 14 :
:: deftheorem Def15 defines Ball METRIC_1:def 15 :
:: deftheorem Def16 defines cl_Ball METRIC_1:def 16 :
:: deftheorem Def17 defines Sphere METRIC_1:def 17 :
Lm6:
for r being real number
for M being non empty MetrStruct
for p being Element of M holds Ball p,r = { q where q is Element of M : dist p,q < r }
Lm7:
for r being real number
for M being non empty MetrStruct
for p being Element of M holds cl_Ball p,r = { q where q is Element of M : dist p,q <= r }
Lm8:
for r being real number
for M being non empty MetrStruct
for p being Element of M holds Sphere p,r = { q where q is Element of M : dist p,q = r }
theorem Th12: :: METRIC_1:12
theorem Th13: :: METRIC_1:13
theorem Th14: :: METRIC_1:14
theorem Th15: :: METRIC_1:15
theorem Th16: :: METRIC_1:16
theorem :: METRIC_1:17
theorem :: METRIC_1:18
theorem :: METRIC_1:19
theorem :: METRIC_1:20