:: SUB_METR semantic presentation

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

theorem Th2: :: SUB_METR:2
for b1 being MetrSpace
for b2, b3 being Element of b1 st b2 <> b3 holds
0 < dist b2,b3
proof end;

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

E4: Empty^2-to-zero . {} ,{} = Empty^2-to-zero . [{} ,{} ]
.= 0 by Lemma3, FUNCOP_1:13, METRIC_1:def 2 ;

theorem Th3: :: SUB_METR:3
canceled;

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

theorem Th5: :: SUB_METR:5
for b1, b2 being Element of {{} } st b1 <> b2 holds
0 < Empty^2-to-zero . b1,b2
proof end;

theorem Th6: :: SUB_METR:6
for b1, b2 being Element of {{} } holds Empty^2-to-zero . b1,b2 = Empty^2-to-zero . b2,b1
proof end;

theorem Th7: :: SUB_METR:7
for b1, b2, b3 being Element of {{} } holds Empty^2-to-zero . b1,b3 <= (Empty^2-to-zero . b1,b2) + (Empty^2-to-zero . b2,b3)
proof end;

theorem Th8: :: SUB_METR:8
for b1, b2, b3 being Element of {{} } holds Empty^2-to-zero . b1,b3 <= max (Empty^2-to-zero . b1,b2),(Empty^2-to-zero . b2,b3)
proof end;

set c1 = MetrStruct(# {{} },Empty^2-to-zero #);

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

definition
let c2 be non empty set ;
let c3 be Function of [:c2,c2:], REAL ;
attr a2 is Discerning means :Def1: :: SUB_METR:def 1
for b1, b2 being Element of a1 st b1 <> b2 holds
0 < a2 . b1,b2;
end;

:: deftheorem Def1 defines Discerning SUB_METR:def 1 :
for b1 being non empty set
for b2 being Function of [:b1,b1:], REAL holds
( b2 is Discerning iff for b3, b4 being Element of b1 st b3 <> b4 holds
0 < b2 . b3,b4 );

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

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

theorem Th9: :: SUB_METR:9
canceled;

theorem Th10: :: SUB_METR:10
canceled;

theorem Th11: :: SUB_METR:11
canceled;

theorem Th12: :: SUB_METR:12
canceled;

theorem Th13: :: SUB_METR:13
canceled;

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

registration
cluster MetrStruct(# {{} },Empty^2-to-zero #) -> Reflexive symmetric triangle Discerning ;
coherence
( MetrStruct(# {{} },Empty^2-to-zero #) is Reflexive & MetrStruct(# {{} },Empty^2-to-zero #) is symmetric & MetrStruct(# {{} },Empty^2-to-zero #) is Discerning & MetrStruct(# {{} },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 Th15: :: SUB_METR:15
canceled;

theorem Th16: :: SUB_METR:16
canceled;

theorem Th17: :: SUB_METR:17
canceled;

theorem Th18: :: SUB_METR:18
for b1 being non empty Reflexive Discerning MetrStruct
for b2, b3 being Element of b1 holds 0 <= dist b2,b3
proof end;

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

theorem Th19: :: SUB_METR:19
canceled;

theorem Th20: :: SUB_METR:20
canceled;

theorem Th21: :: SUB_METR:21
canceled;

theorem Th22: :: SUB_METR:22
canceled;

theorem Th23: :: SUB_METR:23
canceled;

theorem Th24: :: SUB_METR:24
canceled;

theorem Th25: :: SUB_METR:25
canceled;

definition
let c2 be non empty MetrStruct ;
canceled;
attr a1 is ultra means :Def4: :: SUB_METR:def 4
for b1, b2, b3 being Element of a1 holds dist b1,b3 <= max (dist b1,b2),(dist b2,b3);
end;

:: deftheorem Def3 SUB_METR:def 3 :
canceled;

:: deftheorem Def4 defines ultra SUB_METR:def 4 :
for b1 being non empty MetrStruct holds
( b1 is ultra iff for b2, b3, b4 being Element of b1 holds dist b2,b4 <= max (dist b2,b3),(dist b3,b4) );

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;

theorem Th26: :: SUB_METR:26
canceled;

theorem Th27: :: SUB_METR:27
canceled;

theorem Th28: :: SUB_METR:28
canceled;

theorem Th29: :: SUB_METR:29
canceled;

theorem Th30: :: SUB_METR:30
canceled;

theorem Th31: :: SUB_METR:31
canceled;

theorem Th32: :: SUB_METR:32
canceled;

theorem Th33: :: SUB_METR:33
canceled;

theorem Th34: :: SUB_METR:34
canceled;

theorem Th35: :: SUB_METR:35
canceled;

theorem Th36: :: SUB_METR:36
canceled;

theorem Th37: :: SUB_METR:37
canceled;

theorem Th38: :: SUB_METR:38
canceled;

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

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

theorem Th39: :: SUB_METR:39
( [{} ,{} ] in [:{{} ,{{} }},{{} ,{{} }}:] & [{} ,{{} }] in [:{{} ,{{} }},{{} ,{{} }}:] & [{{} },{} ] in [:{{} ,{{} }},{{} ,{{} }}:] & [{{} },{{} }] in [:{{} ,{{} }},{{} ,{{} }}:] )
proof end;

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

theorem Th41: :: SUB_METR:41
canceled;

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

theorem Th43: :: SUB_METR:43
for b1, b2, b3 being Element of {{} ,{{} }} holds Set_to_zero . b1,b3 <= (Set_to_zero . b1,b2) + (Set_to_zero . b2,b3)
proof end;

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

:: deftheorem Def6 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 -> non empty strict Reflexive symmetric triangle ;
coherence
( ZeroSpace is Reflexive & ZeroSpace is symmetric & ZeroSpace is triangle )
proof end;
end;

definition
let c2 be MetrStruct ;
let c3, c4, c5 be Element of c2;
pred c3 is_between c2,c4 means :Def7: :: SUB_METR:def 7
( a2 <> a3 & a2 <> a4 & a3 <> a4 & dist a2,a4 = (dist a2,a3) + (dist a3,a4) );
end;

:: deftheorem Def7 defines is_between SUB_METR:def 7 :
for b1 being MetrStruct
for b2, b3, b4 being Element of b1 holds
( b3 is_between b2,b4 iff ( b2 <> b3 & b2 <> b4 & b3 <> b4 & dist b2,b4 = (dist b2,b3) + (dist b3,b4) ) );

theorem Th44: :: SUB_METR:44
canceled;

theorem Th45: :: SUB_METR:45
canceled;

theorem Th46: :: SUB_METR:46
canceled;

theorem Th47: :: SUB_METR:47
for b1 being non empty Reflexive symmetric triangle MetrStruct
for b2, b3, b4 being Element of b1 st b3 is_between b2,b4 holds
b3 is_between b4,b2
proof end;

theorem Th48: :: SUB_METR:48
for b1 being MetrSpace
for b2, b3, b4 being Element of b1 st b3 is_between b2,b4 holds
( not b2 is_between b3,b4 & not b4 is_between b2,b3 )
proof end;

theorem Th49: :: SUB_METR:49
for b1 being MetrSpace
for b2, b3, b4, b5 being Element of b1 st b3 is_between b2,b4 & b4 is_between b2,b5 holds
( b3 is_between b2,b5 & b4 is_between b3,b5 )
proof end;

definition
let c2 be non empty MetrStruct ;
let c3, c4 be Element of c2;
func open_dist_Segment c2,c3 -> Subset of a1 equals :: SUB_METR:def 8
{ b1 where B is Element of a1 : b1 is_between a2,a3 } ;
coherence
{ b1 where B is Element of c2 : b1 is_between c3,c4 } is Subset of c2
proof end;
end;

:: deftheorem Def8 defines open_dist_Segment SUB_METR:def 8 :
for b1 being non empty MetrStruct
for b2, b3 being Element of b1 holds open_dist_Segment b2,b3 = { b4 where B is Element of b1 : b4 is_between b2,b3 } ;

theorem Th50: :: SUB_METR:50
canceled;

theorem Th51: :: SUB_METR:51
for b1 being non empty MetrSpace
for b2, b3, b4 being Element of b1 holds
( b4 in open_dist_Segment b2,b3 iff b4 is_between b2,b3 )
proof end;

definition
let c2 be non empty MetrStruct ;
let c3, c4 be Element of c2;
func close_dist_Segment c2,c3 -> Subset of a1 equals :: SUB_METR:def 9
{ b1 where B is Element of a1 : b1 is_between a2,a3 } \/ {a2,a3};
coherence
{ b1 where B is Element of c2 : b1 is_between c3,c4 } \/ {c3,c4} is Subset of c2
proof end;
end;

:: deftheorem Def9 defines close_dist_Segment SUB_METR:def 9 :
for b1 being non empty MetrStruct
for b2, b3 being Element of b1 holds close_dist_Segment b2,b3 = { b4 where B is Element of b1 : b4 is_between b2,b3 } \/ {b2,b3};

theorem Th52: :: SUB_METR:52
canceled;

theorem Th53: :: SUB_METR:53
for b1 being non empty MetrStruct
for b2, b3, b4 being Element of b1 holds
( b4 in close_dist_Segment b2,b3 iff ( b4 is_between b2,b3 or b4 = b2 or b4 = b3 ) )
proof end;

theorem Th54: :: SUB_METR:54
for b1 being non empty MetrStruct
for b2, b3 being Element of b1 holds open_dist_Segment b2,b3 c= close_dist_Segment b2,b3 by XBOOLE_1:7;