:: On Pseudometric Spaces
:: by Adam Lecko and Mariusz Startek
::
:: Received September 28, 1990
:: Copyright (c) 1990 Association of Mizar Users
:: deftheorem Def1 defines tolerates METRIC_2:def 1 :
:: deftheorem defines -neighbour METRIC_2:def 2 :
:: deftheorem Def3 defines equivalence_class METRIC_2:def 3 :
Lm1:
for M being non empty Reflexive MetrStruct
for x being Element of M holds x tolerates x
;
theorem :: METRIC_2:1
canceled;
theorem :: METRIC_2:2
canceled;
theorem :: METRIC_2:3
canceled;
theorem :: METRIC_2:4
canceled;
theorem :: METRIC_2:5
canceled;
theorem Th6: :: METRIC_2:6
theorem Th7: :: METRIC_2:7
theorem :: METRIC_2:8
theorem Th9: :: METRIC_2:9
theorem :: METRIC_2:10
theorem :: METRIC_2:11
theorem Th12: :: METRIC_2:12
theorem Th13: :: METRIC_2:13
theorem :: METRIC_2:14
theorem :: METRIC_2:15
canceled;
theorem Th16: :: METRIC_2:16
theorem Th17: :: METRIC_2:17
theorem Th18: :: METRIC_2:18
theorem Th19: :: METRIC_2:19
theorem Th20: :: METRIC_2:20
theorem :: METRIC_2:21
:: deftheorem defines -neighbour METRIC_2:def 4 :
theorem :: METRIC_2:22
canceled;
theorem Th23: :: METRIC_2:23
theorem :: METRIC_2:24
theorem :: METRIC_2:25
canceled;
theorem Th26: :: METRIC_2:26
theorem :: METRIC_2:27
theorem :: METRIC_2:28
theorem Th29: :: METRIC_2:29
:: deftheorem Def5 defines is_dst METRIC_2:def 5 :
theorem :: METRIC_2:30
canceled;
theorem Th31: :: METRIC_2:31
theorem Th32: :: METRIC_2:32
:: deftheorem defines ev_eq_1 METRIC_2:def 6 :
theorem :: METRIC_2:33
canceled;
theorem :: METRIC_2:34
definition
let M be non
empty MetrStruct ;
let v be
Element of
REAL ;
func ev_eq_2 v,
M -> Subset of
[:(M -neighbour ),(M -neighbour ):] equals :: METRIC_2:def 7
{ W where W is Element of [:(M -neighbour ),(M -neighbour ):] : ex V, Q being Element of M -neighbour st
( W = [V,Q] & V,Q is_dst v ) } ;
coherence
{ W where W is Element of [:(M -neighbour ),(M -neighbour ):] : ex V, Q being Element of M -neighbour st
( W = [V,Q] & V,Q is_dst v ) } is Subset of [:(M -neighbour ),(M -neighbour ):]
end;
:: deftheorem defines ev_eq_2 METRIC_2:def 7 :
theorem :: METRIC_2:35
canceled;
theorem :: METRIC_2:36
:: deftheorem defines real_in_rel METRIC_2:def 8 :
theorem :: METRIC_2:37
canceled;
theorem :: METRIC_2:38
:: deftheorem defines elem_in_rel_1 METRIC_2:def 9 :
theorem :: METRIC_2:39
canceled;
theorem Th40: :: METRIC_2:40
:: deftheorem defines elem_in_rel_2 METRIC_2:def 10 :
theorem :: METRIC_2:41
canceled;
theorem Th42: :: METRIC_2:42
definition
let M be non
empty MetrStruct ;
func elem_in_rel M -> Subset of
[:(M -neighbour ),(M -neighbour ):] equals :: METRIC_2:def 11
{ VQ where VQ is Element of [:(M -neighbour ),(M -neighbour ):] : ex V, Q being Element of M -neighbour ex v being Element of REAL st
( VQ = [V,Q] & V,Q is_dst v ) } ;
coherence
{ VQ where VQ is Element of [:(M -neighbour ),(M -neighbour ):] : ex V, Q being Element of M -neighbour ex v being Element of REAL st
( VQ = [V,Q] & V,Q is_dst v ) } is Subset of [:(M -neighbour ),(M -neighbour ):]
end;
:: deftheorem defines elem_in_rel METRIC_2:def 11 :
theorem :: METRIC_2:43
canceled;
theorem :: METRIC_2:44
definition
let M be non
empty MetrStruct ;
func set_in_rel M -> Subset of
[:(M -neighbour ),(M -neighbour ),REAL :] equals :: METRIC_2:def 12
{ VQv where VQv is Element of [:(M -neighbour ),(M -neighbour ),REAL :] : ex V, Q being Element of M -neighbour ex v being Element of REAL st
( VQv = [V,Q,v] & V,Q is_dst v ) } ;
coherence
{ VQv where VQv is Element of [:(M -neighbour ),(M -neighbour ),REAL :] : ex V, Q being Element of M -neighbour ex v being Element of REAL st
( VQv = [V,Q,v] & V,Q is_dst v ) } is Subset of [:(M -neighbour ),(M -neighbour ),REAL :]
end;
:: deftheorem defines set_in_rel METRIC_2:def 12 :
theorem :: METRIC_2:45
canceled;
theorem Th46: :: METRIC_2:46
theorem :: METRIC_2:47
theorem :: METRIC_2:48
theorem :: METRIC_2:49
canceled;
theorem :: METRIC_2:50
theorem :: METRIC_2:51
canceled;
theorem Th52: :: METRIC_2:52
definition
let M be
PseudoMetricSpace;
func nbourdist M -> Function of
[:(M -neighbour ),(M -neighbour ):],
REAL means :
Def13:
:: METRIC_2:def 13
for
V,
Q being
Element of
M -neighbour for
p,
q being
Element of
M st
p in V &
q in Q holds
it . V,
Q = dist p,
q;
existence
ex b1 being Function of [:(M -neighbour ),(M -neighbour ):], REAL st
for V, Q being Element of M -neighbour
for p, q being Element of M st p in V & q in Q holds
b1 . V,Q = dist p,q
uniqueness
for b1, b2 being Function of [:(M -neighbour ),(M -neighbour ):], REAL st ( for V, Q being Element of M -neighbour
for p, q being Element of M st p in V & q in Q holds
b1 . V,Q = dist p,q ) & ( for V, Q being Element of M -neighbour
for p, q being Element of M st p in V & q in Q holds
b2 . V,Q = dist p,q ) holds
b1 = b2
end;
:: deftheorem Def13 defines nbourdist METRIC_2:def 13 :
theorem :: METRIC_2:53
canceled;
theorem Th54: :: METRIC_2:54
theorem Th55: :: METRIC_2:55
theorem Th56: :: METRIC_2:56
:: deftheorem defines Eq_classMetricSpace METRIC_2:def 14 :