begin
:: deftheorem defines dist METRIC_1:def 1 :
Lm1:
op2 . {} ,{} = 0
Lm2:
for x, y being Element of 1 holds
( op2 . x,y = 0 iff x = y )
Lm3:
for x, y being Element of 1 holds op2 . x,y = op2 . y,x
Lm4:
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:
for
a being
Element of
A holds
f . a,
a = 0 ;
attr f is
discerning means :
Def4:
for
a,
b being
Element of
A st
f . a,
b = 0 holds
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;
:: 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:
theorem
theorem Th3:
theorem Th4:
theorem
theorem Th6:
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
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:
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
canceled;
theorem
canceled;
theorem Th9:
theorem Th10:
theorem Th11:
:: 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 :
Lm5:
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 }
Lm6:
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 }
Lm7:
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:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem
theorem
theorem
theorem