:: On Pseudometric Spaces
:: by Adam Lecko and Mariusz Startek
::
:: Received September 28, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

definition
let M be non empty MetrStruct ;
let x, y be Element of M;
predx tolerates y means :Def1: :: METRIC_2:def 1
 dist (x,y) = 0 ;
end;

:: deftheorem Def1 defines tolerates METRIC_2:def_1_:_
 for M being non empty MetrStruct
for x, y being Element of M holds
( x tolerates y iff dist (x,y) = 0 );

definition
let M be non empty Reflexive MetrStruct ;
let x, y be Element of M;
:: original:tolerates
redefine predx tolerates y;
reflexivity
 for x being Element of M holds (M,b1,b1)
proofend;
end;

definition
let M be non empty symmetric MetrStruct ;
let x, y be Element of M;
:: original:tolerates
redefine predx tolerates y;
symmetry
 for x, y being Element of M st (M,b1,b2) holds
(M,b2,b1)
proofend;
end;

definition
let M be non empty MetrStruct ;
let x be Element of M;
funcx -neighbour  ->  Subset of M equals :: METRIC_2:def 2
 {  y where y is Element of M : x tolerates y  }  ;
coherence
  {  y where y is Element of M : x tolerates y  }  is Subset of M
proofend;
end;

:: deftheorem  defines -neighbour METRIC_2:def_2_:_
 for M being non empty MetrStruct
for x being Element of M holds x -neighbour =  {  y where y is Element of M : x tolerates y  }  ;

definition
let M be non empty MetrStruct ;
mode equivalence_class of M ->  Subset of M means :Def3: :: METRIC_2:def 3
 ex x being Element of M st it = x -neighbour ;
existence
 ex b1 being Subset of M ex x being Element of M st b1 = x -neighbour
proofend;
end;

:: deftheorem Def3 defines equivalence_class METRIC_2:def_3_:_
 for M being non empty MetrStruct
for b2 being Subset of M holds
( b2 is equivalence_class of M iff ex x being Element of M st b2 = x -neighbour );

Lm1:  for M being non empty Reflexive MetrStruct
for x being Element of M holds x tolerates x
;

theorem Th1: :: METRIC_2:1
for M being PseudoMetricSpace
for x, y, z being Element of M st x tolerates y & y tolerates z holds
x tolerates z
proofend;

theorem Th2: :: METRIC_2:2
for M being PseudoMetricSpace
for x, y being Element of M holds
( y in x -neighbour iff y tolerates x )
proofend;

theorem :: METRIC_2:3
for M being PseudoMetricSpace
for x, p, q being Element of M st p in x -neighbour & q in x -neighbour holds
p tolerates q
proofend;

theorem Th4: :: METRIC_2:4
for M being PseudoMetricSpace
for x being Element of M holds x in x -neighbour
proofend;

theorem :: METRIC_2:5
for M being PseudoMetricSpace
for x, y being Element of M st x in y -neighbour holds
y in x -neighbour
proofend;

theorem :: METRIC_2:6
for M being PseudoMetricSpace
for p, x, y being Element of M st p in x -neighbour & x tolerates y holds
p in y -neighbour
proofend;

theorem Th7: :: METRIC_2:7
for M being PseudoMetricSpace
for x, y being Element of M st y in x -neighbour holds
x -neighbour = y -neighbour
proofend;

theorem Th8: :: METRIC_2:8
for M being PseudoMetricSpace
for x, y being Element of M holds
( x -neighbour = y -neighbour iff x tolerates y )
proofend;

theorem :: METRIC_2:9
for M being PseudoMetricSpace
for x, y being Element of M holds
( x -neighbour meets y -neighbour iff x tolerates y )
proofend;

Lm2:  for M being PseudoMetricSpace
for V being equivalence_class of M holds V is non empty set
proofend;

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

theorem Th10: :: METRIC_2:10
for M being PseudoMetricSpace
for x, p, q being Element of M st p in x -neighbour & q in x -neighbour holds
dist (p,q) = 0
proofend;

theorem Th11: :: METRIC_2:11
for M being non empty Reflexive discerning MetrStruct
for x, y being Element of M holds
( x tolerates y iff x = y )
proofend;

theorem Th12: :: METRIC_2:12
for M being non empty MetrSpace
for x, y being Element of M holds
( y in x -neighbour iff y = x )
proofend;

theorem Th13: :: METRIC_2:13
for M being non empty MetrSpace
for x being Element of M holds x -neighbour = {x}
proofend;

theorem :: METRIC_2:14
for M being non empty MetrSpace
for V being Subset of M holds
( V is equivalence_class of M iff ex x being Element of M st V = {x} )
proofend;

:: Set of the equivalence classes
definition
let M be non empty MetrStruct ;
funcM -neighbour  ->  set  equals :: METRIC_2:def 4
 {  s where s is Subset of M : ex x being Element of M st x -neighbour = s  }  ;
coherence
  {  s where s is Subset of M : ex x being Element of M st x -neighbour = s  }  is set ;
end;

:: deftheorem  defines -neighbour METRIC_2:def_4_:_
 for M being non empty MetrStruct holds M -neighbour =  {  s where s is Subset of M : ex x being Element of M st x -neighbour = s  }  ;

registration
let M be non empty MetrStruct ;
clusterM -neighbour  ->  non empty ;
coherence
 not M -neighbour is empty
proofend;
end;

theorem Th15: :: METRIC_2:15
for V being set
for M being non empty MetrStruct holds
( V in M -neighbour iff ex x being Element of M st V = x -neighbour )
proofend;

theorem :: METRIC_2:16
for M being non empty MetrStruct
for x being Element of M holds x -neighbour in M -neighbour ;

theorem Th17: :: METRIC_2:17
for V being set
for M being non empty MetrStruct holds
( V in M -neighbour iff V is equivalence_class of M )
proofend;

theorem :: METRIC_2:18
for M being non empty MetrSpace
for x being Element of M holds {x} in M -neighbour
proofend;

theorem :: METRIC_2:19
for V being set
for M being non empty MetrSpace holds
( V in M -neighbour iff ex x being Element of M st V = {x} )
proofend;

theorem Th20: :: METRIC_2:20
for M being PseudoMetricSpace
for V, Q being Element of M -neighbour
for p1, p2, q1, q2 being Element of M st p1 in V & q1 in Q & p2 in V & q2 in Q holds
dist (p1,q1) = dist (p2,q2)
proofend;

definition
let M be non empty MetrStruct ;
let V, Q be Element of M -neighbour ;
let v be Element of REAL ;
predV,Q is_dst v means :Def5: :: METRIC_2:def 5
 for p, q being Element of M st p in V & q in Q holds
dist (p,q) = v;
end;

:: deftheorem Def5 defines is_dst METRIC_2:def_5_:_
 for M being non empty MetrStruct
for V, Q being Element of M -neighbour
for v being Element of REAL holds
( V,Q is_dst v iff for p, q being Element of M st p in V & q in Q holds
dist (p,q) = v );

theorem Th21: :: METRIC_2:21
for M being PseudoMetricSpace
for V, Q being Element of M -neighbour
for v being Element of REAL holds
( V,Q is_dst v iff ex p, q being Element of M st
( p in V & q in Q & dist (p,q) = v ) )
proofend;

theorem Th22: :: METRIC_2:22
for M being PseudoMetricSpace
for V, Q being Element of M -neighbour
for v being Element of REAL st V,Q is_dst v holds
Q,V is_dst v
proofend;

definition
let M be non empty MetrStruct ;
let V, Q be Element of M -neighbour ;
func ev_eq_1 (V,Q) ->  Subset of REAL equals :: METRIC_2:def 6
 {  v where v is Element of REAL : V,Q is_dst v  }  ;
coherence
  {  v where v is Element of REAL : V,Q is_dst v  }  is Subset of REAL
proofend;
end;

:: deftheorem  defines ev_eq_1 METRIC_2:def_6_:_
 for M being non empty MetrStruct
for V, Q being Element of M -neighbour holds ev_eq_1 (V,Q) =  {  v where v is Element of REAL : V,Q is_dst v  }  ;

theorem :: METRIC_2:23
for M being PseudoMetricSpace
for V, Q being Element of M -neighbour
for v being Element of REAL holds
( v in ev_eq_1 (V,Q) iff V,Q is_dst v )
proofend;

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):]
proofend;
end;

:: deftheorem  defines ev_eq_2 METRIC_2:def_7_:_
 for M being non empty MetrStruct
for v being Element of REAL holds ev_eq_2 (v,M) =  {  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 )  }  ;

theorem :: METRIC_2:24
for M being PseudoMetricSpace
for v being Element of REAL
for W being Element of [:(M -neighbour),(M -neighbour):] holds
( W in ev_eq_2 (v,M) iff ex V, Q being Element of M -neighbour st
( W = [V,Q] & V,Q is_dst v ) )
proofend;

definition
let M be non empty MetrStruct ;
func real_in_rel M ->  Subset of REAL equals :: METRIC_2:def 8
 {  v where v is Element of REAL : ex V, Q being Element of M -neighbour st V,Q is_dst v  }  ;
coherence
  {  v where v is Element of REAL : ex V, Q being Element of M -neighbour st V,Q is_dst v  }  is Subset of REAL
proofend;
end;

:: deftheorem  defines real_in_rel METRIC_2:def_8_:_
 for M being non empty MetrStruct holds real_in_rel M =  {  v where v is Element of REAL : ex V, Q being Element of M -neighbour st V,Q is_dst v  }  ;

theorem :: METRIC_2:25
for M being PseudoMetricSpace
for v being Element of REAL holds
( v in real_in_rel M iff ex V, Q being Element of M -neighbour st V,Q is_dst v )
proofend;

definition
let M be non empty MetrStruct ;
func elem_in_rel_1 M ->  Subset of (M -neighbour) equals :: METRIC_2:def 9
 {  V where V is Element of M -neighbour : ex Q being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v  }  ;
coherence
  {  V where V is Element of M -neighbour : ex Q being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v  }  is Subset of (M -neighbour)
proofend;
end;

:: deftheorem  defines elem_in_rel_1 METRIC_2:def_9_:_
 for M being non empty MetrStruct holds elem_in_rel_1 M =  {  V where V is Element of M -neighbour : ex Q being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v  }  ;

theorem Th26: :: METRIC_2:26
for M being PseudoMetricSpace
for V being Element of M -neighbour holds
( V in elem_in_rel_1 M iff ex Q being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v )
proofend;

definition
let M be non empty MetrStruct ;
func elem_in_rel_2 M ->  Subset of (M -neighbour) equals :: METRIC_2:def 10
 {  Q where Q is Element of M -neighbour : ex V being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v  }  ;
coherence
  {  Q where Q is Element of M -neighbour : ex V being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v  }  is Subset of (M -neighbour)
proofend;
end;

:: deftheorem  defines elem_in_rel_2 METRIC_2:def_10_:_
 for M being non empty MetrStruct holds elem_in_rel_2 M =  {  Q where Q is Element of M -neighbour : ex V being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v  }  ;

theorem Th27: :: METRIC_2:27
for M being PseudoMetricSpace
for Q being Element of M -neighbour holds
( Q in elem_in_rel_2 M iff ex V being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v )
proofend;

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):]
proofend;
end;

:: deftheorem  defines elem_in_rel METRIC_2:def_11_:_
 for M being non empty MetrStruct holds elem_in_rel M =  {  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 )  }  ;

theorem :: METRIC_2:28
for M being PseudoMetricSpace
for VQ being Element of [:(M -neighbour),(M -neighbour):] holds
( VQ in elem_in_rel M iff ex V, Q being Element of M -neighbour ex v being Element of REAL st
( VQ = [V,Q] & V,Q is_dst v ) )
proofend;

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:]
proofend;
end;

:: deftheorem  defines set_in_rel METRIC_2:def_12_:_
 for M being non empty MetrStruct holds set_in_rel M =  {  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 )  }  ;

theorem Th29: :: METRIC_2:29
for M being PseudoMetricSpace
for VQv being Element of [:(M -neighbour),(M -neighbour),REAL:] holds
( VQv in set_in_rel M iff ex V, Q being Element of M -neighbour ex v being Element of REAL st
( VQv = [V,Q,v] & V,Q is_dst v ) )
proofend;

theorem :: METRIC_2:30
for M being PseudoMetricSpace holds elem_in_rel_1 M = elem_in_rel_2 M
proofend;

theorem :: METRIC_2:31
for M being PseudoMetricSpace holds set_in_rel M c= [:(elem_in_rel_1 M),(elem_in_rel_2 M),(real_in_rel M):]
proofend;

theorem :: METRIC_2:32
for M being PseudoMetricSpace
for V, Q being Element of M -neighbour
for v1, v2 being Element of REAL st V,Q is_dst v1 & V,Q is_dst v2 holds
v1 = v2
proofend;

theorem Th33: :: METRIC_2:33
for M being PseudoMetricSpace
for V, Q being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v
proofend;

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)
proofend;
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
proofend;
end;

:: deftheorem Def13 defines nbourdist METRIC_2:def_13_:_
 for M being PseudoMetricSpace
for b2 being Function of [:(M -neighbour),(M -neighbour):],REAL holds
( b2 = nbourdist M iff 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) );

theorem Th34: :: METRIC_2:34
for M being PseudoMetricSpace
for V, Q being Element of M -neighbour holds
( (nbourdist M) . (V,Q) = 0 iff V = Q )
proofend;

theorem Th35: :: METRIC_2:35
for M being PseudoMetricSpace
for V, Q being Element of M -neighbour holds (nbourdist M) . (V,Q) = (nbourdist M) . (Q,V)
proofend;

theorem Th36: :: METRIC_2:36
for M being PseudoMetricSpace
for V, Q, W being Element of M -neighbour holds (nbourdist M) . (V,W) <= ((nbourdist M) . (V,Q)) + ((nbourdist M) . (Q,W))
proofend;

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

:: deftheorem  defines Eq_classMetricSpace METRIC_2:def_14_:_
 for M being PseudoMetricSpace holds Eq_classMetricSpace M = MetrStruct(# (M -neighbour),(nbourdist M) #);

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