metric_1.miz



    begin

    definition

      struct ( 1-sorted) MetrStruct (# the carrier -> set,

the distance -> Function of [: the carrier, the carrier:], REAL #)

       attr strict strict;

    end

    registration

      cluster non empty strict for MetrStruct;

      existence

      proof

        set A = the non empty set, r = the Function of [:A, A:], REAL ;

        take MetrStruct (# A, r #);

        thus the carrier of MetrStruct (# A, r #) is non empty;

        thus thesis;

      end;

    end

    definition

      let M be MetrStruct;

      let a,b be Element of M;

      :: METRIC_1:def1

      func dist (a,b) -> Real equals (the distance of M . (a,b));

      coherence ;

    end

    notation

      synonym Empty^2-to-zero for op2 ;

    end

    

     Lm1: 0 in REAL by XREAL_0:def 1;

    definition

      :: original: Empty^2-to-zero

      redefine

      func Empty^2-to-zero -> Function of [:1, 1:], REAL ;

      coherence

      proof

         op2 is Function of [:1, 1:], 1 & 1 c= REAL by CARD_1: 49, ZFMISC_1: 31, Lm1;

        hence thesis by FUNCT_2: 7;

      end;

    end

    

     Lm2: ( op2 . ( 0 , 0 )) = 0

    proof

       [ 0 , 0 ] in [: { 0 }, { 0 }:] by ZFMISC_1: 28;

      hence thesis by FUNCT_2: 50;

    end;

    

     Lm3: for x,y be Element of 1 holds ( op2 . (x,y)) = 0 iff x = y

    proof

      let x,y be Element of 1;

      

       A1: x = {} & y = {} by CARD_1: 49, TARSKI:def 1;

      hence ( op2 . (x,y)) = 0 implies x = y;

      thus thesis by A1, Lm2;

    end;

    

     Lm4: for x,y be Element of 1 holds ( op2 . (x,y)) = ( op2 . (y,x))

    proof

      let x,y be Element of 1;

      x = {} & y = {} by CARD_1: 49, TARSKI:def 1;

      hence thesis;

    end;

    registration

      cluster op2 -> natural-valued;

      coherence ;

    end

    registration

      let f be natural-valued Function;

      let x,y be object;

      cluster (f . (x,y)) -> natural;

      coherence ;

    end

    

     Lm5: for x,y,z be Element of 1 holds ( op2 . (x,z)) <= (( op2 . (x,y)) + ( op2 . (y,z)))

    proof

      let x,y,z be Element of 1;

      x = {} & y = {} by CARD_1: 49, TARSKI:def 1;

      hence thesis by Lm2;

    end;

    definition

      let A be set;

      let f be PartFunc of [:A, A:], REAL ;

      :: METRIC_1:def2

      attr f is Reflexive means for a be Element of A holds (f . (a,a)) = 0 ;

      :: METRIC_1:def3

      attr f is discerning means for a,b be Element of A st (f . (a,b)) = 0 holds a = b;

      :: METRIC_1:def4

      attr f is symmetric means for a,b be Element of A holds (f . (a,b)) = (f . (b,a));

      :: METRIC_1:def5

      attr f is triangle means for a,b,c be Element of A holds (f . (a,c)) <= ((f . (a,b)) + (f . (b,c)));

    end

    definition

      let M be MetrStruct;

      :: METRIC_1:def6

      attr M is Reflexive means

      : Def6: the distance of M is Reflexive;

      :: METRIC_1:def7

      attr M is discerning means

      : Def7: the distance of M is discerning;

      :: METRIC_1:def8

      attr M is symmetric means

      : Def8: the distance of M is symmetric;

      :: METRIC_1:def9

      attr M is triangle means

      : Def9: the distance of M is triangle;

    end

    registration

      cluster strict Reflexive discerning symmetric triangle non empty for MetrStruct;

      existence

      proof

        reconsider M = MetrStruct (# 1, Empty^2-to-zero #) as strict non empty MetrStruct;

        take M;

        

         A1: the distance of M is discerning by Lm3;

        

         A2: the distance of M is symmetric by Lm4;

        

         A3: the distance of M is triangle by Lm5;

        the distance of M is Reflexive by Lm3;

        hence thesis by A1, A2, A3;

      end;

    end

    definition

      mode MetrSpace is Reflexive discerning symmetric triangle MetrStruct;

    end

    theorem :: METRIC_1:1

    

     Th1: for M be MetrStruct holds (for a be Element of M holds ( dist (a,a)) = 0 ) iff M is Reflexive

    proof

      let M be MetrStruct;

      hereby

        assume

         A1: for a be Element of M holds ( dist (a,a)) = 0 ;

        the distance of M is Reflexive

        proof

          let a be Element of M;

          (the distance of M . (a,a)) = ( dist (a,a))

          .= 0 by A1;

          hence thesis;

        end;

        hence M is Reflexive;

      end;

      assume M is Reflexive;

      then the distance of M is Reflexive;

      hence thesis;

    end;

    theorem :: METRIC_1:2

    

     Th2: for M be MetrStruct holds (for a,b be Element of M st ( dist (a,b)) = 0 holds a = b) iff M is discerning

    proof

      let M be MetrStruct;

      hereby

        assume

         A1: for a,b be Element of M st ( dist (a,b)) = 0 holds a = b;

        the distance of M is discerning

        proof

          let a,b be Element of M;

          assume (the distance of M . (a,b)) = 0 ;

          then ( dist (a,b)) = 0 ;

          hence thesis by A1;

        end;

        hence M is discerning;

      end;

      assume M is discerning;

      then the distance of M is discerning;

      hence thesis;

    end;

    theorem :: METRIC_1:3

    

     Th3: for M be MetrStruct st for a,b be Element of M holds ( dist (a,b)) = ( dist (b,a)) holds M is symmetric

    proof

      let M be MetrStruct;

      assume

       A1: for a,b be Element of M holds ( dist (a,b)) = ( dist (b,a));

      the distance of M is symmetric

      proof

        let a,b be Element of M;

        

        thus (the distance of M . (a,b)) = ( dist (a,b))

        .= ( dist (b,a)) by A1

        .= (the distance of M . (b,a));

      end;

      hence M is symmetric;

    end;

    theorem :: METRIC_1:4

    

     Th4: for M be MetrStruct holds (for a,b,c be Element of M holds ( dist (a,c)) <= (( dist (a,b)) + ( dist (b,c)))) iff M is triangle

    proof

      let M be MetrStruct;

      hereby

        assume

         A1: for a,b,c be Element of M holds ( dist (a,c)) <= (( dist (a,b)) + ( dist (b,c)));

        the distance of M is triangle

        proof

          let a,b,c be Element of M;

          

           A2: (the distance of M . (b,c)) = ( dist (b,c));

          (the distance of M . (a,b)) = ( dist (a,b)) & (the distance of M . (a,c)) = ( dist (a,c));

          hence thesis by A1, A2;

        end;

        hence M is triangle;

      end;

      assume

       A3: M is triangle;

      let a,b,c be Element of M;

      the distance of M is triangle by A3;

      hence thesis;

    end;

    definition

      let M be symmetric MetrStruct;

      let a,b be Element of M;

      :: original: dist

      redefine

      func dist (a,b);

      commutativity

      proof

        the distance of M is symmetric by Def8;

        hence thesis;

      end;

    end

    theorem :: METRIC_1:5

    

     Th5: for M be symmetric triangle Reflexive MetrStruct, a,b be Element of M holds 0 <= ( dist (a,b))

    proof

      let M be symmetric triangle Reflexive MetrStruct, a,b be Element of M;

      

       A1: ((1 / 2) * ( dist (a,a))) = ((1 / 2) * 0 ) by Th1;

      ( dist (a,a)) <= (( dist (a,b)) + ( dist (b,a))) & ( dist (a,b)) = ((1 / 2) * ((1 * ( dist (a,b))) + (1 * ( dist (a,b))))) by Th4;

      hence thesis by A1, XREAL_1: 64;

    end;

    theorem :: METRIC_1:6

    

     Th6: for M be MetrStruct st (for a,b,c be Element of M holds (( dist (a,b)) = 0 iff a = b) & ( dist (a,b)) = ( dist (b,a)) & ( dist (a,c)) <= (( dist (a,b)) + ( dist (b,c)))) holds M is MetrSpace

    proof

      let M be MetrStruct;

      assume

       A1: for a,b,c be Element of M holds (( dist (a,b)) = 0 iff a = b) & ( dist (a,b)) = ( dist (b,a)) & ( dist (a,c)) <= (( dist (a,b)) + ( dist (b,c)));

      

       A2: the distance of M is symmetric

      proof

        let a,b be Element of M;

        (the distance of M . (a,b)) = ( dist (a,b))

        .= ( dist (b,a)) by A1

        .= (the distance of M . (b,a));

        hence thesis;

      end;

      

       A3: the distance of M is triangle

      proof

        let a,b,c be Element of M;

        

         A4: (the distance of M . (b,c)) = ( dist (b,c));

        (the distance of M . (a,c)) = ( dist (a,c)) & (the distance of M . (a,b)) = ( dist (a,b));

        hence thesis by A1, A4;

      end;

      

       A5: the distance of M is discerning

      proof

        let a,b be Element of M;

        assume (the distance of M . (a,b)) = 0 ;

        then ( dist (a,b)) = 0 ;

        hence thesis by A1;

      end;

      the distance of M is Reflexive

      proof

        let a be Element of M;

        (the distance of M . (a,a)) = ( dist (a,a))

        .= 0 by A1;

        hence thesis;

      end;

      hence thesis by A5, A2, A3, Def6, Def7, Def8, Def9;

    end;

    theorem :: METRIC_1:7

    

     Th7: for M be MetrSpace, x,y be Element of M st x <> y holds 0 < ( dist (x,y))

    proof

      let M be MetrSpace;

      let x,y be Element of M;

      

       A1: ( dist (x,y)) >= 0 by Th5;

      assume x <> y;

      then ( dist (x,y)) <> 0 by Th2;

      hence thesis by A1, XXREAL_0: 1;

    end;

    definition

      let A be set;

      :: METRIC_1:def10

      func discrete_dist A -> Function of [:A, A:], REAL means

      : Def10: for x,y be Element of A holds (it . (x,x)) = 0 & (x <> y implies (it . (x,y)) = 1);

      existence

      proof

        per cases ;

          suppose

           A1: A is empty;

          then [:A, A:] = {} by ZFMISC_1: 90;

          then

          reconsider f = {} as Function of [:A, A:], REAL by RELSET_1: 12;

          take f;

          let x,y be Element of A;

          thus (f . (x,x)) = 0 ;

          x = {} by A1, SUBSET_1:def 1

          .= y by A1, SUBSET_1:def 1;

          hence thesis;

        end;

          suppose

           A2: A is non empty;

           0 in REAL & 1 in REAL by XREAL_0:def 1;

          then { 0 , 1} c= REAL & ( rng ( chi (( [:A, A:] \ ( id A)), [:A, A:]))) c= { 0 , 1} by ZFMISC_1: 32;

          then

           A3: ( rng ( chi (( [:A, A:] \ ( id A)), [:A, A:]))) c= REAL by XBOOLE_1: 1;

          ( dom ( chi (( [:A, A:] \ ( id A)), [:A, A:]))) = [:A, A:] by FUNCT_3:def 3;

          then

          reconsider char = ( chi (( [:A, A:] \ ( id A)), [:A, A:])) as Function of [:A, A:], REAL by A3, RELSET_1: 4;

          take char;

          let x,y be Element of A;

          ( [:A, A:] \ ( [:A, A:] \ ( id A))) = ( [:A, A:] /\ ( id A)) by XBOOLE_1: 48

          .= ( id A) by XBOOLE_1: 28;

          then [x, x] in ( [:A, A:] \ ( [:A, A:] \ ( id A))) by A2, RELAT_1:def 10;

          hence (char . (x,x)) = 0 by FUNCT_3: 37;

          assume x <> y;

          then

           A4: not [x, y] in ( id A) by RELAT_1:def 10;

           [x, y] in [:A, A:] by A2, ZFMISC_1:def 2;

          then [x, y] in ( [:A, A:] \ ( id A)) by A4, XBOOLE_0:def 5;

          hence thesis by FUNCT_3:def 3;

        end;

      end;

      uniqueness

      proof

        let f,f9 be Function of [:A, A:], REAL ;

        assume that

         A5: for x,y be Element of A holds (f . (x,x)) = 0 & (x <> y implies (f . (x,y)) = 1) and

         A6: for x,y be Element of A holds (f9 . (x,x)) = 0 & (x <> y implies (f9 . (x,y)) = 1);

        now

          let x,y be Element of A;

          now

            per cases ;

              suppose

               A7: x = y;

              

              hence (f . (x,y)) = 0 by A5

              .= (f9 . (x,y)) by A6, A7;

            end;

              suppose

               A8: x <> y;

              

              hence (f . (x,y)) = 1 by A5

              .= (f9 . (x,y)) by A6, A8;

            end;

          end;

          hence (f . (x,y)) = (f9 . (x,y));

        end;

        hence thesis;

      end;

    end

    definition

      let A be set;

      :: METRIC_1:def11

      func DiscreteSpace A -> strict MetrStruct equals MetrStruct (# A, ( discrete_dist A) #);

      coherence ;

    end

    registration

      let A be non empty set;

      cluster ( DiscreteSpace A) -> non empty;

      coherence ;

    end

    registration

      let A be set;

      cluster ( DiscreteSpace A) -> Reflexive discerning symmetric triangle;

      coherence

      proof

        set M = MetrStruct (# A, ( discrete_dist A) #);

        

         A1: the distance of M is discerning by Def10;

        

         A2: the distance of M is symmetric

        proof

          let a,b be Element of M;

          now

            per cases ;

              suppose

               A3: a <> b;

              

              hence (the distance of M . (a,b)) = 1 by Def10

              .= (the distance of M . (b,a)) by A3, Def10;

            end;

              suppose a = b;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

        

         A4: the distance of M is triangle

        proof

          let a,b,c be Element of M;

          

           A5: (the distance of M . (a,b)) = 0 iff a = b by Def10;

          per cases ;

            suppose a = b & a = c;

            hence thesis by A5;

          end;

            suppose a = b & a <> c;

            hence thesis by A5;

          end;

            suppose

             A6: a = c & a <> b;

            then

             A7: (the distance of M . (b,c)) = 1 by Def10;

            (the distance of M . (a,c)) = 0 & (the distance of M . (a,b)) = 1 by A6, Def10;

            hence thesis by A7;

          end;

            suppose

             A8: b = c & a <> c;

            then (the distance of M . (b,c)) = 0 by Def10;

            hence thesis by A8;

          end;

            suppose

             A9: a <> b & a <> c & b <> c;

            then

             A10: (the distance of M . (b,c)) = 1 by Def10;

            (the distance of M . (a,c)) = 1 & (the distance of M . (a,b)) = 1 by A9, Def10;

            hence thesis by A10;

          end;

        end;

        the distance of M is Reflexive by Def10;

        hence thesis by A1, A2, A4;

      end;

    end

    definition

      :: METRIC_1:def12

      func real_dist -> Function of [: REAL , REAL :], REAL means

      : Def12: for x,y be Real holds (it . (x,y)) = |.(x - y).|;

      existence

      proof

        deffunc G( Real, Real) = ( In ( |.($1 - $2).|, REAL ));

        consider F be Function of [: REAL , REAL :], REAL such that

         A1: for x,y be Element of REAL holds (F . (x,y)) = G(x,y) from BINOP_1:sch 4;

        take F;

        let x,y be Real;

        reconsider x, y as Element of REAL by XREAL_0:def 1;

        (F . (x,y)) = G(x,y) by A1;

        hence thesis;

      end;

      uniqueness

      proof

        let F1,F2 be Function of [: REAL , REAL :], REAL ;

        assume that

         A2: for x,y be Real holds (F1 . (x,y)) = |.(x - y).| and

         A3: for x,y be Real holds (F2 . (x,y)) = |.(x - y).|;

        for x,y be Element of REAL holds (F1 . (x,y)) = (F2 . (x,y))

        proof

          let x,y be Element of REAL ;

          

          thus (F1 . (x,y)) = |.(x - y).| by A2

          .= (F2 . (x,y)) by A3;

        end;

        hence thesis;

      end;

    end

    theorem :: METRIC_1:8

    

     Th8: for x,y be Element of REAL holds ( real_dist . (x,y)) = 0 iff x = y

    proof

      let x,y be Element of REAL ;

      thus ( real_dist . (x,y)) = 0 implies x = y

      proof

        assume ( real_dist . (x,y)) = 0 ;

        then 0 = |.(x - y).| by Def12;

        then (x - y) = 0 by ABSVALUE: 2;

        hence thesis;

      end;

      assume x = y;

      then |.(x - y).| = 0 by ABSVALUE: 2;

      hence thesis by Def12;

    end;

    theorem :: METRIC_1:9

    

     Th9: for x,y be Element of REAL holds ( real_dist . (x,y)) = ( real_dist . (y,x))

    proof

      let x,y be Element of REAL ;

      

      thus ( real_dist . (x,y)) = |.(x - y).| by Def12

      .= |.( - (x - y)).| by COMPLEX1: 52

      .= |.(y - x).|

      .= ( real_dist . (y,x)) by Def12;

    end;

    theorem :: METRIC_1:10

    

     Th10: for x,y,z be Element of REAL holds ( real_dist . (x,y)) <= (( real_dist . (x,z)) + ( real_dist . (z,y)))

    proof

      let x,y,z be Element of REAL ;

       |.(x - y).| = |.((x - z) + (z - y)).|;

      then

       A1: |.(x - y).| <= ( |.(x - z).| + |.(z - y).|) by COMPLEX1: 56;

      ( real_dist . (x,y)) = |.(x - y).| & ( real_dist . (x,z)) = |.(x - z).| by Def12;

      hence thesis by A1, Def12;

    end;

    definition

      :: METRIC_1:def13

      func RealSpace -> strict MetrStruct equals MetrStruct (# REAL , real_dist #);

      coherence ;

    end

    registration

      cluster RealSpace -> non empty;

      coherence ;

    end

    registration

      cluster RealSpace -> Reflexive discerning symmetric triangle;

      coherence

      proof

        reconsider M = MetrStruct (# REAL , real_dist #) as non empty MetrStruct;

        for a,b,c be Element of M holds (( dist (a,b)) = 0 iff a = b) & ( dist (a,b)) = ( dist (b,a)) & ( dist (a,c)) <= (( dist (a,b)) + ( dist (b,c))) by Th8, Th9, Th10;

        hence thesis by Th6;

      end;

    end

    definition

      let M be MetrStruct, p be Element of M, r be Real;

      :: METRIC_1:def14

      func Ball (p,r) -> Subset of M means

      : Def14: it = { q where q be Element of M : ( dist (p,q)) < r } if M is non empty

      otherwise it is empty;

      existence

      proof

        reconsider X = {} as Subset of M by XBOOLE_1: 2;

        thus M is non empty implies ex X be Subset of M st X = { q where q be Element of M : ( dist (p,q)) < r }

        proof

          assume M is non empty;

          then

          reconsider M9 = M as non empty MetrStruct;

          reconsider p9 = p as Element of M9;

          defpred P[ Element of M9] means ( dist (p9,$1)) < r;

          set X = { q where q be Element of M9 : P[q] };

          X c= the carrier of M9 from FRAENKEL:sch 10;

          then

          reconsider X as Subset of M;

          take X;

          thus thesis;

        end;

        assume M is empty;

        take X;

        thus thesis;

      end;

      correctness ;

    end

    definition

      let M be MetrStruct, p be Element of M, r be Real;

      :: METRIC_1:def15

      func cl_Ball (p,r) -> Subset of M means

      : Def15: it = { q where q be Element of M : ( dist (p,q)) <= r } if M is non empty

      otherwise it is empty;

      existence

      proof

        reconsider X = {} as Subset of M by XBOOLE_1: 2;

        thus M is non empty implies ex X be Subset of M st X = { q where q be Element of M : ( dist (p,q)) <= r }

        proof

          assume M is non empty;

          then

          reconsider M9 = M as non empty MetrStruct;

          reconsider p9 = p as Element of M9;

          defpred P[ Element of M9] means ( dist (p9,$1)) <= r;

          set X = { q where q be Element of M9 : P[q] };

          X c= the carrier of M9 from FRAENKEL:sch 10;

          then

          reconsider X as Subset of M;

          take X;

          thus thesis;

        end;

        assume M is empty;

        take X;

        thus thesis;

      end;

      correctness ;

    end

    definition

      let M be MetrStruct, p be Element of M, r be Real;

      :: METRIC_1:def16

      func Sphere (p,r) -> Subset of M means

      : Def16: it = { q where q be Element of M : ( dist (p,q)) = r } if M is non empty

      otherwise it is empty;

      existence

      proof

        reconsider X = {} as Subset of M by XBOOLE_1: 2;

        thus M is non empty implies ex X be Subset of M st X = { q where q be Element of M : ( dist (p,q)) = r }

        proof

          assume M is non empty;

          then

          reconsider M9 = M as non empty MetrStruct;

          reconsider p9 = p as Element of M9;

          defpred P[ Element of M9] means ( dist (p9,$1)) = r;

          set X = { q where q be Element of M9 : P[q] };

          X c= the carrier of M9 from FRAENKEL:sch 10;

          then

          reconsider X as Subset of M;

          take X;

          thus thesis;

        end;

        assume M is empty;

        take X;

        thus thesis;

      end;

      correctness ;

    end

    reserve r for Real;

    theorem :: METRIC_1:11

    

     Th11: for M be MetrStruct, p,x be Element of M holds x in ( Ball (p,r)) iff M is non empty & ( dist (p,x)) < r

    proof

      let M be MetrStruct, p,x be Element of M;

      hereby

        assume

         A1: x in ( Ball (p,r));

        then

        reconsider M9 = M as non empty MetrStruct;

        reconsider p9 = p as Element of M9;

        x in { q where q be Element of M9 : ( dist (p9,q)) < r } by A1, Def14;

        then ex q be Element of M st x = q & ( dist (p,q)) < r;

        hence M is non empty & ( dist (p,x)) < r by A1;

      end;

      assume M is non empty;

      then

      reconsider M9 = M as non empty MetrStruct;

      reconsider p9 = p as Element of M9;

      assume ( dist (p,x)) < r;

      then x in { q where q be Element of M9 : ( dist (p9,q)) < r };

      hence thesis by Def14;

    end;

    theorem :: METRIC_1:12

    

     Th12: for M be MetrStruct, p,x be Element of M holds x in ( cl_Ball (p,r)) iff M is non empty & ( dist (p,x)) <= r

    proof

      let M be MetrStruct, p,x be Element of M;

      hereby

        assume

         A1: x in ( cl_Ball (p,r));

        then

        reconsider M9 = M as non empty MetrStruct;

        reconsider p9 = p as Element of M9;

        x in { q where q be Element of M9 : ( dist (p9,q)) <= r } by A1, Def15;

        then ex q be Element of M st x = q & ( dist (p,q)) <= r;

        hence M is non empty & ( dist (p,x)) <= r by A1;

      end;

      assume M is non empty;

      then

      reconsider M9 = M as non empty MetrStruct;

      reconsider p9 = p as Element of M9;

      assume ( dist (p,x)) <= r;

      then x in { q where q be Element of M9 : ( dist (p9,q)) <= r };

      hence thesis by Def15;

    end;

    theorem :: METRIC_1:13

    

     Th13: for M be MetrStruct, p,x be Element of M holds x in ( Sphere (p,r)) iff M is non empty & ( dist (p,x)) = r

    proof

      let M be MetrStruct, p,x be Element of M;

      hereby

        assume

         A1: x in ( Sphere (p,r));

        then

        reconsider M9 = M as non empty MetrStruct;

        reconsider p9 = p as Element of M9;

        x in { q where q be Element of M9 : ( dist (p9,q)) = r } by A1, Def16;

        then ex q be Element of M st x = q & ( dist (p,q)) = r;

        hence M is non empty & ( dist (p,x)) = r by A1;

      end;

      assume M is non empty;

      then

      reconsider M9 = M as non empty MetrStruct;

      reconsider p9 = p as Element of M9;

      assume ( dist (p,x)) = r;

      then x in { q where q be Element of M9 : ( dist (p9,q)) = r };

      hence thesis by Def16;

    end;

    theorem :: METRIC_1:14

    

     Th14: for M be MetrStruct, p be Element of M holds ( Ball (p,r)) c= ( cl_Ball (p,r))

    proof

      let M be MetrStruct, p be Element of M;

      per cases ;

        suppose

         A1: M is non empty;

        now

          let x be Element of M;

          assume x in ( Ball (p,r));

          then ( dist (p,x)) <= r by Th11;

          then x in { q where q be Element of M : ( dist (p,q)) <= r };

          hence x in ( cl_Ball (p,r)) by A1, Def15;

        end;

        hence thesis by SUBSET_1: 2;

      end;

        suppose

         A2: M is empty;

        then ( Ball (p,r)) is empty;

        hence thesis by A2, Def15;

      end;

    end;

    theorem :: METRIC_1:15

    

     Th15: for M be MetrStruct, p be Element of M holds ( Sphere (p,r)) c= ( cl_Ball (p,r))

    proof

      let M be MetrStruct, p be Element of M;

      per cases ;

        suppose

         A1: M is non empty;

        now

          let x be Element of M;

          assume x in ( Sphere (p,r));

          then ( dist (p,x)) = r by Th13;

          then x in { q where q be Element of M : ( dist (p,q)) <= r };

          hence x in ( cl_Ball (p,r)) by Def15, A1;

        end;

        hence thesis by SUBSET_1: 2;

      end;

        suppose

         A2: M is empty;

        then ( Sphere (p,r)) is empty;

        hence thesis by A2, Def15;

      end;

    end;

    theorem :: METRIC_1:16

    for M be MetrStruct, p be Element of M holds (( Sphere (p,r)) \/ ( Ball (p,r))) = ( cl_Ball (p,r))

    proof

      let M be MetrStruct, p be Element of M;

      ( Sphere (p,r)) c= ( cl_Ball (p,r)) & ( Ball (p,r)) c= ( cl_Ball (p,r)) by Th14, Th15;

      hence (( Sphere (p,r)) \/ ( Ball (p,r))) c= ( cl_Ball (p,r)) by XBOOLE_1: 8;

      per cases ;

        suppose

         A1: M is non empty;

        now

          let x be Element of M;

          assume x in ( cl_Ball (p,r));

          then

           A2: ( dist (p,x)) <= r by Th12;

          now

            per cases by A2, XXREAL_0: 1;

              case ( dist (p,x)) < r;

              hence x in ( Ball (p,r)) by A1, Th11;

            end;

              case ( dist (p,x)) = r;

              hence x in ( Sphere (p,r)) by A1, Th13;

            end;

          end;

          hence x in (( Sphere (p,r)) \/ ( Ball (p,r))) by XBOOLE_0:def 3;

        end;

        hence thesis by SUBSET_1: 2;

      end;

        suppose

         A3: M is empty;

        then ( Ball (p,r)) is empty & ( cl_Ball (p,r)) is empty;

        hence thesis by A3, Def16;

      end;

    end;

    theorem :: METRIC_1:17

    for M be non empty MetrStruct, p be Element of M holds ( Ball (p,r)) = { q where q be Element of M : ( dist (p,q)) < r } by Def14;

    theorem :: METRIC_1:18

    for M be non empty MetrStruct, p be Element of M holds ( cl_Ball (p,r)) = { q where q be Element of M : ( dist (p,q)) <= r } by Def15;

    theorem :: METRIC_1:19

    for M be non empty MetrStruct, p be Element of M holds ( Sphere (p,r)) = { q where q be Element of M : ( dist (p,q)) = r } by Def16;

    begin

    theorem :: METRIC_1:20

    for x be set holds ( Empty^2-to-zero . (x,x)) = 0

    proof

      let x be set;

      per cases ;

        suppose [x, x] in [:1, 1:];

        hence thesis by CARD_1: 49, FUNCT_2: 50;

      end;

        suppose not [x, x] in [:1, 1:];

        then not [x, x] in ( dom Empty^2-to-zero );

        hence thesis by FUNCT_1:def 2;

      end;

    end;

    theorem :: METRIC_1:21

    

     Th21: for x,y be Element of 1 st x <> y holds 0 < ( Empty^2-to-zero . (x,y))

    proof

      let x,y be Element of 1;

      x = {} by CARD_1: 49, TARSKI:def 1;

      hence thesis by CARD_1: 49, TARSKI:def 1;

    end;

    theorem :: METRIC_1:22

    

     Th22: for x,y be Element of 1 holds ( Empty^2-to-zero . (x,y)) = ( Empty^2-to-zero . (y,x)) by Lm4;

    theorem :: METRIC_1:23

    

     Th23: for x,y,z be Element of 1 holds ( Empty^2-to-zero . (x,z)) <= (( Empty^2-to-zero . (x,y)) + ( Empty^2-to-zero . (y,z))) by Lm5;

    theorem :: METRIC_1:24

    

     Th24: for x,y,z be Element of 1 holds ( Empty^2-to-zero . (x,z)) <= ( max (( Empty^2-to-zero . (x,y)),( Empty^2-to-zero . (y,z))))

    proof

      let x,y,z be Element of 1;

      

       A1: z = {} by CARD_1: 49, TARSKI:def 1;

      x = {} & y = {} by CARD_1: 49, TARSKI:def 1;

      hence thesis by A1;

    end;

    set M0 = MetrStruct (# 1, Empty^2-to-zero #);

    definition

      let A be non empty set;

      let f be Function of [:A, A:], REAL ;

      :: METRIC_1:def17

      attr f is Discerning means for a,b be Element of A holds a <> b implies 0 < (f . (a,b));

    end

    definition

      let M be non empty MetrStruct;

      :: METRIC_1:def18

      attr M is Discerning means the distance of M is Discerning;

    end

    theorem :: METRIC_1:25

    

     Th25: for M be non empty MetrStruct holds (for a,b be Element of M holds a <> b implies 0 < ( dist (a,b))) iff M is Discerning

    proof

      let M be non empty MetrStruct;

      hereby

        assume

         A1: for a,b be Element of M st a <> b holds 0 < ( dist (a,b));

        the distance of M is Discerning

        proof

          let a,b be Element of M;

          assume a <> b;

          then 0 < ( dist (a,b)) by A1;

          hence thesis;

        end;

        hence M is Discerning;

      end;

      assume M is Discerning;

      then the distance of M is Discerning;

      hence thesis;

    end;

    registration

      cluster MetrStruct (# 1, Empty^2-to-zero #) -> non empty;

      coherence ;

    end

    registration

      cluster MetrStruct (# 1, Empty^2-to-zero #) -> Reflexive symmetric Discerning triangle;

      coherence

      proof

        

         A1: for x be Element of M0 holds ( dist (x,x)) = 0 by Lm3;

        

         A2: for x,y be Element of M0 holds ( dist (x,y)) = ( dist (y,x)) by Th22;

        

         A3: for x,y be Element of M0 st x <> y holds 0 < ( dist (x,y)) by Th21;

        for x,y,z be Element of M0 holds ( dist (x,z)) <= (( dist (x,y)) + ( dist (y,z))) by Th23;

        hence thesis by A2, A1, A3, Th25, Th1, Th3, Th4;

      end;

    end

    definition

      let M be non empty MetrStruct;

      :: METRIC_1:def19

      attr M is ultra means

      : Def19: for a,b,c be Element of M holds ( dist (a,c)) <= ( max (( dist (a,b)),( dist (b,c))));

    end

    registration

      cluster strict ultra Reflexive symmetric Discerning triangle for non empty MetrStruct;

      existence

      proof

        take M0 = MetrStruct (# 1, Empty^2-to-zero #);

        M0 is ultra by Th24;

        hence thesis;

      end;

    end

    theorem :: METRIC_1:26

    

     Th26: for M be Reflexive Discerning non empty MetrStruct, a,b be Element of M holds 0 <= ( dist (a,b))

    proof

      let M be Reflexive Discerning non empty MetrStruct;

      let a,b be Element of M;

      now

        per cases ;

          suppose a = b;

          hence thesis by Th1;

        end;

          suppose a <> b;

          hence thesis by Th25;

        end;

      end;

      hence thesis;

    end;

    definition

      mode PseudoMetricSpace is Reflexive symmetric triangle non empty MetrStruct;

      mode SemiMetricSpace is Reflexive Discerning symmetric non empty MetrStruct;

      mode NonSymmetricMetricSpace is Reflexive Discerning triangle non empty MetrStruct;

      mode UltraMetricSpace is ultra Reflexive symmetric Discerning non empty MetrStruct;

    end

    registration

      cluster -> Discerning for non empty MetrSpace;

      coherence

      proof

        let M be non empty MetrSpace;

        for a,b be Element of M holds a <> b implies 0 < ( dist (a,b)) by Th7;

        hence thesis by Th25;

      end;

    end

    registration

      cluster -> triangle discerning for UltraMetricSpace;

      coherence

      proof

        let M be UltraMetricSpace;

        now

          let x,y,z be Element of M;

          thus ( dist (x,y)) = 0 iff x = y by Th25, Th1;

          thus ( dist (x,y)) = ( dist (y,x));

           0 <= ( dist (x,y)) & 0 <= ( dist (y,z)) by Th26;

          then

           A1: ( max (( dist (x,y)),( dist (y,z)))) <= (( dist (x,y)) + ( dist (y,z))) by SQUARE_1: 2;

          ( dist (x,z)) <= ( max (( dist (x,y)),( dist (y,z)))) by Def19;

          hence ( dist (x,z)) <= (( dist (x,y)) + ( dist (y,z))) by A1, XXREAL_0: 2;

        end;

        hence thesis by Th6;

      end;

    end

    definition

      :: METRIC_1:def20

      func Set_to_zero -> Function of [:2, 2:], REAL equals ( [:2, 2:] --> 0 );

      coherence

      proof

        ( [:2, 2:] --> ( In ( 0 , REAL ))) is Function of [:2, 2:], REAL ;

        hence thesis;

      end;

    end

    theorem :: METRIC_1:27

    

     Th27: for x,y be Element of 2 holds ( Set_to_zero . (x,y)) = 0 by ZFMISC_1: 87, FUNCOP_1: 7;

    theorem :: METRIC_1:28

    

     Th28: for x,y be Element of 2 holds ( Set_to_zero . (x,y)) = ( Set_to_zero . (y,x))

    proof

      let x,y be Element of 2;

      ( Set_to_zero . (x,y)) = 0 by Th27

      .= ( Set_to_zero . (y,x)) by Th27;

      hence thesis;

    end;

    theorem :: METRIC_1:29

    

     Th29: for x,y,z be Element of 2 holds ( Set_to_zero . (x,z)) <= (( Set_to_zero . (x,y)) + ( Set_to_zero . (y,z)))

    proof

      let x,y,z be Element of 2;

      ( Set_to_zero . (x,y)) = 0 & ( Set_to_zero . (y,z)) = 0 by Th27;

      hence thesis by Th27;

    end;

    definition

      :: METRIC_1:def21

      func ZeroSpace -> MetrStruct equals MetrStruct (# 2, Set_to_zero #);

      coherence ;

    end

    registration

      cluster ZeroSpace -> strict non empty;

      coherence ;

    end

    registration

      cluster ZeroSpace -> Reflexive symmetric triangle;

      coherence

      proof

        set M = MetrStruct (# 2, Set_to_zero #);

        

         A1: for x,y,z be Element of M holds ( dist (x,y)) = ( dist (y,x)) & ( dist (x,z)) <= (( dist (x,y)) + ( dist (y,z))) by Th28, Th29;

        for x be Element of M holds ( dist (x,x)) = 0 by Th27;

        hence thesis by A1, Th1, Th3, Th4;

      end;

    end

    definition

      let S be MetrStruct, p,q,r be Element of S;

      :: METRIC_1:def22

      pred q is_between p,r means p <> q & p <> r & q <> r & ( dist (p,r)) = (( dist (p,q)) + ( dist (q,r)));

    end

    theorem :: METRIC_1:30

    for S be symmetric triangle Reflexive non empty MetrStruct, p,q,r be Element of S holds q is_between (p,r) implies q is_between (r,p)

    proof

      let S be symmetric triangle Reflexive non empty MetrStruct, p,q,r be Element of S;

      assume

       A1: q is_between (p,r);

      hence r <> q & r <> p & q <> p;

      ( dist (p,r)) = (( dist (p,q)) + ( dist (q,r))) by A1;

      hence thesis;

    end;

    theorem :: METRIC_1:31

    for S be MetrSpace, p,q,r be Element of S st q is_between (p,r) holds ( not p is_between (q,r)) & not r is_between (p,q)

    proof

      let S be MetrSpace, p,q,r be Element of S;

      assume

       A1: q is_between (p,r);

      then

       A2: ( dist (p,r)) = (( dist (p,q)) + ( dist (q,r)));

      thus not p is_between (q,r) by A2, Th7;

      assume r is_between (p,q);

      then

       A3: ( dist (p,q)) = ((( dist (p,q)) + ( dist (q,r))) + ( dist (r,q))) by A2;

      q <> r by A1;

      hence contradiction by A3, Th7;

    end;

    theorem :: METRIC_1:32

    for S be MetrSpace, p,q,r,s be Element of S st q is_between (p,r) & r is_between (p,s) holds q is_between (p,s) & r is_between (q,s)

    proof

      let S be MetrSpace, p,q,r,s be Element of S;

      assume

       A1: q is_between (p,r);

      then

       A2: p <> q;

      assume

       A3: r is_between (p,s);

      then

       A4: p <> s & r <> s;

      ( dist (p,r)) = (( dist (p,q)) + ( dist (q,r))) by A1;

      then

       A5: ( dist (p,s)) = ((( dist (p,q)) + ( dist (q,r))) + ( dist (r,s))) by A3;

      ( dist (p,s)) <= (( dist (p,q)) + ( dist (q,s))) & (( dist (p,q)) + ( dist (q,s))) <= ((( dist (q,r)) + ( dist (r,s))) + ( dist (p,q))) by Th4, XREAL_1: 6;

      then

       A6: (( dist (p,q)) + ( dist (q,s))) = (( dist (p,q)) + (( dist (q,r)) + ( dist (r,s)))) by A5, XXREAL_0: 1;

      

       A7: q <> r by A1;

      then q <> s by A5, Th7;

      hence thesis by A2, A7, A4, A5, A6;

    end;

    definition

      let M be non empty MetrStruct, p,r be Element of M;

      :: METRIC_1:def23

      func open_dist_Segment (p,r) -> Subset of M equals { q where q be Element of M : q is_between (p,r) };

      coherence

      proof

        defpred X[ Element of M] means $1 is_between (p,r);

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

        hence thesis;

      end;

    end

    theorem :: METRIC_1:33

    for M be non empty MetrSpace, p,r,x be Element of M holds x in ( open_dist_Segment (p,r)) iff x is_between (p,r)

    proof

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

      x in ( open_dist_Segment (p,r)) implies x is_between (p,r)

      proof

        assume x in ( open_dist_Segment (p,r));

        then ex q be Element of M st x = q & q is_between (p,r);

        hence thesis;

      end;

      hence thesis;

    end;

    definition

      let M be non empty MetrStruct, p,r be Element of M;

      :: METRIC_1:def24

      func close_dist_Segment (p,r) -> Subset of M equals ({ q where q be Element of M : q is_between (p,r) } \/ {p, r});

      coherence

      proof

        defpred X[ Element of M] means $1 is_between (p,r);

        

         A1: {p, r} c= the carrier of M by ZFMISC_1: 32;

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

        hence thesis by A1, XBOOLE_1: 8;

      end;

    end

    theorem :: METRIC_1:34

    for M be non empty MetrStruct, p,r,x be Element of M holds x in ( close_dist_Segment (p,r)) iff (x is_between (p,r) or x = p or x = r)

    proof

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

      

       A1: x in ( close_dist_Segment (p,r)) implies (x is_between (p,r) or x = p or x = r)

      proof

        assume x in ( close_dist_Segment (p,r));

        then x in { q where q be Element of M : q is_between (p,r) } or x in {p, r} by XBOOLE_0:def 3;

        then (ex q be Element of M st x = q & q is_between (p,r)) or (x = p or x = r) by TARSKI:def 2;

        hence thesis;

      end;

      now

        assume x is_between (p,r) or x = p or x = r;

        then x in { q where q be Element of M : q is_between (p,r) } or x in {p, r} by TARSKI:def 2;

        hence x in ( close_dist_Segment (p,r)) by XBOOLE_0:def 3;

      end;

      hence thesis by A1;

    end;