:: METRIC_2 semantic presentation

definition
let c1 be non empty MetrStruct ;
let c2, c3 be Element of c1;
pred c2 tolerates c3 means :Def1: :: METRIC_2:def 1
dist a2,a3 = 0;
end;

:: deftheorem Def1 defines tolerates METRIC_2:def 1 :
for b1 being non empty MetrStruct
for b2, b3 being Element of b1 holds
( b2 tolerates b3 iff dist b2,b3 = 0 );

definition
let c1 be non empty Reflexive MetrStruct ;
let c2, c3 be Element of c1;
redefine pred tolerates as c2 tolerates c3;
reflexivity
for b1 being Element of c1 holds b1 tolerates b1
proof end;
end;

definition
let c1 be non empty symmetric MetrStruct ;
let c2, c3 be Element of c1;
redefine pred tolerates as c2 tolerates c3;
symmetry
for b1, b2 being Element of c1 st b1 tolerates b2 holds
b2 tolerates b1
proof end;
end;

definition
let c1 be non empty MetrStruct ;
let c2 be Element of c1;
func c2 -neighbour -> Subset of a1 equals :: METRIC_2:def 2
{ b1 where B is Element of a1 : a2 tolerates b1 } ;
coherence
{ b1 where B is Element of c1 : c2 tolerates b1 } is Subset of c1
proof end;
end;

:: deftheorem Def2 defines -neighbour METRIC_2:def 2 :
for b1 being non empty MetrStruct
for b2 being Element of b1 holds b2 -neighbour = { b3 where B is Element of b1 : b2 tolerates b3 } ;

definition
let c1 be non empty MetrStruct ;
mode equivalence_class of c1 -> Subset of a1 means :Def3: :: METRIC_2:def 3
ex b1 being Element of a1 st a2 = b1 -neighbour ;
existence
ex b1 being Subset of c1ex b2 being Element of c1 st b1 = b2 -neighbour
proof end;
end;

:: deftheorem Def3 defines equivalence_class METRIC_2:def 3 :
for b1 being non empty MetrStruct
for b2 being Subset of b1 holds
( b2 is equivalence_class of b1 iff ex b3 being Element of b1 st b2 = b3 -neighbour );

Lemma3: for b1 being non empty Reflexive MetrStruct
for b2 being Element of b1 holds b2 tolerates b2
;

theorem Th1: :: METRIC_2:1
canceled;

theorem Th2: :: METRIC_2:2
canceled;

theorem Th3: :: METRIC_2:3
canceled;

theorem Th4: :: METRIC_2:4
canceled;

theorem Th5: :: METRIC_2:5
canceled;

theorem Th6: :: METRIC_2:6
for b1 being PseudoMetricSpace
for b2, b3, b4 being Element of b1 st b2 tolerates b3 & b3 tolerates b4 holds
b2 tolerates b4
proof end;

theorem Th7: :: METRIC_2:7
for b1 being PseudoMetricSpace
for b2, b3 being Element of b1 holds
( b3 in b2 -neighbour iff b3 tolerates b2 )
proof end;

theorem Th8: :: METRIC_2:8
for b1 being PseudoMetricSpace
for b2, b3, b4 being Element of b1 st b3 in b2 -neighbour & b4 in b2 -neighbour holds
b3 tolerates b4
proof end;

theorem Th9: :: METRIC_2:9
for b1 being PseudoMetricSpace
for b2 being Element of b1 holds b2 in b2 -neighbour
proof end;

theorem Th10: :: METRIC_2:10
for b1 being PseudoMetricSpace
for b2, b3 being Element of b1 holds
( b2 in b3 -neighbour iff b3 in b2 -neighbour )
proof end;

theorem Th11: :: METRIC_2:11
for b1 being PseudoMetricSpace
for b2, b3, b4 being Element of b1 st b2 in b3 -neighbour & b3 tolerates b4 holds
b2 in b4 -neighbour
proof end;

theorem Th12: :: METRIC_2:12
for b1 being PseudoMetricSpace
for b2, b3 being Element of b1 st b3 in b2 -neighbour holds
b2 -neighbour = b3 -neighbour
proof end;

theorem Th13: :: METRIC_2:13
for b1 being PseudoMetricSpace
for b2, b3 being Element of b1 holds
( b2 -neighbour = b3 -neighbour iff b2 tolerates b3 )
proof end;

theorem Th14: :: METRIC_2:14
for b1 being PseudoMetricSpace
for b2, b3 being Element of b1 holds
( b2 -neighbour meets b3 -neighbour iff b2 tolerates b3 )
proof end;

theorem Th15: :: METRIC_2:15
canceled;

theorem Th16: :: METRIC_2:16
for b1 being PseudoMetricSpace
for b2 being equivalence_class of b1 holds b2 is non empty set
proof end;

registration
let c1 be PseudoMetricSpace;
cluster -> non empty equivalence_class of a1;
coherence
for b1 being equivalence_class of c1 holds not b1 is empty
by Th16;
end;

theorem Th17: :: METRIC_2:17
for b1 being PseudoMetricSpace
for b2, b3, b4 being Element of b1 st b3 in b2 -neighbour & b4 in b2 -neighbour holds
dist b3,b4 = 0
proof end;

theorem Th18: :: METRIC_2:18
for b1 being non empty Reflexive discerning MetrStruct
for b2, b3 being Element of b1 holds
( b2 tolerates b3 iff b2 = b3 )
proof end;

theorem Th19: :: METRIC_2:19
for b1 being non empty MetrSpace
for b2, b3 being Element of b1 holds
( b3 in b2 -neighbour iff b3 = b2 )
proof end;

theorem Th20: :: METRIC_2:20
for b1 being non empty MetrSpace
for b2 being Element of b1 holds b2 -neighbour = {b2}
proof end;

theorem Th21: :: METRIC_2:21
for b1 being non empty MetrSpace
for b2 being Subset of b1 holds
( b2 is equivalence_class of b1 iff ex b3 being Element of b1 st b2 = {b3} )
proof end;

definition
let c1 be non empty MetrStruct ;
func c1 -neighbour -> set equals :: METRIC_2:def 4
{ b1 where B is Subset of a1 : ex b1 being Element of a1 st b2 -neighbour = b1 } ;
coherence
{ b1 where B is Subset of c1 : ex b1 being Element of c1 st b2 -neighbour = b1 } is set
;
end;

:: deftheorem Def4 defines -neighbour METRIC_2:def 4 :
for b1 being non empty MetrStruct holds b1 -neighbour = { b2 where B is Subset of b1 : ex b1 being Element of b1 st b3 -neighbour = b2 } ;

registration
let c1 be non empty MetrStruct ;
cluster a1 -neighbour -> non empty ;
coherence
not c1 -neighbour is empty
proof end;
end;

theorem Th22: :: METRIC_2:22
canceled;

theorem Th23: :: METRIC_2:23
for b1 being set
for b2 being non empty MetrStruct holds
( b1 in b2 -neighbour iff ex b3 being Element of b2 st b1 = b3 -neighbour )
proof end;

theorem Th24: :: METRIC_2:24
for b1 being non empty MetrStruct
for b2 being Element of b1 holds b2 -neighbour in b1 -neighbour ;

theorem Th25: :: METRIC_2:25
canceled;

theorem Th26: :: METRIC_2:26
for b1 being set
for b2 being non empty MetrStruct holds
( b1 in b2 -neighbour iff b1 is equivalence_class of b2 )
proof end;

theorem Th27: :: METRIC_2:27
for b1 being non empty MetrSpace
for b2 being Element of b1 holds {b2} in b1 -neighbour
proof end;

theorem Th28: :: METRIC_2:28
for b1 being set
for b2 being non empty MetrSpace holds
( b1 in b2 -neighbour iff ex b3 being Element of b2 st b1 = {b3} )
proof end;

theorem Th29: :: METRIC_2:29
for b1 being PseudoMetricSpace
for b2, b3 being Element of b1 -neighbour
for b4, b5, b6, b7 being Element of b1 st b4 in b2 & b6 in b3 & b5 in b2 & b7 in b3 holds
dist b4,b6 = dist b5,b7
proof end;

definition
let c1 be non empty MetrStruct ;
let c2, c3 be Element of c1 -neighbour ;
let c4 be Element of REAL ;
pred c2,c3 is_dst c4 means :Def5: :: METRIC_2:def 5
for b1, b2 being Element of a1 st b1 in a2 & b2 in a3 holds
dist b1,b2 = a4;
end;

:: deftheorem Def5 defines is_dst METRIC_2:def 5 :
for b1 being non empty MetrStruct
for b2, b3 being Element of b1 -neighbour
for b4 being Element of REAL holds
( b2,b3 is_dst b4 iff for b5, b6 being Element of b1 st b5 in b2 & b6 in b3 holds
dist b5,b6 = b4 );

theorem Th30: :: METRIC_2:30
canceled;

theorem Th31: :: METRIC_2:31
for b1 being PseudoMetricSpace
for b2, b3 being Element of b1 -neighbour
for b4 being Element of REAL holds
( b2,b3 is_dst b4 iff ex b5, b6 being Element of b1 st
( b5 in b2 & b6 in b3 & dist b5,b6 = b4 ) )
proof end;

theorem Th32: :: METRIC_2:32
for b1 being PseudoMetricSpace
for b2, b3 being Element of b1 -neighbour
for b4 being Element of REAL holds
( b2,b3 is_dst b4 iff b3,b2 is_dst b4 )
proof end;

definition
let c1 be non empty MetrStruct ;
let c2, c3 be Element of c1 -neighbour ;
func ev_eq_1 c2,c3 -> Subset of REAL equals :: METRIC_2:def 6
{ b1 where B is Element of REAL : a2,a3 is_dst b1 } ;
coherence
{ b1 where B is Element of REAL : c2,c3 is_dst b1 } is Subset of REAL
proof end;
end;

:: deftheorem Def6 defines ev_eq_1 METRIC_2:def 6 :
for b1 being non empty MetrStruct
for b2, b3 being Element of b1 -neighbour holds ev_eq_1 b2,b3 = { b4 where B is Element of REAL : b2,b3 is_dst b4 } ;

theorem Th33: :: METRIC_2:33
canceled;

theorem Th34: :: METRIC_2:34
for b1 being PseudoMetricSpace
for b2, b3 being Element of b1 -neighbour
for b4 being Element of REAL holds
( b4 in ev_eq_1 b2,b3 iff b2,b3 is_dst b4 )
proof end;

definition
let c1 be non empty MetrStruct ;
let c2 be Element of REAL ;
func ev_eq_2 c2,c1 -> Subset of [:(a1 -neighbour ),(a1 -neighbour ):] equals :: METRIC_2:def 7
{ b1 where B is Element of [:(a1 -neighbour ),(a1 -neighbour ):] : ex b1, b2 being Element of a1 -neighbour st
( b1 = [b2,b3] & b2,b3 is_dst a2 )
}
;
coherence
{ b1 where B is Element of [:(c1 -neighbour ),(c1 -neighbour ):] : ex b1, b2 being Element of c1 -neighbour st
( b1 = [b2,b3] & b2,b3 is_dst c2 )
}
is Subset of [:(c1 -neighbour ),(c1 -neighbour ):]
proof end;
end;

:: deftheorem Def7 defines ev_eq_2 METRIC_2:def 7 :
for b1 being non empty MetrStruct
for b2 being Element of REAL holds ev_eq_2 b2,b1 = { b3 where B is Element of [:(b1 -neighbour ),(b1 -neighbour ):] : ex b1, b2 being Element of b1 -neighbour st
( b3 = [b4,b5] & b4,b5 is_dst b2 )
}
;

theorem Th35: :: METRIC_2:35
canceled;

theorem Th36: :: METRIC_2:36
for b1 being PseudoMetricSpace
for b2 being Element of REAL
for b3 being Element of [:(b1 -neighbour ),(b1 -neighbour ):] holds
( b3 in ev_eq_2 b2,b1 iff ex b4, b5 being Element of b1 -neighbour st
( b3 = [b4,b5] & b4,b5 is_dst b2 ) )
proof end;

definition
let c1 be non empty MetrStruct ;
func real_in_rel c1 -> Subset of REAL equals :: METRIC_2:def 8
{ b1 where B is Element of REAL : ex b1, b2 being Element of a1 -neighbour st b2,b3 is_dst b1 } ;
coherence
{ b1 where B is Element of REAL : ex b1, b2 being Element of c1 -neighbour st b2,b3 is_dst b1 } is Subset of REAL
proof end;
end;

:: deftheorem Def8 defines real_in_rel METRIC_2:def 8 :
for b1 being non empty MetrStruct holds real_in_rel b1 = { b2 where B is Element of REAL : ex b1, b2 being Element of b1 -neighbour st b3,b4 is_dst b2 } ;

theorem Th37: :: METRIC_2:37
canceled;

theorem Th38: :: METRIC_2:38
for b1 being PseudoMetricSpace
for b2 being Element of REAL holds
( b2 in real_in_rel b1 iff ex b3, b4 being Element of b1 -neighbour st b3,b4 is_dst b2 )
proof end;

definition
let c1 be non empty MetrStruct ;
func elem_in_rel_1 c1 -> Subset of (a1 -neighbour ) equals :: METRIC_2:def 9
{ b1 where B is Element of a1 -neighbour : ex b1 being Element of a1 -neighbour ex b2 being Element of REAL st b1,b2 is_dst b3 } ;
coherence
{ b1 where B is Element of c1 -neighbour : ex b1 being Element of c1 -neighbour ex b2 being Element of REAL st b1,b2 is_dst b3 } is Subset of (c1 -neighbour )
proof end;
end;

:: deftheorem Def9 defines elem_in_rel_1 METRIC_2:def 9 :
for b1 being non empty MetrStruct holds elem_in_rel_1 b1 = { b2 where B is Element of b1 -neighbour : ex b1 being Element of b1 -neighbour ex b2 being Element of REAL st b2,b3 is_dst b4 } ;

theorem Th39: :: METRIC_2:39
canceled;

theorem Th40: :: METRIC_2:40
for b1 being PseudoMetricSpace
for b2 being Element of b1 -neighbour holds
( b2 in elem_in_rel_1 b1 iff ex b3 being Element of b1 -neighbour ex b4 being Element of REAL st b2,b3 is_dst b4 )
proof end;

definition
let c1 be non empty MetrStruct ;
func elem_in_rel_2 c1 -> Subset of (a1 -neighbour ) equals :: METRIC_2:def 10
{ b1 where B is Element of a1 -neighbour : ex b1 being Element of a1 -neighbour ex b2 being Element of REAL st b2,b1 is_dst b3 } ;
coherence
{ b1 where B is Element of c1 -neighbour : ex b1 being Element of c1 -neighbour ex b2 being Element of REAL st b2,b1 is_dst b3 } is Subset of (c1 -neighbour )
proof end;
end;

:: deftheorem Def10 defines elem_in_rel_2 METRIC_2:def 10 :
for b1 being non empty MetrStruct holds elem_in_rel_2 b1 = { b2 where B is Element of b1 -neighbour : ex b1 being Element of b1 -neighbour ex b2 being Element of REAL st b3,b2 is_dst b4 } ;

theorem Th41: :: METRIC_2:41
canceled;

theorem Th42: :: METRIC_2:42
for b1 being PseudoMetricSpace
for b2 being Element of b1 -neighbour holds
( b2 in elem_in_rel_2 b1 iff ex b3 being Element of b1 -neighbour ex b4 being Element of REAL st b3,b2 is_dst b4 )
proof end;

definition
let c1 be non empty MetrStruct ;
func elem_in_rel c1 -> Subset of [:(a1 -neighbour ),(a1 -neighbour ):] equals :: METRIC_2:def 11
{ b1 where B is Element of [:(a1 -neighbour ),(a1 -neighbour ):] : ex b1, b2 being Element of a1 -neighbour ex b3 being Element of REAL st
( b1 = [b2,b3] & b2,b3 is_dst b4 )
}
;
coherence
{ b1 where B is Element of [:(c1 -neighbour ),(c1 -neighbour ):] : ex b1, b2 being Element of c1 -neighbour ex b3 being Element of REAL st
( b1 = [b2,b3] & b2,b3 is_dst b4 )
}
is Subset of [:(c1 -neighbour ),(c1 -neighbour ):]
proof end;
end;

:: deftheorem Def11 defines elem_in_rel METRIC_2:def 11 :
for b1 being non empty MetrStruct holds elem_in_rel b1 = { b2 where B is Element of [:(b1 -neighbour ),(b1 -neighbour ):] : ex b1, b2 being Element of b1 -neighbour ex b3 being Element of REAL st
( b2 = [b3,b4] & b3,b4 is_dst b5 )
}
;

theorem Th43: :: METRIC_2:43
canceled;

theorem Th44: :: METRIC_2:44
for b1 being PseudoMetricSpace
for b2 being Element of [:(b1 -neighbour ),(b1 -neighbour ):] holds
( b2 in elem_in_rel b1 iff ex b3, b4 being Element of b1 -neighbour ex b5 being Element of REAL st
( b2 = [b3,b4] & b3,b4 is_dst b5 ) )
proof end;

definition
let c1 be non empty MetrStruct ;
func set_in_rel c1 -> Subset of [:(a1 -neighbour ),(a1 -neighbour ),REAL :] equals :: METRIC_2:def 12
{ b1 where B is Element of [:(a1 -neighbour ),(a1 -neighbour ),REAL :] : ex b1, b2 being Element of a1 -neighbour ex b3 being Element of REAL st
( b1 = [b2,b3,b4] & b2,b3 is_dst b4 )
}
;
coherence
{ b1 where B is Element of [:(c1 -neighbour ),(c1 -neighbour ),REAL :] : ex b1, b2 being Element of c1 -neighbour ex b3 being Element of REAL st
( b1 = [b2,b3,b4] & b2,b3 is_dst b4 )
}
is Subset of [:(c1 -neighbour ),(c1 -neighbour ),REAL :]
proof end;
end;

:: deftheorem Def12 defines set_in_rel METRIC_2:def 12 :
for b1 being non empty MetrStruct holds set_in_rel b1 = { b2 where B is Element of [:(b1 -neighbour ),(b1 -neighbour ),REAL :] : ex b1, b2 being Element of b1 -neighbour ex b3 being Element of REAL st
( b2 = [b3,b4,b5] & b3,b4 is_dst b5 )
}
;

theorem Th45: :: METRIC_2:45
canceled;

theorem Th46: :: METRIC_2:46
for b1 being PseudoMetricSpace
for b2 being Element of [:(b1 -neighbour ),(b1 -neighbour ),REAL :] holds
( b2 in set_in_rel b1 iff ex b3, b4 being Element of b1 -neighbour ex b5 being Element of REAL st
( b2 = [b3,b4,b5] & b3,b4 is_dst b5 ) )
proof end;

theorem Th47: :: METRIC_2:47
for b1 being PseudoMetricSpace holds elem_in_rel_1 b1 = elem_in_rel_2 b1
proof end;

theorem Th48: :: METRIC_2:48
for b1 being PseudoMetricSpace holds set_in_rel b1 c= [:(elem_in_rel_1 b1),(elem_in_rel_2 b1),(real_in_rel b1):]
proof end;

theorem Th49: :: METRIC_2:49
canceled;

theorem Th50: :: METRIC_2:50
for b1 being PseudoMetricSpace
for b2, b3 being Element of b1 -neighbour
for b4, b5 being Element of REAL st b2,b3 is_dst b4 & b2,b3 is_dst b5 holds
b4 = b5
proof end;

theorem Th51: :: METRIC_2:51
canceled;

theorem Th52: :: METRIC_2:52
for b1 being PseudoMetricSpace
for b2, b3 being Element of b1 -neighbour ex b4 being Element of REAL st b2,b3 is_dst b4
proof end;

definition
let c1 be PseudoMetricSpace;
func nbourdist c1 -> Function of [:(a1 -neighbour ),(a1 -neighbour ):], REAL means :Def13: :: METRIC_2:def 13
for b1, b2 being Element of a1 -neighbour
for b3, b4 being Element of a1 st b3 in b1 & b4 in b2 holds
a2 . b1,b2 = dist b3,b4;
existence
ex b1 being Function of [:(c1 -neighbour ),(c1 -neighbour ):], REAL st
for b2, b3 being Element of c1 -neighbour
for b4, b5 being Element of c1 st b4 in b2 & b5 in b3 holds
b1 . b2,b3 = dist b4,b5
proof end;
uniqueness
for b1, b2 being Function of [:(c1 -neighbour ),(c1 -neighbour ):], REAL st ( for b3, b4 being Element of c1 -neighbour
for b5, b6 being Element of c1 st b5 in b3 & b6 in b4 holds
b1 . b3,b4 = dist b5,b6 ) & ( for b3, b4 being Element of c1 -neighbour
for b5, b6 being Element of c1 st b5 in b3 & b6 in b4 holds
b2 . b3,b4 = dist b5,b6 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines nbourdist METRIC_2:def 13 :
for b1 being PseudoMetricSpace
for b2 being Function of [:(b1 -neighbour ),(b1 -neighbour ):], REAL holds
( b2 = nbourdist b1 iff for b3, b4 being Element of b1 -neighbour
for b5, b6 being Element of b1 st b5 in b3 & b6 in b4 holds
b2 . b3,b4 = dist b5,b6 );

theorem Th53: :: METRIC_2:53
canceled;

theorem Th54: :: METRIC_2:54
for b1 being PseudoMetricSpace
for b2, b3 being Element of b1 -neighbour holds
( (nbourdist b1) . b2,b3 = 0 iff b2 = b3 )
proof end;

theorem Th55: :: METRIC_2:55
for b1 being PseudoMetricSpace
for b2, b3 being Element of b1 -neighbour holds (nbourdist b1) . b2,b3 = (nbourdist b1) . b3,b2
proof end;

theorem Th56: :: METRIC_2:56
for b1 being PseudoMetricSpace
for b2, b3, b4 being Element of b1 -neighbour holds (nbourdist b1) . b2,b4 <= ((nbourdist b1) . b2,b3) + ((nbourdist b1) . b3,b4)
proof end;

definition
let c1 be PseudoMetricSpace;
func Eq_classMetricSpace c1 -> MetrSpace equals :: METRIC_2:def 14
MetrStruct(# (a1 -neighbour ),(nbourdist a1) #);
coherence
MetrStruct(# (c1 -neighbour ),(nbourdist c1) #) is MetrSpace
proof end;
end;

:: deftheorem Def14 defines Eq_classMetricSpace METRIC_2:def 14 :
for b1 being PseudoMetricSpace holds Eq_classMetricSpace b1 = MetrStruct(# (b1 -neighbour ),(nbourdist b1) #);

registration
let c1 be PseudoMetricSpace;
cluster Eq_classMetricSpace a1 -> non empty strict ;
coherence
( Eq_classMetricSpace c1 is strict & not Eq_classMetricSpace c1 is empty )
;
end;