metric_2.miz



    begin

    definition

      let M be non empty MetrStruct, x,y be Element of M;

      :: METRIC_2:def1

      pred x tolerates y means ( dist (x,y)) = 0 ;

    end

    definition

      let M be Reflexive non empty MetrStruct, x,y be Element of M;

      :: original: tolerates

      redefine

      pred x tolerates y;

      reflexivity by METRIC_1: 1;

    end

    definition

      let M be symmetric non empty MetrStruct, x,y be Element of M;

      :: original: tolerates

      redefine

      pred x tolerates y;

      symmetry

      proof

        let x,y be Element of M;

        assume x tolerates y;

        then ( dist (x,y)) = 0 ;

        hence thesis;

      end;

    end

    definition

      let M be non empty MetrStruct, x be Element of M;

      :: METRIC_2:def2

      func x -neighbour -> Subset of M equals { y where y be Element of M : x tolerates y };

      coherence

      proof

        defpred P[ Element of M] means x tolerates $1;

        { y where y be Element of M : P[y] } c= the carrier of M from FRAENKEL:sch 10;

        hence thesis;

      end;

    end

    definition

      let M be non empty MetrStruct;

      :: METRIC_2:def3

      mode equivalence_class of M -> Subset of M means

      : Def3: ex x be Element of M st it = (x -neighbour );

      existence

      proof

        set z = the Element of M;

        (z -neighbour ) is Subset of M;

        hence thesis;

      end;

    end

    

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

    theorem :: METRIC_2:1

    

     Th1: for M be PseudoMetricSpace, x,y,z be Element of M holds x tolerates y & y tolerates z implies x tolerates z

    proof

      let M be PseudoMetricSpace, x,y,z be Element of M;

      assume x tolerates y & y tolerates z;

      then ( dist (x,y)) = 0 & ( dist (y,z)) = 0 ;

      then ( dist (x,z)) <= ( 0 + 0 ) by METRIC_1: 4;

      then ( dist (x,z)) = 0 by METRIC_1: 5;

      hence thesis;

    end;

    theorem :: METRIC_2:2

    

     Th2: for M be PseudoMetricSpace, x,y be Element of M holds y in (x -neighbour ) iff y tolerates x

    proof

      let M be PseudoMetricSpace, x,y be Element of M;

      hereby

        assume y in (x -neighbour );

        then ex q be Element of M st y = q & x tolerates q;

        hence y tolerates x;

      end;

      assume y tolerates x;

      hence thesis;

    end;

    theorem :: METRIC_2:3

    for M be PseudoMetricSpace, x,p,q be Element of M st p in (x -neighbour ) & q in (x -neighbour ) holds p tolerates q

    proof

      let M be PseudoMetricSpace, x,p,q be Element of M;

      assume p in (x -neighbour ) & q in (x -neighbour );

      then p tolerates x & q tolerates x by Th2;

      hence thesis by Th1;

    end;

    theorem :: METRIC_2:4

    

     Th4: for M be PseudoMetricSpace, x be Element of M holds x in (x -neighbour )

    proof

      let M be PseudoMetricSpace, x be Element of M;

      x tolerates x by Lm1;

      hence thesis;

    end;

    theorem :: METRIC_2:5

    for M be PseudoMetricSpace, x,y be Element of M holds x in (y -neighbour ) implies y in (x -neighbour )

    proof

      let M be PseudoMetricSpace, x,y be Element of M;

      assume x in (y -neighbour );

      then x tolerates y by Th2;

      hence thesis;

    end;

    theorem :: METRIC_2:6

    for M be PseudoMetricSpace, p,x,y be Element of M holds p in (x -neighbour ) & x tolerates y implies p in (y -neighbour )

    proof

      let M be PseudoMetricSpace, p,x,y be Element of M;

      assume that

       A1: p in (x -neighbour ) and

       A2: x tolerates y;

      p tolerates x by A1, Th2;

      then p tolerates y by A2, Th1;

      hence thesis;

    end;

    theorem :: METRIC_2:7

    

     Th7: for M be PseudoMetricSpace, x,y be Element of M holds y in (x -neighbour ) implies (x -neighbour ) = (y -neighbour )

    proof

      let M be PseudoMetricSpace, x,y be Element of M;

      assume

       A1: y in (x -neighbour );

      for p be Element of M holds p in (y -neighbour ) implies p in (x -neighbour )

      proof

        let p be Element of M;

        assume p in (y -neighbour );

        then

         A2: p tolerates y by Th2;

        y tolerates x by A1, Th2;

        then p tolerates x by A2, Th1;

        hence thesis;

      end;

      then

       A3: (y -neighbour ) c= (x -neighbour ) by SUBSET_1: 2;

      for p be Element of M holds p in (x -neighbour ) implies p in (y -neighbour )

      proof

        let p be Element of M;

        assume p in (x -neighbour );

        then

         A4: p tolerates x by Th2;

        x tolerates y by A1, Th2;

        then p tolerates y by A4, Th1;

        hence thesis;

      end;

      then (x -neighbour ) c= (y -neighbour ) by SUBSET_1: 2;

      hence thesis by A3, XBOOLE_0:def 10;

    end;

    theorem :: METRIC_2:8

    

     Th8: for M be PseudoMetricSpace, x,y be Element of M holds (x -neighbour ) = (y -neighbour ) iff x tolerates y by Th2, Th4, Th7;

    theorem :: METRIC_2:9

    for M be PseudoMetricSpace, x,y be Element of M holds (x -neighbour ) meets (y -neighbour ) iff x tolerates y

    proof

      let M be PseudoMetricSpace, x,y be Element of M;

      hereby

        assume (x -neighbour ) meets (y -neighbour );

        then

        consider p be object such that

         A1: p in (x -neighbour ) and

         A2: p in (y -neighbour ) by XBOOLE_0: 3;

        

         A3: ex q be Element of M st q = p & x tolerates q by A1;

        reconsider p as Element of M by A1;

        ex s be Element of M st s = p & y tolerates s by A2;

        hence x tolerates y by A3, Th1;

      end;

      assume x tolerates y;

      then

       A4: x in (y -neighbour );

      x in (x -neighbour ) by Th4;

      hence thesis by A4, XBOOLE_0: 3;

    end;

    

     Lm2: for M be PseudoMetricSpace, V be equivalence_class of M holds V is non empty set

    proof

      let M be PseudoMetricSpace, V be equivalence_class of M;

      ex x be Element of M st V = (x -neighbour ) by Def3;

      hence thesis by Th4;

    end;

    registration

      let M be PseudoMetricSpace;

      cluster -> non empty for equivalence_class of M;

      coherence by Lm2;

    end

    theorem :: METRIC_2:10

    

     Th10: for M be PseudoMetricSpace, x,p,q be Element of M holds p in (x -neighbour ) & q in (x -neighbour ) implies ( dist (p,q)) = 0

    proof

      let M be PseudoMetricSpace, x,p,q be Element of M;

      assume p in (x -neighbour ) & q in (x -neighbour );

      then p tolerates x & q tolerates x by Th2;

      then p tolerates q by Th1;

      hence thesis;

    end;

    theorem :: METRIC_2:11

    

     Th11: for M be Reflexive discerning non empty MetrStruct, x,y be Element of M holds x tolerates y iff x = y by METRIC_1: 2;

    theorem :: METRIC_2:12

    

     Th12: for M be non empty MetrSpace, x,y be Element of M holds y in (x -neighbour ) iff y = x

    proof

      let M be non empty MetrSpace, x,y be Element of M;

      hereby

        assume y in (x -neighbour );

        then ex q be Element of M st y = q & x tolerates q;

        hence y = x by Th11;

      end;

      assume y = x;

      then x tolerates y by Th11;

      hence thesis;

    end;

    theorem :: METRIC_2:13

    

     Th13: for M be non empty MetrSpace, x be Element of M holds (x -neighbour ) = {x}

    proof

      let M be non empty MetrSpace, x be Element of M;

      for p be Element of M holds p in {x} implies p in (x -neighbour )

      proof

        let p be Element of M;

        assume p in {x};

        then p = x by TARSKI:def 1;

        hence thesis by Th12;

      end;

      then

       A1: {x} c= (x -neighbour ) by SUBSET_1: 2;

      for p be Element of M holds p in (x -neighbour ) implies p in {x}

      proof

        let p be Element of M;

        assume p in (x -neighbour );

        then p = x by Th12;

        hence thesis by TARSKI:def 1;

      end;

      then (x -neighbour ) c= {x} by SUBSET_1: 2;

      hence thesis by A1, XBOOLE_0:def 10;

    end;

    theorem :: METRIC_2:14

    for M be non empty MetrSpace, V be Subset of M holds (V is equivalence_class of M iff ex x be Element of M st V = {x})

    proof

      let M be non empty MetrSpace, V be Subset of M;

      

       A1: V is equivalence_class of M implies ex x be Element of M st V = {x}

      proof

        assume V is equivalence_class of M;

        then

        consider x be Element of M such that

         A2: V = (x -neighbour ) by Def3;

        (x -neighbour ) = {x} by Th13;

        hence thesis by A2;

      end;

      (ex x be Element of M st V = {x}) implies V is equivalence_class of M

      proof

        given x be Element of M such that

         A3: V = {x};

         {x} = (x -neighbour ) by Th13;

        hence thesis by A3, Def3;

      end;

      hence thesis by A1;

    end;

    definition

      let M be non empty MetrStruct;

      :: METRIC_2:def4

      func M -neighbour -> set equals { s where s be Subset of M : ex x be Element of M st (x -neighbour ) = s };

      coherence ;

    end

    registration

      let M be non empty MetrStruct;

      cluster (M -neighbour ) -> non empty;

      coherence

      proof

        set y = the Element of M;

        (y -neighbour ) in { s where s be Subset of M : ex x be Element of M st (x -neighbour ) = s };

        hence thesis;

      end;

    end

    reserve V for set;

    theorem :: METRIC_2:15

    

     Th15: for M be non empty MetrStruct holds V in (M -neighbour ) iff ex x be Element of M st V = (x -neighbour )

    proof

      let M be non empty MetrStruct;

      V in (M -neighbour ) implies ex x be Element of M st V = (x -neighbour )

      proof

        assume V in (M -neighbour );

        then ex q be Subset of M st (q = V & ex x be Element of M st q = (x -neighbour ));

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: METRIC_2:16

    for M be non empty MetrStruct, x be Element of M holds (x -neighbour ) in (M -neighbour );

    theorem :: METRIC_2:17

    

     Th17: for M be non empty MetrStruct holds V in (M -neighbour ) iff V is equivalence_class of M

    proof

      let M be non empty MetrStruct;

      

       A1: V is equivalence_class of M implies V in (M -neighbour )

      proof

        assume V is equivalence_class of M;

        then ex x be Element of M st V = (x -neighbour ) by Def3;

        hence thesis;

      end;

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

      proof

        assume V in (M -neighbour );

        then ex x be Element of M st V = (x -neighbour ) by Th15;

        hence thesis by Def3;

      end;

      hence thesis by A1;

    end;

    theorem :: METRIC_2:18

    for M be non empty MetrSpace, x be Element of M holds {x} in (M -neighbour )

    proof

      let M be non empty MetrSpace, x be Element of M;

      (x -neighbour ) = {x} by Th13;

      hence thesis;

    end;

    theorem :: METRIC_2:19

    for M be non empty MetrSpace holds V in (M -neighbour ) iff ex x be Element of M st V = {x}

    proof

      let M be non empty MetrSpace;

      

       A1: V in (M -neighbour ) implies ex x be Element of M st V = {x}

      proof

        assume V in (M -neighbour );

        then

        consider x be Element of M such that

         A2: V = (x -neighbour ) by Th15;

        (x -neighbour ) = {x} by Th13;

        hence thesis by A2;

      end;

      (ex x be Element of M st V = {x}) implies V in (M -neighbour )

      proof

        given x be Element of M such that

         A3: V = {x};

        (x -neighbour ) = {x} by Th13;

        hence thesis by A3;

      end;

      hence thesis by A1;

    end;

    theorem :: METRIC_2:20

    

     Th20: for M be PseudoMetricSpace, V,Q be Element of (M -neighbour ) holds for p1,p2,q1,q2 be Element of M holds (p1 in V & q1 in Q & p2 in V & q2 in Q implies ( dist (p1,q1)) = ( dist (p2,q2)))

    proof

      let M be PseudoMetricSpace, V,Q be Element of (M -neighbour );

      let p1,p2,q1,q2 be Element of M;

      assume that

       A1: p1 in V and

       A2: q1 in Q and

       A3: p2 in V and

       A4: q2 in Q;

      V is equivalence_class of M by Th17;

      then ex x be Element of M st V = (x -neighbour ) by Def3;

      then

       A5: ( dist (p1,p2)) = 0 by A1, A3, Th10;

      Q is equivalence_class of M by Th17;

      then ex y be Element of M st Q = (y -neighbour ) by Def3;

      then

       A6: ( dist (q1,q2)) = 0 by A2, A4, Th10;

      ( dist (p2,q2)) <= (( dist (p2,p1)) + ( dist (p1,q2))) & ( dist (p1,q2)) <= (( dist (p1,q1)) + ( dist (q1,q2))) by METRIC_1: 4;

      then

       A7: ( dist (p2,q2)) <= ( dist (p1,q1)) by A5, A6, XXREAL_0: 2;

      ( dist (p1,q1)) <= (( dist (p1,p2)) + ( dist (p2,q1))) & ( dist (p2,q1)) <= (( dist (p2,q2)) + ( dist (q2,q1))) by METRIC_1: 4;

      then ( dist (p1,q1)) <= ( dist (p2,q2)) by A5, A6, XXREAL_0: 2;

      hence thesis by A7, XXREAL_0: 1;

    end;

    definition

      let M be non empty MetrStruct, V,Q be Element of (M -neighbour ), v be Real;

      :: METRIC_2:def5

      pred V,Q is_dst v means for p,q be Element of M st p in V & q in Q holds ( dist (p,q)) = v;

    end

    theorem :: METRIC_2:21

    

     Th21: for M be PseudoMetricSpace, V,Q be Element of (M -neighbour ), v be Real holds (V,Q) is_dst v iff ex p,q be Element of M st p in V & q in Q & ( dist (p,q)) = v

    proof

      let M be PseudoMetricSpace, V,Q be Element of (M -neighbour ), v be Real;

      

       A1: (V,Q) is_dst v implies ex p,q be Element of M st p in V & q in Q & ( dist (p,q)) = v

      proof

        consider q be Element of M such that

         A2: Q = (q -neighbour ) by Th15;

        

         A3: q in Q by A2, Th4;

        assume

         A4: (V,Q) is_dst v;

        consider p be Element of M such that

         A5: V = (p -neighbour ) by Th15;

        p in V by A5, Th4;

        then ( dist (p,q)) = v by A4, A3;

        hence thesis by A5, A3, Th4;

      end;

      (ex p,q be Element of M st (p in V & q in Q & ( dist (p,q)) = v)) implies (V,Q) is_dst v by Th20;

      hence thesis by A1;

    end;

    theorem :: METRIC_2:22

    

     Th22: for M be PseudoMetricSpace, V,Q be Element of (M -neighbour ), v be Element of REAL st (V,Q) is_dst v holds (Q,V) is_dst v

    proof

      let M be PseudoMetricSpace, V,Q be Element of (M -neighbour ), v be Element of REAL ;

      assume (V,Q) is_dst v;

      then for q,p be Element of M st q in Q & p in V holds ( dist (q,p)) = v;

      hence thesis;

    end;

    definition

      let M be non empty MetrStruct, V,Q be Element of (M -neighbour );

      :: METRIC_2:def6

      func ev_eq_1 (V,Q) -> Subset of REAL equals { v where v be Element of REAL : (V,Q) is_dst v };

      coherence

      proof

        defpred P[ Element of REAL ] means (V,Q) is_dst $1;

        { v where v be Element of REAL : P[v] } c= REAL from FRAENKEL:sch 10;

        hence thesis;

      end;

    end

    theorem :: METRIC_2:23

    for M be PseudoMetricSpace, V,Q be Element of (M -neighbour ), v be Element of REAL holds v in ( ev_eq_1 (V,Q)) iff (V,Q) is_dst v

    proof

      let M be PseudoMetricSpace, V,Q be Element of (M -neighbour ), v be Element of REAL ;

      v in ( ev_eq_1 (V,Q)) implies (V,Q) is_dst v

      proof

        assume v in ( ev_eq_1 (V,Q));

        then ex r be Element of REAL st r = v & (V,Q) is_dst r;

        hence thesis;

      end;

      hence thesis;

    end;

    definition

      let M be non empty MetrStruct, v be Element of REAL ;

      :: METRIC_2:def7

      func ev_eq_2 (v,M) -> Subset of [:(M -neighbour ), (M -neighbour ):] equals { W where W be Element of [:(M -neighbour ), (M -neighbour ):] : ex V,Q be Element of (M -neighbour ) st W = [V, Q] & (V,Q) is_dst v };

      coherence

      proof

        defpred P[ Element of [:(M -neighbour ), (M -neighbour ):]] means ex V,Q be Element of (M -neighbour ) st $1 = [V, Q] & (V,Q) is_dst v;

        { W where W be Element of [:(M -neighbour ), (M -neighbour ):] : P[W] } c= [:(M -neighbour ), (M -neighbour ):] from FRAENKEL:sch 10;

        hence thesis;

      end;

    end

    theorem :: METRIC_2:24

    for M be PseudoMetricSpace, v be Element of REAL , W be Element of [:(M -neighbour ), (M -neighbour ):] holds W in ( ev_eq_2 (v,M)) iff ex V,Q be Element of (M -neighbour ) st W = [V, Q] & (V,Q) is_dst v

    proof

      let M be PseudoMetricSpace, v be Element of REAL , W be Element of [:(M -neighbour ), (M -neighbour ):];

      W in ( ev_eq_2 (v,M)) implies ex V,Q be Element of (M -neighbour ) st W = [V, Q] & (V,Q) is_dst v

      proof

        assume W in ( ev_eq_2 (v,M));

        then ex S be Element of [:(M -neighbour ), (M -neighbour ):] st W = S & ex V,Q be Element of (M -neighbour ) st S = [V, Q] & (V,Q) is_dst v;

        hence thesis;

      end;

      hence thesis;

    end;

    definition

      let M be non empty MetrStruct;

      :: METRIC_2:def8

      func real_in_rel M -> Subset of REAL equals { v where v be Element of REAL : ex V,Q be Element of (M -neighbour ) st ((V,Q) is_dst v) };

      coherence

      proof

        defpred P[ Element of REAL ] means ex V,Q be Element of (M -neighbour ) st (V,Q) is_dst $1;

        { v where v be Element of REAL : P[v] } c= REAL from FRAENKEL:sch 10;

        hence thesis;

      end;

    end

    theorem :: METRIC_2:25

    for M be PseudoMetricSpace, v be Element of REAL holds v in ( real_in_rel M) iff ex V,Q be Element of (M -neighbour ) st (V,Q) is_dst v

    proof

      let M be PseudoMetricSpace, v be Element of REAL ;

      v in ( real_in_rel M) implies ex V,Q be Element of (M -neighbour ) st (V,Q) is_dst v

      proof

        assume v in ( real_in_rel M);

        then ex r be Element of REAL st v = r & ex V,Q be Element of (M -neighbour ) st (V,Q) is_dst r;

        hence thesis;

      end;

      hence thesis;

    end;

    definition

      let M be non empty MetrStruct;

      :: METRIC_2:def9

      func elem_in_rel_1 M -> Subset of (M -neighbour ) equals { V where V be Element of (M -neighbour ) : ex Q be Element of (M -neighbour ), v be Element of REAL st (V,Q) is_dst v };

      coherence

      proof

        defpred P[ Element of (M -neighbour )] means ex Q be Element of (M -neighbour ), v be Element of REAL st ($1,Q) is_dst v;

        { V where V be Element of (M -neighbour ) : P[V] } c= (M -neighbour ) from FRAENKEL:sch 10;

        hence thesis;

      end;

    end

    theorem :: METRIC_2:26

    

     Th26: for M be PseudoMetricSpace, V be Element of (M -neighbour ) holds V in ( elem_in_rel_1 M) iff ex Q be Element of (M -neighbour ), v be Element of REAL st (V,Q) is_dst v

    proof

      let M be PseudoMetricSpace, V be Element of (M -neighbour );

      V in ( elem_in_rel_1 M) implies ex Q be Element of (M -neighbour ), v be Element of REAL st (V,Q) is_dst v

      proof

        assume V in ( elem_in_rel_1 M);

        then ex S be Element of (M -neighbour ) st S = V & ex Q be Element of (M -neighbour ), v be Element of REAL st (S,Q) is_dst v;

        hence thesis;

      end;

      hence thesis;

    end;

    definition

      let M be non empty MetrStruct;

      :: METRIC_2:def10

      func elem_in_rel_2 M -> Subset of (M -neighbour ) equals { Q where Q be Element of (M -neighbour ) : ex V be Element of (M -neighbour ), v be Element of REAL st (V,Q) is_dst v };

      coherence

      proof

        defpred P[ Element of (M -neighbour )] means ex V be Element of (M -neighbour ), v be Element of REAL st (V,$1) is_dst v;

        { Q where Q be Element of (M -neighbour ) : P[Q] } c= (M -neighbour ) from FRAENKEL:sch 10;

        hence thesis;

      end;

    end

    theorem :: METRIC_2:27

    

     Th27: for M be PseudoMetricSpace, Q be Element of (M -neighbour ) holds Q in ( elem_in_rel_2 M) iff ex V be Element of (M -neighbour ), v be Element of REAL st (V,Q) is_dst v

    proof

      let M be PseudoMetricSpace, Q be Element of (M -neighbour );

      Q in ( elem_in_rel_2 M) implies ex V be Element of (M -neighbour ), v be Element of REAL st (V,Q) is_dst v

      proof

        assume Q in ( elem_in_rel_2 M);

        then ex S be Element of (M -neighbour ) st S = Q & ex V be Element of (M -neighbour ), v be Element of REAL st (V,S) is_dst v;

        hence thesis;

      end;

      hence thesis;

    end;

    definition

      let M be non empty MetrStruct;

      :: METRIC_2:def11

      func elem_in_rel M -> Subset of [:(M -neighbour ), (M -neighbour ):] equals { VQ where VQ be Element of [:(M -neighbour ), (M -neighbour ):] : ex V,Q be Element of (M -neighbour ), v be Element of REAL st VQ = [V, Q] & (V,Q) is_dst v };

      coherence

      proof

        defpred P[ Element of [:(M -neighbour ), (M -neighbour ):]] means ex V,Q be Element of (M -neighbour ), v be Element of REAL st $1 = [V, Q] & (V,Q) is_dst v;

        { VQ where VQ be Element of [:(M -neighbour ), (M -neighbour ):] : P[VQ] } c= [:(M -neighbour ), (M -neighbour ):] from FRAENKEL:sch 10;

        hence thesis;

      end;

    end

    theorem :: METRIC_2:28

    for M be PseudoMetricSpace, VQ be Element of [:(M -neighbour ), (M -neighbour ):] holds VQ in ( elem_in_rel M) iff ex V,Q be Element of (M -neighbour ), v be Element of REAL st VQ = [V, Q] & (V,Q) is_dst v

    proof

      let M be PseudoMetricSpace, VQ be Element of [:(M -neighbour ), (M -neighbour ):];

      VQ in ( elem_in_rel M) implies ex V,Q be Element of (M -neighbour ), v be Element of REAL st VQ = [V, Q] & (V,Q) is_dst v

      proof

        assume VQ in ( elem_in_rel M);

        then ex S be Element of [:(M -neighbour ), (M -neighbour ):] st VQ = S & ex V,Q be Element of (M -neighbour ), v be Element of REAL st S = [V, Q] & (V,Q) is_dst v;

        hence thesis;

      end;

      hence thesis;

    end;

    definition

      let M be non empty MetrStruct;

      :: METRIC_2:def12

      func set_in_rel M -> Subset of [:(M -neighbour ), (M -neighbour ), REAL :] equals { VQv where VQv be Element of [:(M -neighbour ), (M -neighbour ), REAL :] : ex V,Q be Element of (M -neighbour ), v be Element of REAL st VQv = [V, Q, v] & (V,Q) is_dst v };

      coherence

      proof

        defpred P[ Element of [:(M -neighbour ), (M -neighbour ), REAL :]] means ex V,Q be Element of (M -neighbour ), v be Element of REAL st $1 = [V, Q, v] & (V,Q) is_dst v;

        { VQv where VQv be Element of [:(M -neighbour ), (M -neighbour ), REAL :] : P[VQv] } c= [:(M -neighbour ), (M -neighbour ), REAL :] from FRAENKEL:sch 10;

        hence thesis;

      end;

    end

    theorem :: METRIC_2:29

    

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

    proof

      let M be PseudoMetricSpace, VQv be Element of [:(M -neighbour ), (M -neighbour ), REAL :];

      VQv in ( set_in_rel M) implies ex V,Q be Element of (M -neighbour ), v be Element of REAL st VQv = [V, Q, v] & (V,Q) is_dst v

      proof

        assume VQv in ( set_in_rel M);

        then ex S be Element of [:(M -neighbour ), (M -neighbour ), REAL :] st VQv = S & ex V,Q be Element of (M -neighbour ), v be Element of REAL st S = [V, Q, v] & (V,Q) is_dst v;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: METRIC_2:30

    for M be PseudoMetricSpace holds ( elem_in_rel_1 M) = ( elem_in_rel_2 M)

    proof

      let M be PseudoMetricSpace;

      for V be Element of (M -neighbour ) holds (V in ( elem_in_rel_2 M) implies V in ( elem_in_rel_1 M))

      proof

        let V be Element of (M -neighbour );

        assume V in ( elem_in_rel_2 M);

        then

        consider Q be Element of (M -neighbour ), v be Element of REAL such that

         A1: (Q,V) is_dst v by Th27;

        (V,Q) is_dst v by A1, Th22;

        hence thesis;

      end;

      then

       A2: ( elem_in_rel_2 M) c= ( elem_in_rel_1 M) by SUBSET_1: 2;

      for V be Element of (M -neighbour ) holds (V in ( elem_in_rel_1 M) implies V in ( elem_in_rel_2 M))

      proof

        let V be Element of (M -neighbour );

        assume V in ( elem_in_rel_1 M);

        then

        consider Q be Element of (M -neighbour ), v be Element of REAL such that

         A3: (V,Q) is_dst v by Th26;

        (Q,V) is_dst v by A3, Th22;

        hence thesis;

      end;

      then ( elem_in_rel_1 M) c= ( elem_in_rel_2 M) by SUBSET_1: 2;

      hence thesis by A2, XBOOLE_0:def 10;

    end;

    theorem :: METRIC_2:31

    for M be PseudoMetricSpace holds ( set_in_rel M) c= [:( elem_in_rel_1 M), ( elem_in_rel_2 M), ( real_in_rel M):]

    proof

      let M be PseudoMetricSpace;

      for VQv be Element of [:(M -neighbour ), (M -neighbour ), REAL :] holds (VQv in ( set_in_rel M) implies VQv in [:( elem_in_rel_1 M), ( elem_in_rel_2 M), ( real_in_rel M):])

      proof

        let VQv be Element of [:(M -neighbour ), (M -neighbour ), REAL :];

        assume VQv in ( set_in_rel M);

        then

        consider V,Q be Element of (M -neighbour ), v be Element of REAL such that

         A1: VQv = [V, Q, v] and

         A2: (V,Q) is_dst v by Th29;

        

         A3: v in ( real_in_rel M) by A2;

        V in ( elem_in_rel_1 M) & Q in ( elem_in_rel_2 M) by A2;

        hence thesis by A1, A3, MCART_1: 69;

      end;

      hence thesis by SUBSET_1: 2;

    end;

    theorem :: METRIC_2:32

    for M be PseudoMetricSpace, V,Q be Element of (M -neighbour ), v1,v2 be Element of REAL holds (V,Q) is_dst v1 & (V,Q) is_dst v2 implies v1 = v2

    proof

      let M be PseudoMetricSpace, V,Q be Element of (M -neighbour ), v1,v2 be Element of REAL ;

      assume that

       A1: (V,Q) is_dst v1 and

       A2: (V,Q) is_dst v2;

      consider p1 be Element of M such that

       A3: V = (p1 -neighbour ) by Th15;

      consider q1 be Element of M such that

       A4: Q = (q1 -neighbour ) by Th15;

      

       A5: q1 in Q by A4, Th4;

      

       A6: p1 in V by A3, Th4;

      then ( dist (p1,q1)) = v1 by A1, A5;

      hence thesis by A2, A6, A5;

    end;

    theorem :: METRIC_2:33

    

     Th33: for M be PseudoMetricSpace, V,Q be Element of (M -neighbour ) holds ex v be Real st (V,Q) is_dst v

    proof

      let M be PseudoMetricSpace, V,Q be Element of (M -neighbour );

      consider p be Element of M such that

       A1: V = (p -neighbour ) by Th15;

      consider q be Element of M such that

       A2: Q = (q -neighbour ) by Th15;

      

       A3: q in Q by A2, Th4;

      p in V by A1, Th4;

      then (V,Q) is_dst ( dist (p,q)) by A3, Th21;

      hence thesis;

    end;

    definition

      let M be PseudoMetricSpace;

      :: METRIC_2:def13

      func nbourdist M -> Function of [:(M -neighbour ), (M -neighbour ):], REAL means

      : Def13: for V,Q be Element of (M -neighbour ) holds for p,q be Element of M st p in V & q in Q holds (it . (V,Q)) = ( dist (p,q));

      existence

      proof

        defpred P[ Element of (M -neighbour ), Element of (M -neighbour ), Real] means ($1,$2) is_dst $3;

        

         A1: for V,Q be Element of (M -neighbour ) holds ex v be Element of REAL st P[V, Q, v]

        proof

          let V,Q be Element of (M -neighbour );

          consider v be Real such that

           A2: P[V, Q, v] by Th33;

          reconsider v as Element of REAL by XREAL_0:def 1;

          take v;

          thus thesis by A2;

        end;

        consider F be Function of [:(M -neighbour ), (M -neighbour ):], REAL such that

         A3: for V,Q be Element of (M -neighbour ) holds P[V, Q, (F . (V,Q))] from BINOP_1:sch 3( A1);

        take F;

        let V,Q be Element of (M -neighbour ), p,q be Element of M such that

         A4: p in V & q in Q;

        (V,Q) is_dst (F . (V,Q)) by A3;

        hence thesis by A4;

      end;

      uniqueness

      proof

        let F1,F2 be Function of [:(M -neighbour ), (M -neighbour ):], REAL ;

        assume that

         A5: for V,Q be Element of (M -neighbour ) holds for p,q be Element of M st p in V & q in Q holds (F1 . (V,Q)) = ( dist (p,q)) and

         A6: for V,Q be Element of (M -neighbour ) holds for p,q be Element of M st p in V & q in Q holds (F2 . (V,Q)) = ( dist (p,q));

        for V,Q be Element of (M -neighbour ) holds (F1 . (V,Q)) = (F2 . (V,Q))

        proof

          let V,Q be Element of (M -neighbour );

          consider p be Element of M such that

           A7: V = (p -neighbour ) by Th15;

          consider q be Element of M such that

           A8: Q = (q -neighbour ) by Th15;

          

           A9: q in Q by A8, Th4;

          

           A10: p in V by A7, Th4;

          

          then (F1 . (V,Q)) = ( dist (p,q)) by A5, A9

          .= (F2 . (V,Q)) by A6, A10, A9;

          hence thesis;

        end;

        hence thesis by BINOP_1: 2;

      end;

    end

    theorem :: METRIC_2:34

    

     Th34: for M be PseudoMetricSpace, V,Q be Element of (M -neighbour ) holds (( nbourdist M) . (V,Q)) = 0 iff V = Q

    proof

      let M be PseudoMetricSpace, V,Q be Element of (M -neighbour );

      

       A1: V = Q implies (( nbourdist M) . (V,Q)) = 0

      proof

        consider p be Element of M such that

         A2: V = (p -neighbour ) by Th15;

        

         A3: p in V by A2, Th4;

        consider q be Element of M such that

         A4: Q = (q -neighbour ) by Th15;

        assume V = Q;

        then

         A5: p tolerates q by A3, A4, Th2;

        q in Q by A4, Th4;

        

        then (( nbourdist M) . (V,Q)) = ( dist (p,q)) by A3, Def13

        .= 0 by A5;

        hence thesis;

      end;

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

      proof

        assume

         A6: (( nbourdist M) . (V,Q)) = 0 ;

        consider p be Element of M such that

         A7: V = (p -neighbour ) by Th15;

        consider q be Element of M such that

         A8: Q = (q -neighbour ) by Th15;

        

         A9: q in Q by A8, Th4;

        p in V by A7, Th4;

        then ( dist (p,q)) = 0 by A6, A9, Def13;

        then p tolerates q;

        hence thesis by A7, A8, Th8;

      end;

      hence thesis by A1;

    end;

    theorem :: METRIC_2:35

    

     Th35: for M be PseudoMetricSpace, V,Q be Element of (M -neighbour ) holds (( nbourdist M) . (V,Q)) = (( nbourdist M) . (Q,V))

    proof

      let M be PseudoMetricSpace, V,Q be Element of (M -neighbour );

      consider p be Element of M such that

       A1: V = (p -neighbour ) by Th15;

      consider q be Element of M such that

       A2: Q = (q -neighbour ) by Th15;

      

       A3: q in Q by A2, Th4;

      

       A4: p in V by A1, Th4;

      

      then (( nbourdist M) . (V,Q)) = ( dist (q,p)) by A3, Def13

      .= (( nbourdist M) . (Q,V)) by A4, A3, Def13;

      hence thesis;

    end;

    theorem :: METRIC_2:36

    

     Th36: for M be PseudoMetricSpace, V,Q,W be Element of (M -neighbour ) holds (( nbourdist M) . (V,W)) <= ((( nbourdist M) . (V,Q)) + (( nbourdist M) . (Q,W)))

    proof

      let M be PseudoMetricSpace, V,Q,W be Element of (M -neighbour );

      consider p be Element of M such that

       A1: V = (p -neighbour ) by Th15;

      consider w be Element of M such that

       A2: W = (w -neighbour ) by Th15;

      

       A3: w in W by A2, Th4;

      consider q be Element of M such that

       A4: Q = (q -neighbour ) by Th15;

      

       A5: q in Q by A4, Th4;

      then

       A6: (( nbourdist M) . (Q,W)) = ( dist (q,w)) by A3, Def13;

      

       A7: p in V by A1, Th4;

      then

       A8: (( nbourdist M) . (V,W)) = ( dist (p,w)) by A3, Def13;

      (( nbourdist M) . (V,Q)) = ( dist (p,q)) by A7, A5, Def13;

      hence thesis by A8, A6, METRIC_1: 4;

    end;

    definition

      let M be PseudoMetricSpace;

      :: METRIC_2:def14

      func Eq_classMetricSpace M -> MetrSpace equals MetrStruct (# (M -neighbour ), ( nbourdist M) #);

      coherence

      proof

        set Z = MetrStruct (# (M -neighbour ), ( nbourdist M) #);

        now

          let V,Q,W be Element of Z;

          reconsider V9 = V, Q9 = Q, W9 = W as Element of (M -neighbour );

          

           A1: ( dist (V,Q)) = (( nbourdist M) . (V9,Q9)) by METRIC_1:def 1;

          hence ( dist (V,Q)) = 0 iff V = Q by Th34;

          ( dist (Q,V)) = (( nbourdist M) . (Q9,V9)) by METRIC_1:def 1;

          hence ( dist (V,Q)) = ( dist (Q,V)) by A1, Th35;

          ( dist (V,W)) = (( nbourdist M) . (V9,W9)) & ( dist (Q,W)) = (( nbourdist M) . (Q9,W9)) by METRIC_1:def 1;

          hence ( dist (V,W)) <= (( dist (V,Q)) + ( dist (Q,W))) by A1, Th36;

        end;

        hence thesis by METRIC_1: 6;

      end;

    end

    registration

      let M be PseudoMetricSpace;

      cluster ( Eq_classMetricSpace M) -> strict non empty;

      coherence ;

    end