:: Submetric Spaces - Part I
:: by Adam Lecko and Mariusz Startek
::
:: Received September 27, 1990
:: Copyright (c) 1990 Association of Mizar Users



theorem Th1: :: SUB_METR:1
for x, y being real number st 0 <= x & 0 <= y holds
max x,y <= x + y
proof end;

theorem Th2: :: SUB_METR:2
for M being MetrSpace
for x, y being Element of M st x <> y holds
0 < dist x,y
proof end;

theorem :: SUB_METR:3
canceled;

theorem Th4: :: SUB_METR:4
for x being Element of 1 holds Empty^2-to-zero . x,x = 0
proof end;

theorem Th5: :: SUB_METR:5
for x, y being Element of 1 st x <> y holds
0 < Empty^2-to-zero . x,y
proof end;

theorem Th6: :: SUB_METR:6
for x, y being Element of 1 holds Empty^2-to-zero . x,y = Empty^2-to-zero . y,x
proof end;

theorem Th7: :: SUB_METR:7
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)
proof end;

theorem Th8: :: SUB_METR:8
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)
proof end;

set M0 = MetrStruct(# 1,Empty^2-to-zero #);

definition
mode PseudoMetricSpace is non empty Reflexive symmetric triangle MetrStruct ;
end;

definition
let A be non empty set ;
let f be Function of [:A,A:],REAL ;
attr f is Discerning means :Def1: :: SUB_METR:def 1
for a, b being Element of A st a <> b holds
0 < f . a,b;
end;

:: deftheorem Def1 defines Discerning SUB_METR:def 1 :
for A being non empty set
for f being Function of [:A,A:],REAL holds
( f is Discerning iff for a, b being Element of A st a <> b holds
0 < f . a,b );

definition
let M be non empty MetrStruct ;
attr M is Discerning means :Def2: :: SUB_METR:def 2
the distance of M is Discerning ;
end;

:: deftheorem Def2 defines Discerning SUB_METR:def 2 :
for M being non empty MetrStruct holds
( M is Discerning iff the distance of M is Discerning );

theorem :: SUB_METR:9
canceled;

theorem :: SUB_METR:10
canceled;

theorem :: SUB_METR:11
canceled;

theorem :: SUB_METR:12
canceled;

theorem :: SUB_METR:13
canceled;

theorem Th14: :: SUB_METR:14
for M being non empty MetrStruct holds
( ( for a, b being Element of M st a <> b holds
0 < dist a,b ) iff M is Discerning )
proof end;

registration
cluster MetrStruct(# 1,Empty^2-to-zero #) -> Reflexive symmetric triangle Discerning ;
coherence
( MetrStruct(# 1,Empty^2-to-zero #) is Reflexive & MetrStruct(# 1,Empty^2-to-zero #) is symmetric & MetrStruct(# 1,Empty^2-to-zero #) is Discerning & MetrStruct(# 1,Empty^2-to-zero #) is triangle )
proof end;
end;

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

definition
mode SemiMetricSpace is non empty Reflexive symmetric Discerning MetrStruct ;
end;

theorem :: SUB_METR:15
canceled;

theorem :: SUB_METR:16
canceled;

theorem :: SUB_METR:17
canceled;

theorem Th18: :: SUB_METR:18
for M being non empty Reflexive Discerning MetrStruct
for a, b being Element of M holds 0 <= dist a,b
proof end;

definition
mode NonSymmetricMetricSpace is non empty Reflexive triangle Discerning MetrStruct ;
end;

definition
let M be non empty MetrStruct ;
canceled;
attr M is ultra means :Def4: :: SUB_METR:def 4
for a, b, c being Element of M holds dist a,c <= max (dist a,b),(dist b,c);
end;

:: deftheorem SUB_METR:def 3 :
canceled;

:: deftheorem Def4 defines ultra SUB_METR:def 4 :
for M being non empty MetrStruct holds
( M is ultra iff for a, b, c being Element of M holds dist a,c <= max (dist a,b),(dist b,c) );

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

definition
mode UltraMetricSpace is non empty Reflexive symmetric Discerning ultra MetrStruct ;
end;

registration
cluster non empty -> non empty Discerning MetrStruct ;
coherence
for b1 being non empty MetrSpace holds b1 is Discerning
proof end;
end;

registration
cluster -> discerning triangle MetrStruct ;
coherence
for b1 being UltraMetricSpace holds
( b1 is triangle & b1 is discerning )
proof end;
end;

definition
func Set_to_zero -> Function of [:{{} ,{{} }},{{} ,{{} }}:],REAL equals :: SUB_METR:def 5
[:{{} ,{{} }},{{} ,{{} }}:] --> 0 ;
coherence
[:{{} ,{{} }},{{} ,{{} }}:] --> 0 is Function of [:{{} ,{{} }},{{} ,{{} }}:],REAL
;
end;

:: deftheorem defines Set_to_zero SUB_METR:def 5 :
Set_to_zero = [:{{} ,{{} }},{{} ,{{} }}:] --> 0 ;

theorem :: SUB_METR:19
canceled;

theorem :: SUB_METR:20
canceled;

theorem :: SUB_METR:21
canceled;

theorem :: SUB_METR:22
canceled;

theorem :: SUB_METR:23
canceled;

theorem :: SUB_METR:24
canceled;

theorem :: SUB_METR:25
canceled;

theorem :: SUB_METR:26
canceled;

theorem :: SUB_METR:27
canceled;

theorem :: SUB_METR:28
canceled;

theorem :: SUB_METR:29
canceled;

theorem :: SUB_METR:30
canceled;

theorem :: SUB_METR:31
canceled;

theorem :: SUB_METR:32
canceled;

theorem :: SUB_METR:33
canceled;

theorem :: SUB_METR:34
canceled;

theorem :: SUB_METR:35
canceled;

theorem :: SUB_METR:36
canceled;

theorem :: SUB_METR:37
canceled;

theorem :: SUB_METR:38
canceled;

theorem :: SUB_METR:39
canceled;

theorem Th40: :: SUB_METR:40
for x, y being Element of {{} ,{{} }} holds Set_to_zero . x,y = 0
proof end;

theorem :: SUB_METR:41
canceled;

theorem Th42: :: SUB_METR:42
for x, y being Element of {{} ,{{} }} holds Set_to_zero . x,y = Set_to_zero . y,x
proof end;

theorem Th43: :: SUB_METR:43
for x, y, z being Element of {{} ,{{} }} holds Set_to_zero . x,z <= (Set_to_zero . x,y) + (Set_to_zero . y,z)
proof end;

definition
func ZeroSpace -> MetrStruct equals :: SUB_METR:def 6
MetrStruct(# {{} ,{{} }},Set_to_zero #);
coherence
MetrStruct(# {{} ,{{} }},Set_to_zero #) is MetrStruct
;
end;

:: deftheorem defines ZeroSpace SUB_METR:def 6 :
ZeroSpace = MetrStruct(# {{} ,{{} }},Set_to_zero #);

registration
cluster ZeroSpace -> non empty strict ;
coherence
( ZeroSpace is strict & not ZeroSpace is empty )
;
end;

registration
cluster ZeroSpace -> Reflexive symmetric triangle ;
coherence
( ZeroSpace is Reflexive & ZeroSpace is symmetric & ZeroSpace is triangle )
proof end;
end;

definition
let S be MetrStruct ;
let p, q, r be Element of S;
pred q is_between p,r means :Def7: :: SUB_METR:def 7
( p <> q & p <> r & q <> r & dist p,r = (dist p,q) + (dist q,r) );
end;

:: deftheorem Def7 defines is_between SUB_METR:def 7 :
for S being MetrStruct
for p, q, r being Element of S holds
( q is_between p,r iff ( p <> q & p <> r & q <> r & dist p,r = (dist p,q) + (dist q,r) ) );

theorem :: SUB_METR:44
canceled;

theorem :: SUB_METR:45
canceled;

theorem :: SUB_METR:46
canceled;

theorem :: SUB_METR:47
for S being non empty Reflexive symmetric triangle MetrStruct
for p, q, r being Element of S st q is_between p,r holds
q is_between r,p
proof end;

theorem :: SUB_METR:48
for S being MetrSpace
for 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 )
proof end;

theorem :: SUB_METR:49
for S being MetrSpace
for 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 )
proof end;

definition
let M be non empty MetrStruct ;
let p, r be Element of M;
func open_dist_Segment p,r -> Subset of M equals :: SUB_METR:def 8
{ q where q is Element of M : q is_between p,r } ;
coherence
{ q where q is Element of M : q is_between p,r } is Subset of M
proof end;
end;

:: deftheorem defines open_dist_Segment SUB_METR:def 8 :
for M being non empty MetrStruct
for p, r being Element of M holds open_dist_Segment p,r = { q where q is Element of M : q is_between p,r } ;

theorem :: SUB_METR:50
canceled;

theorem :: SUB_METR:51
for M being non empty MetrSpace
for p, r, x being Element of M holds
( x in open_dist_Segment p,r iff x is_between p,r )
proof end;

definition
let M be non empty MetrStruct ;
let p, r be Element of M;
func close_dist_Segment p,r -> Subset of M equals :: SUB_METR:def 9
{ q where q is Element of M : q is_between p,r } \/ {p,r};
coherence
{ q where q is Element of M : q is_between p,r } \/ {p,r} is Subset of M
proof end;
end;

:: deftheorem defines close_dist_Segment SUB_METR:def 9 :
for M being non empty MetrStruct
for p, r being Element of M holds close_dist_Segment p,r = { q where q is Element of M : q is_between p,r } \/ {p,r};

theorem :: SUB_METR:52
canceled;

theorem :: SUB_METR:53
for M being non empty MetrStruct
for 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 ) )
proof end;