:: by Adam Lecko and Mariusz Startek

::

:: Received September 28, 1990

:: Copyright (c) 1990-2021 Association of Mizar Users

:: deftheorem 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 );

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 pred x tolerates y;

reflexivity

for x being Element of M holds (M,b_{1},b_{1})
by METRIC_1:1;

end;
let x, y be Element of M;

:: original: tolerates

redefine pred x tolerates y;

reflexivity

for x being Element of M holds (M,b

definition

let M be non empty symmetric MetrStruct ;

let x, y be Element of M;

:: original: tolerates

redefine pred x tolerates y;

symmetry

for x, y being Element of M st (M,b_{1},b_{2}) holds

(M,b_{2},b_{1})

end;
let x, y be Element of M;

:: original: tolerates

redefine pred x tolerates y;

symmetry

for x, y being Element of M st (M,b

(M,b

proof end;

definition

let M be non empty MetrStruct ;

let x be Element of M;

{ y where y is Element of M : x tolerates y } is Subset of M

end;
let x be Element of M;

func x -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 } ;

{ y where y is Element of M : x tolerates y } is Subset of M

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

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 ;

ex b_{1} being Subset of M ex x being Element of M st b_{1} = x -neighbour

end;
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 x being Element of M st it = x -neighbour ;

ex b

proof end;

:: deftheorem Def3 defines equivalence_class METRIC_2:def 3 :

for M being non empty MetrStruct

for b_{2} being Subset of M holds

( b_{2} is equivalence_class of M iff ex x being Element of M st b_{2} = x -neighbour );

for M being non empty MetrStruct

for b

( b

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

for x, y, z being Element of M st x tolerates y & y tolerates z holds

x tolerates z

proof end;

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 )

for x, y being Element of M holds

( y in x -neighbour iff y tolerates x )

proof end;

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

for x, p, q being Element of M st p in x -neighbour & q in x -neighbour holds

p tolerates q

proof end;

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

for x, y being Element of M st x in y -neighbour holds

y in x -neighbour

proof end;

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

for p, x, y being Element of M st p in x -neighbour & x tolerates y holds

p in y -neighbour

proof end;

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

for x, y being Element of M st y in x -neighbour holds

x -neighbour = y -neighbour

proof end;

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 ) by Th2, Th4, Th7;

for x, y being Element of M holds

( x -neighbour = y -neighbour iff x tolerates y ) by Th2, Th4, Th7;

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 )

for x, y being Element of M holds

( x -neighbour meets y -neighbour iff x tolerates y )

proof end;

Lm2: for M being PseudoMetricSpace

for V being equivalence_class of M holds V is non empty set

proof end;

registration

let M be PseudoMetricSpace;

coherence

for b_{1} being equivalence_class of M holds not b_{1} is empty
by Lm2;

end;
coherence

for b

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

for x, p, q being Element of M st p in x -neighbour & q in x -neighbour holds

dist (p,q) = 0

proof end;

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 ) by METRIC_1:2;

for x, y being Element of M holds

( x tolerates y iff x = y ) by METRIC_1:2;

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} )

for V being Subset of M holds

( V is equivalence_class of M iff ex x being Element of M st V = {x} )

proof end;

:: Set of the equivalence classes

definition

let M be non empty MetrStruct ;

{ s where s is Subset of M : ex x being Element of M st x -neighbour = s } is set ;

end;
func M -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 } ;

{ s where s is Subset of M : ex x being Element of M st x -neighbour = s } is set ;

:: 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 } ;

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 } ;

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 )

for M being non empty MetrStruct holds

( V in M -neighbour iff ex x being Element of M st V = x -neighbour )

proof end;

theorem :: METRIC_2:16

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 )

for M being non empty MetrStruct holds

( V in M -neighbour iff V is equivalence_class of M )

proof end;

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} )

for M being non empty MetrSpace holds

( V in M -neighbour iff ex x being Element of M st V = {x} )

proof end;

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)

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)

proof end;

:: deftheorem defines is_dst METRIC_2:def 5 :

for M being non empty MetrStruct

for V, Q being Element of M -neighbour

for v being 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 );

for M being non empty MetrStruct

for V, Q being Element of M -neighbour

for v being 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 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 ) )

for V, Q being Element of M -neighbour

for v being 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 ) )

proof end;

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

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

proof end;

definition

let M be non empty MetrStruct ;

let V, Q be Element of M -neighbour ;

{ v where v is Element of REAL : V,Q is_dst v } is Subset of REAL

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

{ v where v is Element of REAL : V,Q is_dst v } is Subset of REAL

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

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 )

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 )

proof end;

definition

let M be non empty MetrStruct ;

let v be Element of REAL ;

{ 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;
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 ) } ;

{ 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):]

proof 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 ) } ;

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 ) )

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 ) )

proof end;

definition

let M be non empty MetrStruct ;

{ 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

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

{ 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

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

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 )

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 )

proof end;

definition

let M be non empty MetrStruct ;

{ 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)

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

{ 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)

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

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 )

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 )

proof end;

definition

let M be non empty MetrStruct ;

{ 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)

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

{ 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)

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

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 )

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 )

proof end;

definition

let M be non empty MetrStruct ;

{ 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;
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 ) } ;

{ 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):]

proof 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 ) } ;

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 ) )

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 ) )

proof end;

definition

let M be non empty MetrStruct ;

{ 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;
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 ) } ;

{ 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:]

proof 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 ) } ;

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 ) )

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 ) )

proof end;

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):]

proof end;

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

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

proof end;

theorem Th33: :: METRIC_2:33

for M being PseudoMetricSpace

for V, Q being Element of M -neighbour ex v being Real st V,Q is_dst v

for V, Q being Element of M -neighbour ex v being Real st V,Q is_dst v

proof end;

definition

let M be PseudoMetricSpace;

ex b_{1} 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

b_{1} . (V,Q) = dist (p,q)

for b_{1}, b_{2} 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

b_{1} . (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

b_{2} . (V,Q) = dist (p,q) ) holds

b_{1} = b_{2}

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

ex b

for V, Q being Element of M -neighbour

for p, q being Element of M st p in V & q in Q holds

b

proof end;

uniqueness for b

for p, q being Element of M st p in V & q in Q holds

b

for p, q being Element of M st p in V & q in Q holds

b

b

proof end;

:: deftheorem Def13 defines nbourdist METRIC_2:def 13 :

for M being PseudoMetricSpace

for b_{2} being Function of [:(M -neighbour),(M -neighbour):],REAL holds

( b_{2} = 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

b_{2} . (V,Q) = dist (p,q) );

for M being PseudoMetricSpace

for b

( b

for p, q being Element of M st p in V & q in Q holds

b

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 )

for V, Q being Element of M -neighbour holds

( (nbourdist M) . (V,Q) = 0 iff V = Q )

proof end;

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)

for V, Q being Element of M -neighbour holds (nbourdist M) . (V,Q) = (nbourdist M) . (Q,V)

proof end;

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))

for V, Q, W being Element of M -neighbour holds (nbourdist M) . (V,W) <= ((nbourdist M) . (V,Q)) + ((nbourdist M) . (Q,W))

proof end;

definition

let M be PseudoMetricSpace;

MetrStruct(# (M -neighbour),(nbourdist M) #) is MetrSpace

end;
func Eq_classMetricSpace M -> MetrSpace equals :: METRIC_2:def 14

MetrStruct(# (M -neighbour),(nbourdist M) #);

coherence MetrStruct(# (M -neighbour),(nbourdist M) #);

MetrStruct(# (M -neighbour),(nbourdist M) #) is MetrSpace

proof end;

:: deftheorem defines Eq_classMetricSpace METRIC_2:def 14 :

for M being PseudoMetricSpace holds Eq_classMetricSpace M = MetrStruct(# (M -neighbour),(nbourdist M) #);

for M being PseudoMetricSpace holds Eq_classMetricSpace M = MetrStruct(# (M -neighbour),(nbourdist M) #);

registration

let M be PseudoMetricSpace;

coherence

( Eq_classMetricSpace M is strict & not Eq_classMetricSpace M is empty ) ;

end;
coherence

( Eq_classMetricSpace M is strict & not Eq_classMetricSpace M is empty ) ;