:: SUB_METR semantic presentation

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;

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

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

theorem :: SUB_METR:3

canceled;

theorem Th4: :: SUB_METR:4

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

proof end;

theorem Th5: :: SUB_METR:5

for x, y being Element of {{} } st x <> y holds
0 < Empty^2-to-zero . x,y

proof end;

theorem Th6: :: SUB_METR:6

for x, y being Element of {{} } 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 {{} } 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 {{} } 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(# {{} },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 :

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 :

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(# {{} },Empty^2-to-zero #) -> Reflexive symmetric triangle Discerning ;
coherence

proof end;

end;

registration

cluster non empty Reflexive symmetric triangle Discerning MetrStruct ;
existence

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;

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;

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 :

:: deftheorem Def4 defines ultra SUB_METR:def 4 :

registration

cluster non empty strict Reflexive symmetric Discerning ultra MetrStruct ;
existence

proof end;

end;

definition

mode UltraMetricSpace is non empty Reflexive symmetric Discerning ultra MetrStruct ;

end;

registration

cluster non empty -> non empty Discerning MetrStruct ;
coherence

proof end;

end;

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;

registration

cluster -> discerning triangle MetrStruct ;
coherence

proof end;

end;

definition

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

proof end;

end;

:: deftheorem defines Set_to_zero SUB_METR:def 5 :

theorem :: SUB_METR:39

( [{} ,{} ] in [:{{} ,{{} }},{{} ,{{} }}:] & [{} ,{{} }] in [:{{} ,{{} }},{{} ,{{} }}:] & [{{} },{} ] in [:{{} ,{{} }},{{} ,{{} }}:] & [{{} },{{} }] in [:{{} ,{{} }},{{} ,{{} }}:] )

proof end;

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 ;

end;

:: deftheorem defines ZeroSpace SUB_METR:def 6 :

registration

cluster ZeroSpace -> non empty strict ;
coherence ;

end;

registration

cluster ZeroSpace -> non empty strict Reflexive symmetric triangle ;
coherence

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 :

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

proof end;

end;

:: deftheorem defines open_dist_Segment SUB_METR:def 8 :

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

proof end;

end;

:: deftheorem defines close_dist_Segment SUB_METR:def 9 :

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;

theorem :: SUB_METR:54

for M being non empty MetrStruct
for p, r being Element of M holds open_dist_Segment p,r c= close_dist_Segment p,r by XBOOLE_1:7;