metric_6.miz



    begin

    reserve X for MetrSpace,

x,y,z for Element of X,

A for non empty set,

G for Function of [:A, A:], REAL ,

f for Function,

k,n,m,m1,m2 for Nat,

q,r for Real;

    theorem :: METRIC_6:1

    

     Th1: |.(( dist (x,z)) - ( dist (y,z))).| <= ( dist (x,y))

    proof

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

      then (( dist (y,z)) - ( dist (x,z))) <= ( dist (x,y)) by XREAL_1: 20;

      then

       A1: ( - ( dist (x,y))) <= ( - (( dist (y,z)) - ( dist (x,z)))) by XREAL_1: 24;

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

      then (( dist (x,z)) - ( dist (y,z))) <= ( dist (x,y)) by XREAL_1: 20;

      hence thesis by A1, ABSVALUE: 5;

    end;

    theorem :: METRIC_6:2

    

     Th2: G is_metric_of A implies for a,b be Element of A holds 0 <= (G . (a,b))

    proof

      assume

       A1: G is_metric_of A;

      let a,b be Element of A;

      

       A2: ((1 / 2) * (G . (a,a))) = ((1 / 2) * 0 ) by A1, PCOMPS_1:def 6;

      (G . (a,b)) = ((1 / 2) * ((1 * (G . (a,b))) + (G . (a,b))))

      .= ((1 / 2) * ((G . (a,b)) + (G . (b,a)))) by A1, PCOMPS_1:def 6;

      hence thesis by A1, A2, PCOMPS_1:def 6;

    end;

    theorem :: METRIC_6:3

    

     Th3: G is_metric_of A iff G is Reflexive discerning symmetric triangle

    proof

      

       A1: G is_metric_of A implies G is Reflexive discerning symmetric triangle

      proof

        assume

         A2: G is_metric_of A;

        then for a be Element of A holds (G . (a,a)) = 0 by PCOMPS_1:def 6;

        hence G is Reflexive by METRIC_1:def 2;

        for a,b be Element of A holds (G . (a,b)) = 0 iff a = b by A2, PCOMPS_1:def 6;

        hence G is discerning by METRIC_1:def 3;

        for a,b be Element of A holds (G . (a,b)) = (G . (b,a)) by A2, PCOMPS_1:def 6;

        hence G is symmetric by METRIC_1:def 4;

        for a,b,c be Element of A holds (G . (a,c)) <= ((G . (a,b)) + (G . (b,c))) by A2, PCOMPS_1:def 6;

        hence thesis by METRIC_1:def 5;

      end;

      G is Reflexive discerning symmetric triangle implies G is_metric_of A

      proof

        assume G is Reflexive discerning & G is symmetric & G is triangle;

        then for a,b,c be Element of A holds ((G . (a,b)) = 0 iff a = b) & (G . (a,b)) = (G . (b,a)) & (G . (a,c)) <= ((G . (a,b)) + (G . (b,c))) by METRIC_1:def 2, METRIC_1:def 3, METRIC_1:def 4, METRIC_1:def 5;

        hence thesis by PCOMPS_1:def 6;

      end;

      hence thesis by A1;

    end;

    theorem :: METRIC_6:4

    for X be strict non empty MetrSpace holds the distance of X is Reflexive discerning symmetric triangle

    proof

      let X be strict non empty MetrSpace;

      

       A1: the distance of X is_metric_of the carrier of X by PCOMPS_1: 35;

      hence the distance of X is Reflexive by Th3;

      thus the distance of X is discerning by A1, Th3;

      thus the distance of X is symmetric by A1, Th3;

      thus thesis by A1, Th3;

    end;

    theorem :: METRIC_6:5

    G is_metric_of A iff (G is Reflexive discerning & for a,b,c be Element of A holds (G . (b,c)) <= ((G . (a,b)) + (G . (a,c))))

    proof

      

       A1: (G is Reflexive discerning & for a,b,c be Element of A holds (G . (b,c)) <= ((G . (a,b)) + (G . (a,c)))) implies G is_metric_of A

      proof

        assume that

         A2: G is Reflexive discerning and

         A3: for a,b,c be Element of A holds (G . (b,c)) <= ((G . (a,b)) + (G . (a,c)));

        

         A4: for b,c be Element of A holds (G . (b,c)) = (G . (c,b))

        proof

          let b,c be Element of A;

          (G . (c,b)) <= ((G . (b,c)) + (G . (b,b))) by A3;

          then

           A5: (G . (c,b)) <= ((G . (b,c)) + 0 ) by A2, METRIC_1:def 2;

          (G . (b,c)) <= ((G . (c,b)) + (G . (c,c))) by A3;

          then (G . (b,c)) <= ((G . (c,b)) + 0 ) by A2, METRIC_1:def 2;

          hence thesis by A5, XXREAL_0: 1;

        end;

        for a,b,c be Element of A holds (G . (a,c)) <= ((G . (a,b)) + (G . (b,c)))

        proof

          let a,b,c be Element of A;

          (G . (a,c)) <= ((G . (b,a)) + (G . (b,c))) by A3;

          hence thesis by A4;

        end;

        then G is Reflexive discerning symmetric triangle by A2, A4, METRIC_1:def 4, METRIC_1:def 5;

        hence thesis by Th3;

      end;

      G is_metric_of A implies (G is Reflexive discerning & for a,b,c be Element of A holds (G . (b,c)) <= ((G . (a,b)) + (G . (a,c))))

      proof

        assume

         A6: G is_metric_of A;

        then

         A7: G is Reflexive discerning symmetric triangle by Th3;

        now

          let a,b,c be Element of A;

          (G . (b,c)) <= ((G . (b,a)) + (G . (a,c))) by A7, METRIC_1:def 5;

          hence (G . (b,c)) <= ((G . (a,b)) + (G . (a,c))) by A7, METRIC_1:def 4;

        end;

        hence thesis by A6, Th3;

      end;

      hence thesis by A1;

    end;

    definition

      let A, G;

      :: METRIC_6:def1

      func bounded_metric (A,G) -> Function of [:A, A:], REAL means

      : Def1: for a,b be Element of A holds (it . (a,b)) = ((G . (a,b)) / (1 + (G . (a,b))));

      existence

      proof

        deffunc H( Element of A, Element of A) = ( In (((G . ($1,$2)) / (1 + (G . ($1,$2)))), REAL ));

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

         A1: for a,b be Element of A holds (F . (a,b)) = H(a,b) from BINOP_1:sch 4;

        take F;

        let a,b be Element of A;

        (F . (a,b)) = H(a,b) by A1;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be Function of [:A, A:], REAL ;

        assume that

         A2: for a,b be Element of A holds (f1 . (a,b)) = ((G . (a,b)) / (1 + (G . (a,b)))) and

         A3: for a,b be Element of A holds (f2 . (a,b)) = ((G . (a,b)) / (1 + (G . (a,b))));

        for a,b be Element of A holds (f1 . (a,b)) = (f2 . (a,b))

        proof

          let a,b be Element of A;

          (f1 . (a,b)) = ((G . (a,b)) / (1 + (G . (a,b)))) by A2;

          hence thesis by A3;

        end;

        hence thesis by BINOP_1: 2;

      end;

    end

    theorem :: METRIC_6:6

    G is_metric_of A implies ( bounded_metric (A,G)) is_metric_of A

    proof

      assume

       A1: G is_metric_of A;

      

       A2: for a,b,c be Element of A holds (( bounded_metric (A,G)) . (a,c)) <= ((( bounded_metric (A,G)) . (a,b)) + (( bounded_metric (A,G)) . (b,c)))

      proof

        let a,b,c be Element of A;

        set a1 = (G . (a,b));

        set a3 = (G . (a,c));

        set a5 = (G . (b,c));

        

         A3: (( bounded_metric (A,G)) . (a,b)) = ((G . (a,b)) / (1 + (G . (a,b)))) & (( bounded_metric (A,G)) . (a,c)) = ((G . (a,c)) / (1 + (G . (a,c)))) by Def1;

        

         A4: (( bounded_metric (A,G)) . (b,c)) = ((G . (b,c)) / (1 + (G . (b,c)))) by Def1;

        

         A5: a3 >= 0 by A1, Th2;

        

         A6: 0 <= (G . (a,b)) & 0 <= (G . (b,c)) by A1, Th2;

        then

         A7: 0 <> ((1 + a1) * (1 + a5)) by XCMPLX_1: 6;

        

         A8: ((a1 / (1 + a1)) + (a5 / (1 + a5))) = (((a1 * (1 + a5)) + (a5 * (1 + a1))) / ((1 + a1) * (1 + a5))) by A6, XCMPLX_1: 116

        .= ((((a1 * 1) + (a1 * a5)) + ((a5 * 1) + (a5 * a1))) / ((1 + a1) * (1 + a5)));

         0 <= (G . (a,c)) by A1, Th2;

        then

         A9: (((a1 / (1 + a1)) + (a5 / (1 + a5))) - (a3 / (1 + a3))) = (((((a1 + (a1 * a5)) + (a5 + (a5 * a1))) * (1 + a3)) - (a3 * ((1 + a1) * (1 + a5)))) / (((1 + a1) * (1 + a5)) * (1 + a3))) by A7, A8, XCMPLX_1: 130;

        

         A10: a1 >= 0 & a5 >= 0 by A1, Th2;

        a3 <= (a1 + a5) by A1, PCOMPS_1:def 6;

        then ((a1 + a5) - a3) >= 0 by XREAL_1: 48;

        then (((a5 + a1) - a3) + ((a1 * a5) + ((a5 * a1) + ((a5 * a1) * a3)))) >= 0 by A10, A5;

        hence thesis by A3, A4, A9, A10, A5, XREAL_1: 49;

      end;

      

       A11: for a,b be Element of A holds ((( bounded_metric (A,G)) . (a,b)) = 0 iff a = b)

      proof

        let a,b be Element of A;

        

         A12: (( bounded_metric (A,G)) . (a,b)) = 0 implies a = b

        proof

          assume (( bounded_metric (A,G)) . (a,b)) = 0 ;

          then

           A13: ((G . (a,b)) / (1 + (G . (a,b)))) = 0 by Def1;

           0 <= (G . (a,b)) by A1, Th2;

          then (G . (a,b)) = 0 by A13, XCMPLX_1: 50;

          hence thesis by A1, PCOMPS_1:def 6;

        end;

        a = b implies (( bounded_metric (A,G)) . (a,b)) = 0

        proof

          assume a = b;

          then (G . (a,b)) = 0 by A1, PCOMPS_1:def 6;

          then ((G . (a,b)) / (1 + (G . (a,b)))) = 0 ;

          hence thesis by Def1;

        end;

        hence thesis by A12;

      end;

      for a,b be Element of A holds (( bounded_metric (A,G)) . (a,b)) = (( bounded_metric (A,G)) . (b,a))

      proof

        let a,b be Element of A;

        ((G . (a,b)) / (1 + (G . (a,b)))) = ((G . (b,a)) / (1 + (G . (a,b)))) by A1, PCOMPS_1:def 6

        .= ((G . (b,a)) / (1 + (G . (b,a)))) by A1, PCOMPS_1:def 6

        .= (( bounded_metric (A,G)) . (b,a)) by Def1;

        hence thesis by Def1;

      end;

      hence thesis by A11, A2, PCOMPS_1:def 6;

    end;

    reserve X for non empty MetrSpace,

x,y for Element of X,

V for Subset of X,

S,S1,T for sequence of X,

Nseq for increasing sequence of NAT ;

    theorem :: METRIC_6:7

    

     Th7: for x holds ex S st ( rng S) = {x}

    proof

      let x;

      consider f such that

       A1: ( dom f) = NAT and

       A2: ( rng f) = {x} by FUNCT_1: 5;

      reconsider f as sequence of X by A1, A2, FUNCT_2: 2;

      take f;

      thus thesis by A2;

    end;

    definition

      let X be non empty MetrStruct;

      let S be sequence of X;

      let x be Element of X;

      :: METRIC_6:def2

      pred S is_convergent_in_metrspace_to x means for r st 0 < r holds ex m st for n st m <= n holds ( dist ((S . n),x)) < r;

    end

    definition

      let X be symmetric triangle non empty MetrStruct;

      let V be Subset of X;

      :: original: bounded

      redefine

      :: METRIC_6:def3

      attr V is bounded means

      : Def3: ex r be Real, x be Element of X st 0 < r & V c= ( Ball (x,r));

      compatibility

      proof

        hereby

          assume

           A1: V is bounded;

          per cases ;

            suppose V <> {} ;

            then

            consider x be Element of X such that

             A2: x in V by SUBSET_1: 4;

            consider r such that

             A3: 0 < r and

             A4: for x,y be Element of X st x in V & y in V holds ( dist (x,y)) <= r by A1;

            reconsider dr = (2 * r) as Real;

            take s = dr, x;

            thus 0 < s by A3, XREAL_1: 129;

            thus V c= ( Ball (x,s))

            proof

              let u be object;

              assume

               A5: u in V;

              then

              reconsider v = u as Element of X;

              

               A6: (1 * r) < s by A3, XREAL_1: 68;

              ( dist (x,v)) <= r by A4, A2, A5;

              then ( dist (x,v)) < s by A6, XXREAL_0: 2;

              hence thesis by METRIC_1: 11;

            end;

          end;

            suppose

             A7: V = {} ;

            set x = the Element of X;

            reconsider jd = (1 / 2) as Real;

            take r = jd, x;

            thus 0 < r & V c= ( Ball (x,r)) by A7;

          end;

        end;

        given r be Real, x be Element of X such that

         A8: 0 < r and

         A9: V c= ( Ball (x,r));

        take (2 * r);

        thus (2 * r) > 0 by A8, XREAL_1: 129;

        let z,y be Element of X;

        assume

         A10: z in V;

        assume y in V;

        then

         A11: ( dist (x,y)) < r by A9, METRIC_1: 11;

        ( dist (x,z)) < r by A9, A10, METRIC_1: 11;

        then

         A12: (( dist (z,x)) + ( dist (x,y))) <= (r + r) by A11, XREAL_1: 7;

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

        hence ( dist (z,y)) <= (2 * r) by A12, XXREAL_0: 2;

      end;

    end

    definition

      let X be non empty MetrStruct;

      let S be sequence of X;

      :: METRIC_6:def4

      attr S is bounded means ex r be Real, x be Element of X st 0 < r & ( rng S) c= ( Ball (x,r));

    end

    definition

      let X, V, S;

      :: METRIC_6:def5

      pred V contains_almost_all_sequence S means

      : Def5: ex m st for n st m <= n holds (S . n) in V;

    end

    theorem :: METRIC_6:8

    

     Th8: S is bounded iff ex r, x st ( 0 < r & for n holds (S . n) in ( Ball (x,r)))

    proof

      thus S is bounded implies ex r, x st ( 0 < r & for n holds (S . n) in ( Ball (x,r)))

      proof

        assume S is bounded;

        then

        consider r be Real, x such that

         A1: 0 < r and

         A2: ( rng S) c= ( Ball (x,r));

        take q = r;

        take y = x;

        now

          let n;

          n in NAT by ORDINAL1:def 12;

          then (S . n) in ( rng S) by FUNCT_2: 4;

          hence (S . n) in ( Ball (y,q)) by A2;

        end;

        hence thesis by A1;

      end;

      thus (ex r, x st ( 0 < r & for n holds (S . n) in ( Ball (x,r)))) implies S is bounded

      proof

        given r, x such that

         A3: 0 < r and

         A4: for n holds (S . n) in ( Ball (x,r));

        reconsider r as Real;

        for x1 be object holds x1 in ( rng S) implies x1 in ( Ball (x,r))

        proof

          let x1 be object;

          assume x1 in ( rng S);

          then

          consider x2 be object such that

           A5: x2 in ( dom S) and

           A6: x1 = (S . x2) by FUNCT_1:def 3;

          x2 in NAT by A5, FUNCT_2:def 1;

          hence thesis by A4, A6;

        end;

        then ( rng S) c= ( Ball (x,r));

        hence thesis by A3;

      end;

    end;

    theorem :: METRIC_6:9

    S is_convergent_in_metrspace_to x implies S is convergent;

    theorem :: METRIC_6:10

    

     Th10: S is convergent implies ex x st S is_convergent_in_metrspace_to x

    proof

      assume S is convergent;

      then

      consider x such that

       A1: for r st 0 < r holds ex m st for n st m <= n holds ( dist ((S . n),x)) < r;

      S is_convergent_in_metrspace_to x by A1;

      hence thesis;

    end;

    definition

      let X, S, x;

      :: METRIC_6:def6

      func dist_to_point (S,x) -> Real_Sequence means

      : Def6: for n holds (it . n) = ( dist ((S . n),x));

      existence

      proof

        deffunc F( Nat) = ( dist ((S . $1),x));

        consider seq be Real_Sequence such that

         A1: for n be Nat holds (seq . n) = F(n) from SEQ_1:sch 1;

        take seq;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let seq1,seq2 be Real_Sequence;

        assume that

         A2: for n holds (seq1 . n) = ( dist ((S . n),x)) and

         A3: for n holds (seq2 . n) = ( dist ((S . n),x));

        now

          let n be Element of NAT ;

          (seq1 . n) = ( dist ((S . n),x)) by A2;

          hence (seq1 . n) = (seq2 . n) by A3;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    definition

      let X, S, T;

      :: METRIC_6:def7

      func sequence_of_dist (S,T) -> Real_Sequence means

      : Def7: for n holds (it . n) = ( dist ((S . n),(T . n)));

      existence

      proof

        deffunc F( Nat) = ( dist ((S . $1),(T . $1)));

        consider seq be Real_Sequence such that

         A1: for n be Nat holds (seq . n) = F(n) from SEQ_1:sch 1;

        take seq;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let seq1,seq2 be Real_Sequence;

        assume that

         A2: for n holds (seq1 . n) = ( dist ((S . n),(T . n))) and

         A3: for n holds (seq2 . n) = ( dist ((S . n),(T . n)));

        now

          let n be Element of NAT ;

          (seq1 . n) = ( dist ((S . n),(T . n))) by A2;

          hence (seq1 . n) = (seq2 . n) by A3;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    theorem :: METRIC_6:11

    

     Th11: S is_convergent_in_metrspace_to x implies ( lim S) = x

    proof

      assume S is_convergent_in_metrspace_to x;

      then S is convergent & for r st 0 < r holds ex m st for n st m <= n holds ( dist ((S . n),x)) < r;

      hence thesis by TBSP_1:def 3;

    end;

    theorem :: METRIC_6:12

    

     Th12: S is_convergent_in_metrspace_to x iff S is convergent & ( lim S) = x by TBSP_1:def 3, Th11;

    theorem :: METRIC_6:13

    

     Th13: S is convergent implies ex x st S is_convergent_in_metrspace_to x & ( lim S) = x

    proof

      assume S is convergent;

      then ex x st S is_convergent_in_metrspace_to x by Th10;

      hence thesis by Th11;

    end;

    theorem :: METRIC_6:14

    

     Th14: S is_convergent_in_metrspace_to x iff ( dist_to_point (S,x)) is convergent & ( lim ( dist_to_point (S,x))) = 0

    proof

      

       A1: S is_convergent_in_metrspace_to x implies ( dist_to_point (S,x)) is convergent & ( lim ( dist_to_point (S,x))) = 0

      proof

        assume

         A2: S is_convergent_in_metrspace_to x;

        

         A3: for r be Real st 0 < r holds ex m be Nat st for n be Nat st m <= n holds |.((( dist_to_point (S,x)) . n) - 0 ).| < r

        proof

          let r be Real;

          assume

           A4: 0 < r;

          reconsider r as Real;

          consider m1 such that

           A5: for n st m1 <= n holds ( dist ((S . n),x)) < r by A2, A4;

          take k = m1;

          let n be Nat;

          assume k <= n;

          then ( dist ((S . n),x)) < r by A5;

          then

           A6: (( dist_to_point (S,x)) . n) < r by Def6;

          ( dist ((S . n),x)) = (( dist_to_point (S,x)) . n) by Def6;

          then 0 <= (( dist_to_point (S,x)) . n) by METRIC_1: 5;

          hence thesis by A6, ABSVALUE:def 1;

        end;

        then ( dist_to_point (S,x)) is convergent by SEQ_2:def 6;

        hence thesis by A3, SEQ_2:def 7;

      end;

      ( dist_to_point (S,x)) is convergent & ( lim ( dist_to_point (S,x))) = 0 implies S is_convergent_in_metrspace_to x

      proof

        assume

         A7: ( dist_to_point (S,x)) is convergent & ( lim ( dist_to_point (S,x))) = 0 ;

        for r st 0 < r holds ex m st for n st m <= n holds ( dist ((S . n),x)) < r

        proof

          let r;

          assume 0 < r;

          then

          consider m1 be Nat such that

           A8: for n be Nat st m1 <= n holds |.((( dist_to_point (S,x)) . n) - 0 ).| < r by A7, SEQ_2:def 7;

          reconsider k = m1 as Element of NAT by ORDINAL1:def 12;

          take k;

          let n;

          assume k <= n;

          then |.((( dist_to_point (S,x)) . n) - 0 ).| < r by A8;

          then

           A9: |.( dist ((S . n),x)).| < r by Def6;

           0 <= ( dist ((S . n),x)) by METRIC_1: 5;

          hence thesis by A9, ABSVALUE:def 1;

        end;

        hence thesis;

      end;

      hence thesis by A1;

    end;

    theorem :: METRIC_6:15

    

     Th15: S is_convergent_in_metrspace_to x implies for r st 0 < r holds ( Ball (x,r)) contains_almost_all_sequence S

    proof

      assume

       A1: S is_convergent_in_metrspace_to x;

      thus for r st 0 < r holds ( Ball (x,r)) contains_almost_all_sequence S

      proof

        let r such that

         A2: 0 < r;

        ex m st for n st m <= n holds (S . n) in ( Ball (x,r))

        proof

          consider m1 such that

           A3: for n st m1 <= n holds ( dist ((S . n),x)) < r by A1, A2;

          take k = m1;

          now

            let n;

            assume k <= n;

            then ( dist (x,(S . n))) < r by A3;

            hence (S . n) in ( Ball (x,r)) by METRIC_1: 11;

          end;

          hence thesis;

        end;

        hence thesis;

      end;

    end;

    theorem :: METRIC_6:16

    

     Th16: (for r st 0 < r holds ( Ball (x,r)) contains_almost_all_sequence S) implies for V st x in V & V in ( Family_open_set X) holds V contains_almost_all_sequence S

    proof

      assume

       A1: for r st 0 < r holds ( Ball (x,r)) contains_almost_all_sequence S;

      

       A2: for r st 0 < r holds ex m st for n st m <= n holds (S . n) in ( Ball (x,r)) by A1, Def5;

      thus for V st x in V & V in ( Family_open_set X) holds V contains_almost_all_sequence S

      proof

        let V;

        assume x in V & V in ( Family_open_set X);

        then

        consider q such that

         A3: 0 < q and

         A4: ( Ball (x,q)) c= V by PCOMPS_1:def 4;

        consider m1 such that

         A5: for n st m1 <= n holds (S . n) in ( Ball (x,q)) by A2, A3;

        for n st m1 <= n holds (S . n) in V by A4, A5;

        hence thesis;

      end;

    end;

    theorem :: METRIC_6:17

    

     Th17: (for V st x in V & V in ( Family_open_set X) holds V contains_almost_all_sequence S) implies S is_convergent_in_metrspace_to x

    proof

      

       A1: for r st 0 < r holds x in ( Ball (x,r))

      proof

        let r;

        assume 0 < r;

        then ( dist (x,x)) < r by METRIC_1: 1;

        hence thesis by METRIC_1: 11;

      end;

      assume

       A2: for V st x in V & V in ( Family_open_set X) holds V contains_almost_all_sequence S;

      for r st 0 < r holds ex m st for n st m <= n holds ( dist ((S . n),x)) < r

      proof

        let r;

        assume 0 < r;

        then x in ( Ball (x,r)) by A1;

        then ( Ball (x,r)) contains_almost_all_sequence S by A2, PCOMPS_1: 29;

        then

        consider m1 such that

         A3: for n st m1 <= n holds (S . n) in ( Ball (x,r));

        take k = m1;

        let n;

        assume k <= n;

        then (S . n) in ( Ball (x,r)) by A3;

        hence thesis by METRIC_1: 11;

      end;

      hence thesis;

    end;

    theorem :: METRIC_6:18

    S is_convergent_in_metrspace_to x iff for r st 0 < r holds ( Ball (x,r)) contains_almost_all_sequence S

    proof

      thus S is_convergent_in_metrspace_to x implies for r st 0 < r holds ( Ball (x,r)) contains_almost_all_sequence S by Th15;

      thus (for r st 0 < r holds ( Ball (x,r)) contains_almost_all_sequence S) implies S is_convergent_in_metrspace_to x

      proof

        assume for r st 0 < r holds ( Ball (x,r)) contains_almost_all_sequence S;

        then for V st x in V & V in ( Family_open_set X) holds V contains_almost_all_sequence S by Th16;

        hence thesis by Th17;

      end;

    end;

    theorem :: METRIC_6:19

    S is_convergent_in_metrspace_to x iff for V st x in V & V in ( Family_open_set X) holds V contains_almost_all_sequence S

    proof

      thus S is_convergent_in_metrspace_to x implies for V st x in V & V in ( Family_open_set X) holds V contains_almost_all_sequence S

      proof

        assume S is_convergent_in_metrspace_to x;

        then for r st 0 < r holds ( Ball (x,r)) contains_almost_all_sequence S by Th15;

        hence thesis by Th16;

      end;

      thus thesis by Th17;

    end;

    theorem :: METRIC_6:20

    (for r st 0 < r holds ( Ball (x,r)) contains_almost_all_sequence S) iff for V st x in V & V in ( Family_open_set X) holds V contains_almost_all_sequence S by Th15, Th16, Th17;

    theorem :: METRIC_6:21

    

     Th21: S is convergent & T is convergent implies ( dist (( lim S),( lim T))) = ( lim ( sequence_of_dist (S,T)))

    proof

      assume that

       A1: S is convergent and

       A2: T is convergent;

      consider x such that

       A3: S is_convergent_in_metrspace_to x and

       A4: ( lim S) = x by A1, Th13;

      consider y such that

       A5: T is_convergent_in_metrspace_to y and

       A6: ( lim T) = y by A2, Th13;

      

       A7: for r be Real st 0 < r holds ex m be Nat st for n be Nat st m <= n holds |.((( sequence_of_dist (S,T)) . n) - ( dist (x,y))).| < r

      proof

        let r be Real;

        assume

         A8: 0 < r;

        reconsider r as Real;

        

         A9: 0 < (r / 2) by A8, XREAL_1: 215;

        then

        consider m1 such that

         A10: for n st m1 <= n holds ( dist ((S . n),x)) < (r / 2) by A3;

        consider m2 such that

         A11: for n st m2 <= n holds ( dist ((T . n),y)) < (r / 2) by A5, A9;

        reconsider k = (m1 + m2) as Nat;

        take k;

        let n be Nat such that

         A12: k <= n;

         |.(( dist ((S . n),(T . n))) - ( dist (x,(T . n)))).| <= ( dist ((S . n),x)) & |.(( dist ((T . n),x)) - ( dist (y,x))).| <= ( dist ((T . n),y)) by Th1;

        then

         A13: ( |.(( dist ((S . n),(T . n))) - ( dist ((T . n),x))).| + |.(( dist ((T . n),x)) - ( dist (x,y))).|) <= (( dist ((S . n),x)) + ( dist ((T . n),y))) by XREAL_1: 7;

         |.((( sequence_of_dist (S,T)) . n) - ( dist (( lim S),( lim T)))).| = |.(( dist ((S . n),(T . n))) - ( dist (x,y))).| by A4, A6, Def7

        .= |.((( dist ((S . n),(T . n))) - ( dist ((T . n),x))) + (( dist ((T . n),x)) - ( dist (x,y)))).|;

        then |.((( sequence_of_dist (S,T)) . n) - ( dist (( lim S),( lim T)))).| <= ( |.(( dist ((S . n),(T . n))) - ( dist ((T . n),x))).| + |.(( dist ((T . n),x)) - ( dist (x,y))).|) by COMPLEX1: 56;

        then

         A14: |.((( sequence_of_dist (S,T)) . n) - ( dist (( lim S),( lim T)))).| <= (( dist ((S . n),x)) + ( dist ((T . n),y))) by A13, XXREAL_0: 2;

        m2 <= k by NAT_1: 12;

        then m2 <= n by A12, XXREAL_0: 2;

        then

         A15: ( dist ((T . n),y)) < (r / 2) by A11;

        m1 <= k by NAT_1: 11;

        then m1 <= n by A12, XXREAL_0: 2;

        then ( dist ((S . n),x)) < (r / 2) by A10;

        then (( dist ((S . n),x)) + ( dist ((T . n),y))) < ((r / 2) + (r / 2)) by A15, XREAL_1: 8;

        hence thesis by A4, A6, A14, XXREAL_0: 2;

      end;

      then ( sequence_of_dist (S,T)) is convergent by SEQ_2:def 6;

      hence thesis by A4, A6, A7, SEQ_2:def 7;

    end;

    theorem :: METRIC_6:22

    S is_convergent_in_metrspace_to x & S is_convergent_in_metrspace_to y implies x = y

    proof

      assume that

       A1: S is_convergent_in_metrspace_to x and

       A2: S is_convergent_in_metrspace_to y;

      

       A3: ( lim S) = y by A2, Th12;

      

       A4: for n be Nat holds (( sequence_of_dist (S,S)) . n) = ( In ( 0 , REAL ))

      proof

        let n be Nat;

        (( sequence_of_dist (S,S)) . n) = ( dist ((S . n),(S . n))) by Def7

        .= 0 by METRIC_1: 1;

        hence thesis;

      end;

      

       A5: ex n st (( sequence_of_dist (S,S)) . n) = 0

      proof

        take 0 ;

        thus thesis by A4;

      end;

      ( lim S) = x & S is convergent by A1, Th12;

      then

       A6: ( dist (x,y)) = ( lim ( sequence_of_dist (S,S))) by A3, Th21;

      ( sequence_of_dist (S,S)) is constant by A4, VALUED_0:def 18;

      then ( dist (x,y)) = 0 by A6, A5, SEQ_4: 25;

      hence thesis by METRIC_1: 2;

    end;

    theorem :: METRIC_6:23

    

     Th23: S is constant implies S is convergent

    proof

      assume S is constant;

      then

      consider x such that

       A1: for n be Nat holds (S . n) = x by VALUED_0:def 18;

      take x;

      let r such that

       A2: 0 < r;

      take k = 0 ;

      now

        let n such that k <= n;

        ( dist ((S . n),x)) = ( dist (x,x)) by A1

        .= 0 by METRIC_1: 1;

        hence ( dist ((S . n),x)) < r by A2;

      end;

      hence for n st k <= n holds ( dist ((S . n),x)) < r;

    end;

    theorem :: METRIC_6:24

    S is_convergent_in_metrspace_to x & S1 is subsequence of S implies S1 is_convergent_in_metrspace_to x

    proof

      assume that

       A1: S is_convergent_in_metrspace_to x and

       A2: S1 is subsequence of S;

      consider Nseq such that

       A3: S1 = (S * Nseq) by A2, VALUED_0:def 17;

      for r st 0 < r holds ex m st for n st m <= n holds ( dist ((S1 . n),x)) < r

      proof

        let r;

        assume 0 < r;

        then

        consider m1 such that

         A4: for n st m1 <= n holds ( dist ((S . n),x)) < r by A1;

        take m = m1;

        for n st m <= n holds ( dist ((S1 . n),x)) < r

        proof

          let n such that

           A5: m <= n;

          

           A6: n in NAT by ORDINAL1:def 12;

          ( dom S) = NAT by FUNCT_2:def 1;

          then ( dom Nseq) = NAT & (Nseq . n) in ( dom S) by FUNCT_2:def 1;

          then n in ( dom (S * Nseq)) by FUNCT_1: 11, A6;

          then

           A7: (S1 . n) = (S . (Nseq . n)) by A3, FUNCT_1: 12;

          n <= (Nseq . n) by SEQM_3: 14;

          then m1 <= (Nseq . n) by A5, XXREAL_0: 2;

          hence thesis by A4, A7;

        end;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: METRIC_6:25

    S is Cauchy & S1 is subsequence of S implies S1 is Cauchy

    proof

      assume that

       A1: S is Cauchy and

       A2: S1 is subsequence of S;

      consider Nseq such that

       A3: S1 = (S * Nseq) by A2, VALUED_0:def 17;

      for r st 0 < r holds ex m st for n, k st m <= n & m <= k holds ( dist ((S1 . n),(S1 . k))) < r

      proof

        let r;

        assume 0 < r;

        then

        consider m1 such that

         A4: for n, k st m1 <= n & m1 <= k holds ( dist ((S . n),(S . k))) < r by A1;

        take m = m1;

        for n, k st m <= n & m <= k holds ( dist ((S1 . n),(S1 . k))) < r

        proof

          let n, k such that

           A5: m <= n and

           A6: m <= k;

          k <= (Nseq . k) by SEQM_3: 14;

          then

           A7: m1 <= (Nseq . k) by A6, XXREAL_0: 2;

          

           A8: k in NAT by ORDINAL1:def 12;

          

           A9: n in NAT by ORDINAL1:def 12;

          ( dom S) = NAT by FUNCT_2:def 1;

          then ( dom Nseq) = NAT & (Nseq . k) in ( dom S) by FUNCT_2:def 1;

          then k in ( dom (S * Nseq)) by FUNCT_1: 11, A8;

          then

           A10: (S1 . k) = (S . (Nseq . k)) by A3, FUNCT_1: 12;

          ( dom S) = NAT by FUNCT_2:def 1;

          then ( dom Nseq) = NAT & (Nseq . n) in ( dom S) by FUNCT_2:def 1;

          then n in ( dom (S * Nseq)) by FUNCT_1: 11, A9;

          then

           A11: (S1 . n) = (S . (Nseq . n)) by A3, FUNCT_1: 12;

          n <= (Nseq . n) by SEQM_3: 14;

          then m1 <= (Nseq . n) by A5, XXREAL_0: 2;

          hence thesis by A4, A11, A7, A10;

        end;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: METRIC_6:26

    S is constant implies S is Cauchy by Th23, TBSP_1: 5;

    theorem :: METRIC_6:27

    S is convergent implies S is bounded

    proof

      assume S is convergent;

      then

      consider x such that

       A1: S is_convergent_in_metrspace_to x and ( lim S) = x by Th13;

      ( dist_to_point (S,x)) is convergent by A1, Th14;

      then ( dist_to_point (S,x)) is bounded by SEQ_2: 13;

      then

      consider r be Real such that

       A2: 0 < r and

       A3: for n be Nat holds |.(( dist_to_point (S,x)) . n).| < r by SEQ_2: 3;

      reconsider r as Real;

      for n holds (S . n) in ( Ball (x,r))

      proof

        let n;

        

         A4: (( dist_to_point (S,x)) . n) = ( dist ((S . n),x)) by Def6;

        then 0 <= (( dist_to_point (S,x)) . n) by METRIC_1: 5;

        then |.(( dist_to_point (S,x)) . n).| = (( dist_to_point (S,x)) . n) by ABSVALUE:def 1;

        then ( dist ((S . n),x)) < r by A3, A4;

        hence thesis by METRIC_1: 11;

      end;

      hence thesis by A2, Th8;

    end;

    theorem :: METRIC_6:28

    

     Th28: S is Cauchy implies S is bounded

    proof

      assume

       A1: S is Cauchy;

      now

        take r = 1;

        thus 0 < r;

        consider m1 such that

         A2: for n, k st m1 <= n & m1 <= k holds ( dist ((S . n),(S . k))) < r by A1;

        take m = m1;

        thus for n, k st m <= n & m <= k holds ( dist ((S . n),(S . k))) < r by A2;

      end;

      then

      consider r2 be Real, m1 such that

       A3: 0 < r2 and

       A4: for n, k st m1 <= n & m1 <= k holds ( dist ((S . n),(S . k))) < r2;

      consider r1 be Real such that

       A5: 0 < r1 and

       A6: for m2 be Nat st m2 <= m1 holds |.(( dist_to_point (S,(S . m1))) . m2).| < r1 by SEQ_2: 4;

      

       A7: for m st m <= m1 holds ( dist ((S . m),(S . m1))) < r1

      proof

        let m such that

         A8: m <= m1;

        

         A9: (( dist_to_point (S,(S . m1))) . m) = ( dist ((S . m),(S . m1))) by Def6;

        then 0 <= (( dist_to_point (S,(S . m1))) . m) by METRIC_1: 5;

        then |.(( dist_to_point (S,(S . m1))) . m).| = ( dist ((S . m),(S . m1))) by A9, ABSVALUE:def 1;

        hence thesis by A6, A8;

      end;

      ex r, x st 0 < r & for n holds (S . n) in ( Ball (x,r))

      proof

        reconsider r = (r1 + r2) as Real;

        take r;

        take x = (S . m1);

        for n holds (S . n) in ( Ball (x,r))

        proof

          let n;

          now

            per cases ;

              suppose

               A10: n <= m1;

              

               A11: r1 < r by A3, XREAL_1: 29;

              ( dist ((S . n),(S . m1))) < r1 by A7, A10;

              then ( dist ((S . n),x)) < r by A11, XXREAL_0: 2;

              hence thesis by METRIC_1: 11;

            end;

              suppose

               A12: m1 <= n;

              

               A13: r2 < r by A5, XREAL_1: 29;

              ( dist ((S . n),(S . m1))) < r2 by A4, A12;

              then ( dist ((S . n),x)) < r by A13, XXREAL_0: 2;

              hence thesis by METRIC_1: 11;

            end;

          end;

          hence thesis;

        end;

        hence thesis by A3, A5;

      end;

      hence thesis by Th8;

    end;

    registration

      let M be non empty MetrSpace;

      cluster constant -> convergent for sequence of M;

      coherence by Th23;

      cluster Cauchy -> bounded for sequence of M;

      coherence by Th28;

    end

    registration

      let M be non empty MetrSpace;

      cluster constant convergent Cauchy bounded for sequence of M;

      existence

      proof

        set x = the Element of M;

        consider S be sequence of M such that

         A1: ( rng S) = {x} by Th7;

        take S;

        thus

         A2: S is constant by A1, FUNCT_2: 111;

        hence S is convergent;

        thus S is Cauchy by A2;

        thus thesis by A2;

      end;

    end

    theorem :: METRIC_6:29

    for X be symmetric triangle non empty Reflexive MetrStruct, V be bounded Subset of X, x be Element of X holds ex r be Real st 0 < r & V c= ( Ball (x,r))

    proof

      let X be symmetric triangle non empty Reflexive MetrStruct, V be bounded Subset of X, y be Element of X;

      consider r be Real, x be Element of X such that

       A1: 0 < r and

       A2: V c= ( Ball (x,r)) by Def3;

      take s = (r + ( dist (x,y)));

      ( dist (x,y)) >= 0 by METRIC_1: 5;

      then s >= (r + 0 ) by XREAL_1: 7;

      hence 0 < s by A1;

      let e be object;

      assume

       A3: e in V;

      then

      reconsider e as Element of X;

      e in ( Ball (x,r)) by A3, A2;

      then ( dist (e,x)) < r by METRIC_1: 11;

      then

       A4: (( dist (e,x)) + ( dist (x,y))) < (r + ( dist (x,y))) by XREAL_1: 8;

      ( dist (e,y)) <= (( dist (e,x)) + ( dist (x,y))) by METRIC_1: 4;

      then ( dist (e,y)) < (r + ( dist (x,y))) by A4, XXREAL_0: 2;

      then e in ( Ball (y,s)) by METRIC_1: 11;

      hence thesis;

    end;