:: METRIC_1 semantic presentation

definition

attr c₁ is strict;
struct MetrStruct -> 1-sorted ;
aggr MetrStruct(# carrier, distance #) -> MetrStruct ;
sel distance c₁ -> Function of [:the carrier of c₁,the carrier of c₁:], REAL ;

end;

registration

cluster non empty strict MetrStruct ;
existence

proof end;

end;

definition

let A, B be set ;
let f be PartFunc of [:A,B:], REAL ;
let a be Element of A;
let b be Element of B;
:: original: .
redefine func f . a,b -> Real;
coherence

proof 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;
coherence ;

end;

:: deftheorem defines dist METRIC_1:def 1 :

definition

func Empty^2-to-zero -> Function of [:{{} },{{} }:], REAL equals :: METRIC_1:def 2
[:{{} },{{} }:] --> 0;
coherence

proof end;

end;

:: deftheorem defines Empty^2-to-zero METRIC_1:def 2 :

Lm1: [{} ,{} ] in [:{{} },{{} }:]
by ZFMISC_1:34;

Lm2: Empty^2-to-zero . {} ,{} = Empty^2-to-zero . [{} ,{} ]
.= 0 by Lm1, FUNCOP_1:13 ;

Lm3: for x, y being Element of {{} } holds
( Empty^2-to-zero . x,y = 0 iff x = y )

proof end;

Lm4: for x, y being Element of {{} } holds Empty^2-to-zero . x,y = Empty^2-to-zero . y,x

proof end;

Lm5: for x, y, z being Element of {{} } holds Empty^2-to-zero . x,z <= (Empty^2-to-zero . x,y) + (Empty^2-to-zero . y,z)

proof end;

definition

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 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 :

definition

let M be MetrStruct ;
attr M is Reflexive means :Def7: :: METRIC_1:def 7
the distance of M is Reflexive;
attr M is discerning means :Def8: :: METRIC_1:def 8
the distance of M is discerning;
attr M is symmetric means :Def9: :: METRIC_1:def 9
the distance of M is symmetric;
attr M is triangle means :Def10: :: METRIC_1:def 10
the distance of M is triangle;

end;

:: 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 :

registration

cluster non empty strict Reflexive discerning symmetric triangle MetrStruct ;
existence

proof end;

end;

definition

mode MetrSpace is Reflexive discerning symmetric triangle MetrStruct ;

end;

theorem Th1: :: METRIC_1:1

for M being MetrStruct holds
( ( for a being Element of M holds dist a,a = 0 ) iff M is Reflexive )

proof end;

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 )

proof end;

theorem Th3: :: METRIC_1:3

for M being MetrStruct holds
( ( for a, b being Element of M holds dist a,b = dist b,a ) iff M is symmetric )

proof end;

theorem Th4: :: 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 )

proof end;

definition

let M be symmetric MetrStruct ;
let a, b be Element of M;
:: original: dist
redefine func dist a,b -> Real;
commutativity by Th3;

end;

theorem :: METRIC_1:5

for M being Reflexive symmetric triangle MetrStruct
for a, b being Element of M holds 0 <= dist a,b

proof end;

theorem Th6: :: METRIC_1:6

for M being MetrStruct st ( for a, b, c being Element of M holds
( ( dist a,b = 0 implies a = b ) & ( a = b implies dist a,b = 0 ) & dist a,b = dist b,a & dist a,c <= (dist a,b) + (dist b,c) ) ) holds
M is MetrSpace

proof end;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines discrete_dist METRIC_1:def 11 :

definition

let A be set ;
func DiscreteSpace A -> strict MetrStruct equals :: METRIC_1:def 12
MetrStruct(# A,(discrete_dist A) #);
coherence ;

end;

:: deftheorem defines DiscreteSpace METRIC_1:def 12 :

registration

let A be non empty set ;
cluster DiscreteSpace A -> non empty strict ;
coherence by STRUCT_0:def 1;

end;

registration

let A be set ;
cluster DiscreteSpace A -> strict Reflexive discerning symmetric triangle ;
coherence

proof end;

end;

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

proof end;

uniqueness

proof end;

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

for x, y being Element of REAL holds
( real_dist . x,y = 0 iff x = y )

proof end;

theorem Th10: :: METRIC_1:10

for x, y being Element of REAL holds real_dist . x,y = real_dist . y,x

proof end;

theorem Th11: :: METRIC_1:11

for x, y, z being Element of REAL holds real_dist . x,y <= (real_dist . x,z) + (real_dist . z,y)

proof end;

definition

func RealSpace -> strict MetrStruct equals :: METRIC_1:def 14
MetrStruct(# REAL ,real_dist #);
coherence ;

end;

:: deftheorem defines RealSpace METRIC_1:def 14 :

registration

cluster RealSpace -> non empty strict ;
coherence by STRUCT_0:def 1;

end;

registration

cluster RealSpace -> non empty strict Reflexive discerning symmetric triangle ;
coherence

proof end;

end;

definition

let M be MetrStruct ;
let p be Element of M;
let r be real number ;
func Ball p,r -> Subset of M means :Def15: :: METRIC_1:def 15
ex M' being non empty MetrStruct ex p' being Element of M' st
( M' = M & p' = p & it = { q where q is Element of M' : dist p',q < r } ) if not M is empty
otherwise it is empty;
existence

proof end;

correctness ;

end;

:: deftheorem Def15 defines Ball METRIC_1:def 15 :

definition

let M be MetrStruct ;
let p be Element of M;
let r be real number ;
func cl_Ball p,r -> Subset of M means :Def16: :: METRIC_1:def 16
ex M' being non empty MetrStruct ex p' being Element of M' st
( M' = M & p' = p & it = { q where q is Element of M' : dist p',q <= r } ) if not M is empty
otherwise it is empty;
existence

proof end;

correctness ;

end;

:: deftheorem Def16 defines cl_Ball METRIC_1:def 16 :

definition

let M be MetrStruct ;
let p be Element of M;
let r be real number ;
func Sphere p,r -> Subset of M means :Def17: :: METRIC_1:def 17
ex M' being non empty MetrStruct ex p' being Element of M' st
( M' = M & p' = p & it = { q where q is Element of M' : dist p',q = r } ) if not M is empty
otherwise it is empty;
existence

proof end;

correctness ;

end;

:: 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 }

proof end;

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 }

proof end;

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 }

proof end;

theorem Th12: :: METRIC_1:12

for r being real number
for M being MetrStruct
for p, x being Element of M holds
( x in Ball p,r iff ( not M is empty & dist p,x < r ) )

proof end;

theorem Th13: :: METRIC_1:13

for r being real number
for M being MetrStruct
for p, x being Element of M holds
( x in cl_Ball p,r iff ( not M is empty & dist p,x <= r ) )

proof end;

theorem Th14: :: METRIC_1:14

for r being real number
for M being MetrStruct
for p, x being Element of M holds
( x in Sphere p,r iff ( not M is empty & dist p,x = r ) )

proof end;

theorem Th15: :: METRIC_1:15

for r being real number
for M being MetrStruct
for p being Element of M holds Ball p,r c= cl_Ball p,r

proof end;

theorem Th16: :: METRIC_1:16

for r being real number
for M being MetrStruct
for p being Element of M holds Sphere p,r c= cl_Ball p,r

proof end;

theorem :: METRIC_1:17

for r being real number
for M being MetrStruct
for p being Element of M holds (Sphere p,r) \/ (Ball p,r) = cl_Ball p,r

proof end;

theorem :: METRIC_1:18

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 } by Lm6;

theorem :: METRIC_1:19

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 } by Lm7;

theorem :: METRIC_1:20

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 } by Lm8;