:: METRIC_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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

registration
cluster non empty strict MetrStruct ;
existence
ex b1 being MetrStruct st
( not b1 is empty & b1 is strict )
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
f . a,b is Real
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
the distance of M . a,b is Real
;
end;

:: deftheorem defines dist METRIC_1:def 1 :
for M being MetrStruct
for a, b being Element of M holds dist a,b = the distance of M . a,b;

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

:: deftheorem defines Empty^2-to-zero METRIC_1:def 2 :
Empty^2-to-zero = [:{{} },{{} }:] --> 0;

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 :
for A being set
for f being PartFunc of [:A,A:], REAL holds
( f is Reflexive iff for a being Element of A holds f . a,a = 0 );

:: deftheorem Def4 defines discerning METRIC_1:def 4 :
for A being set
for f being PartFunc of [:A,A:], REAL holds
( f is discerning iff for a, b being Element of A st f . a,b = 0 holds
a = b );

:: deftheorem Def5 defines symmetric METRIC_1:def 5 :
for A being set
for f being PartFunc of [:A,A:], REAL holds
( f is symmetric iff for a, b being Element of A holds f . a,b = f . b,a );

:: deftheorem Def6 defines triangle METRIC_1:def 6 :
for A being set
for f being PartFunc of [:A,A:], REAL holds
( f is triangle iff for a, b, c being Element of A holds f . a,c <= (f . a,b) + (f . b,c) );

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 :
for M being MetrStruct holds
( M is Reflexive iff the distance of M is Reflexive );

:: deftheorem Def8 defines discerning METRIC_1:def 8 :
for M being MetrStruct holds
( M is discerning iff the distance of M is discerning );

:: deftheorem Def9 defines symmetric METRIC_1:def 9 :
for M being MetrStruct holds
( M is symmetric iff the distance of M is symmetric );

:: deftheorem Def10 defines triangle METRIC_1:def 10 :
for M being MetrStruct holds
( M is triangle iff the distance of M is triangle );

registration
cluster non empty strict Reflexive discerning symmetric triangle MetrStruct ;
existence
ex b1 being MetrStruct st
( b1 is strict & b1 is Reflexive & b1 is discerning & b1 is symmetric & b1 is triangle & not b1 is empty )
proof end;
end;

definition
mode MetrSpace is Reflexive discerning symmetric triangle MetrStruct ;
end;

theorem Th1: :: METRIC_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
for a, b being Element of M holds dist a,b = dist b,a
by Th3;
end;

theorem :: METRIC_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
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 ) )
proof end;
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
proof end;
end;

:: deftheorem Def11 defines discrete_dist METRIC_1:def 11 :
for A being set
for b2 being Function of [:A,A:], REAL holds
( b2 = discrete_dist A iff for x, y being Element of A holds
( b2 . x,x = 0 & ( x <> y implies b2 . x,y = 1 ) ) );

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

:: deftheorem defines DiscreteSpace METRIC_1:def 12 :
for A being set holds DiscreteSpace A = MetrStruct(# A,(discrete_dist A) #);

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

registration
let A be set ;
cluster DiscreteSpace A -> strict Reflexive discerning symmetric triangle ;
coherence
( DiscreteSpace A is Reflexive & DiscreteSpace A is discerning & DiscreteSpace A is symmetric & DiscreteSpace A is triangle )
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
ex b1 being Function of [:REAL ,REAL :], REAL st
for x, y being Element of REAL holds b1 . x,y = abs (x - y)
proof end;
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
proof end;
end;

:: deftheorem Def13 defines real_dist METRIC_1:def 13 :
for b1 being Function of [:REAL ,REAL :], REAL holds
( b1 = real_dist iff for x, y being Element of REAL holds b1 . x,y = abs (x - y) );

theorem :: METRIC_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: METRIC_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th9: :: METRIC_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being Element of REAL holds
( real_dist . x,y = 0 iff x = y )
proof end;

theorem Th10: :: METRIC_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being Element of REAL holds real_dist . x,y = real_dist . y,x
proof end;

theorem Th11: :: METRIC_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
MetrStruct(# REAL ,real_dist #) is strict MetrStruct
;
end;

:: deftheorem defines RealSpace METRIC_1:def 14 :
RealSpace = MetrStruct(# REAL ,real_dist #);

registration
cluster RealSpace -> non empty strict ;
coherence
not RealSpace is empty
by STRUCT_0:def 1;
end;

registration
cluster RealSpace -> non empty strict Reflexive discerning symmetric triangle ;
coherence
( RealSpace is Reflexive & RealSpace is discerning & RealSpace is symmetric & RealSpace is triangle )
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
( ( not M is empty implies ex b1 being Subset of M ex M' being non empty MetrStruct ex p' being Element of M' st
( M' = M & p' = p & b1 = { q where q is Element of M' : dist p',q < r } ) ) & ( M is empty implies ex b1 being Subset of M st b1 is empty ) )
proof end;
correctness
consistency
for b1 being Subset of M holds verum
;
uniqueness
for b1, b2 being Subset of M holds
( ( not M is empty & ex M' being non empty MetrStruct ex p' being Element of M' st
( M' = M & p' = p & b1 = { q where q is Element of M' : dist p',q < r } ) & ex M' being non empty MetrStruct ex p' being Element of M' st
( M' = M & p' = p & b2 = { q where q is Element of M' : dist p',q < r } ) implies b1 = b2 ) & ( M is empty & b1 is empty & b2 is empty implies b1 = b2 ) )
;
;
end;

:: deftheorem Def15 defines Ball METRIC_1:def 15 :
for M being MetrStruct
for p being Element of M
for r being real number
for b4 being Subset of M holds
( ( not M is empty implies ( b4 = Ball p,r iff ex M' being non empty MetrStruct ex p' being Element of M' st
( M' = M & p' = p & b4 = { q where q is Element of M' : dist p',q < r } ) ) ) & ( M is empty implies ( b4 = Ball p,r iff b4 is empty ) ) );

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
( ( not M is empty implies ex b1 being Subset of M ex M' being non empty MetrStruct ex p' being Element of M' st
( M' = M & p' = p & b1 = { q where q is Element of M' : dist p',q <= r } ) ) & ( M is empty implies ex b1 being Subset of M st b1 is empty ) )
proof end;
correctness
consistency
for b1 being Subset of M holds verum
;
uniqueness
for b1, b2 being Subset of M holds
( ( not M is empty & ex M' being non empty MetrStruct ex p' being Element of M' st
( M' = M & p' = p & b1 = { q where q is Element of M' : dist p',q <= r } ) & ex M' being non empty MetrStruct ex p' being Element of M' st
( M' = M & p' = p & b2 = { q where q is Element of M' : dist p',q <= r } ) implies b1 = b2 ) & ( M is empty & b1 is empty & b2 is empty implies b1 = b2 ) )
;
;
end;

:: deftheorem Def16 defines cl_Ball METRIC_1:def 16 :
for M being MetrStruct
for p being Element of M
for r being real number
for b4 being Subset of M holds
( ( not M is empty implies ( b4 = cl_Ball p,r iff ex M' being non empty MetrStruct ex p' being Element of M' st
( M' = M & p' = p & b4 = { q where q is Element of M' : dist p',q <= r } ) ) ) & ( M is empty implies ( b4 = cl_Ball p,r iff b4 is empty ) ) );

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
( ( not M is empty implies ex b1 being Subset of M ex M' being non empty MetrStruct ex p' being Element of M' st
( M' = M & p' = p & b1 = { q where q is Element of M' : dist p',q = r } ) ) & ( M is empty implies ex b1 being Subset of M st b1 is empty ) )
proof end;
correctness
consistency
for b1 being Subset of M holds verum
;
uniqueness
for b1, b2 being Subset of M holds
( ( not M is empty & ex M' being non empty MetrStruct ex p' being Element of M' st
( M' = M & p' = p & b1 = { q where q is Element of M' : dist p',q = r } ) & ex M' being non empty MetrStruct ex p' being Element of M' st
( M' = M & p' = p & b2 = { q where q is Element of M' : dist p',q = r } ) implies b1 = b2 ) & ( M is empty & b1 is empty & b2 is empty implies b1 = b2 ) )
;
;
end;

:: deftheorem Def17 defines Sphere METRIC_1:def 17 :
for M being MetrStruct
for p being Element of M
for r being real number
for b4 being Subset of M holds
( ( not M is empty implies ( b4 = Sphere p,r iff ex M' being non empty MetrStruct ex p' being Element of M' st
( M' = M & p' = p & b4 = { q where q is Element of M' : dist p',q = r } ) ) ) & ( M is empty implies ( b4 = Sphere p,r iff b4 is empty ) ) );

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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;