The abstract of the Mizar article:

Sequences in Metric Spaces

by

Stanislawa Kanas, and

Adam Lecko

Received December 12, 1991

MML identifier: METRIC_6

[ Mizar article, MML identifier index ]

environ

 vocabulary METRIC_1, FUNCT_1, ABSVALUE, ARYTM_1, PCOMPS_1, ARYTM_3, RELAT_2,
      NORMSP_1, ORDINAL2, SEQM_3, RELAT_1, LATTICES, BOOLE, SEQ_2, SEQ_1,
      BHSP_3, METRIC_6, ARYTM;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
      XREAL_0, ABSVALUE, RELAT_1, FUNCT_1, FUNCT_2, STRUCT_0, REAL_1, METRIC_1,
      SEQ_1, SEQ_2, SEQM_3, PCOMPS_1, NAT_1, TBSP_1, NORMSP_1, BHSP_3;
 constructors ABSVALUE, REAL_1, SEQ_2, PCOMPS_1, NAT_1, TBSP_1, BHSP_3,
      MEMBERED, XBOOLE_0;
 clusters METRIC_1, STRUCT_0, XREAL_0, RELSET_1, SEQM_3, ARYTM_3, SEQ_1,
      MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin :: Preliminaries

 reserve X for MetrSpace,
         x,y,z for Element of X,
         A for non empty set,
         a for Element of A,
         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
   abs(dist(x,z) - dist(y,z)) <= dist(x,y);

theorem :: METRIC_6:2
   G is_metric_of A implies
       (for a,b being Element of A holds 0 <= G.(a,b));

theorem :: METRIC_6:3
  G is_metric_of A iff G is Reflexive discerning symmetric triangle;

theorem :: METRIC_6:4
    for X being strict non empty MetrSpace holds
  the distance of X is Reflexive discerning symmetric triangle;

theorem :: METRIC_6:5
    G is_metric_of A iff (G is Reflexive discerning &
  for a,b,c being Element of A holds G.(b,c) <= G.(a,b) + G.(a,c));

definition let A; let G;
 canceled 3;

  func bounded_metric(A,G) -> Function of [:A,A:],REAL means
:: METRIC_6:def 4
   for a,b being Element of A holds
        it.(a,b) = G.(a,b)/(1 + G.(a,b));
end;

theorem :: METRIC_6:6
    G is_metric_of A implies bounded_metric(A,G) is_metric_of A;

:: Sequences

 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 Seq_of_Nat,
         F for Function of NAT, the carrier of X;

canceled;

theorem :: METRIC_6:8
    F is sequence of X iff
  for a st a in NAT holds F.a is Element of X;

canceled;

theorem :: METRIC_6:10
  for x ex S st rng S = {x};

definition let X; let S; let x;
 canceled 3;

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

definition let X; let V be Subset of X;
  redefine canceled;

attr V is bounded means
:: METRIC_6:def 10
      ex r,x st 0 < r & V c= Ball(x,r);
end;

definition let X; let S;
  attr S is bounded means
:: METRIC_6:def 11
    ex r,x st 0 < r & rng S c= Ball(x,r);
end;

definition let X; let V; let S;
  pred V contains_almost_all_sequence S means
:: METRIC_6:def 12
    ex m st for n st m <= n holds S.n in V;
end;

canceled 9;

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

theorem :: METRIC_6:21
    S is_convergent_in_metrspace_to x implies
         S is convergent;

theorem :: METRIC_6:22
    S is convergent implies
         ex x st S is_convergent_in_metrspace_to x;

definition let X; let S; let x;
 canceled;

  func dist_to_point(S,x) -> Real_Sequence means
:: METRIC_6:def 14
    for n holds it.n = dist(S.n,x);
end;

definition let X; let S; let T;
  func sequence_of_dist(S,T) -> Real_Sequence means
:: METRIC_6:def 15
    for n holds it.n = dist(S.n,T.n);
end;

definition let X; let S;
  assume  S is convergent;
  func lim S -> Element of X means
:: METRIC_6:def 16
    for r st 0 < r ex m st for n st m <= n holds dist(S.n,it) < r;
end;

canceled 3;

theorem :: METRIC_6:26
   S is_convergent_in_metrspace_to x implies lim S = x;

theorem :: METRIC_6:27
   S is_convergent_in_metrspace_to x iff (S is convergent & lim S = x);

theorem :: METRIC_6:28
    S is convergent implies
          (ex x st S is_convergent_in_metrspace_to x & lim S = x);

theorem :: METRIC_6:29
   S is_convergent_in_metrspace_to x iff
       (dist_to_point(S,x) is convergent & lim dist_to_point(S,x) = 0);

theorem :: METRIC_6:30
   S is_convergent_in_metrspace_to x implies
        (for r st 0 < r holds Ball(x,r) contains_almost_all_sequence S);

theorem :: METRIC_6:31
   (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);

theorem :: METRIC_6:32
   (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;

theorem :: METRIC_6:33
    S is_convergent_in_metrspace_to x iff
  (for r st 0 < r holds Ball(x,r) contains_almost_all_sequence S);

theorem :: METRIC_6:34
    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);

theorem :: METRIC_6:35
     (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);

theorem :: METRIC_6:36
   (S is convergent & T is convergent) implies
           dist(lim S,lim T) = lim sequence_of_dist(S,T);

theorem :: METRIC_6:37
    (S is_convergent_in_metrspace_to x & S is_convergent_in_metrspace_to y)
              implies x = y;

theorem :: METRIC_6:38
   S is constant implies S is convergent;

theorem :: METRIC_6:39
    S is_convergent_in_metrspace_to x & S1 is_subsequence_of S implies
        S1 is_convergent_in_metrspace_to x;

theorem :: METRIC_6:40
    S is Cauchy & S1 is_subsequence_of S implies S1 is Cauchy;

canceled;

theorem :: METRIC_6:42
    S is constant implies S is Cauchy;

theorem :: METRIC_6:43
    S is convergent implies S is bounded;

theorem :: METRIC_6:44
  S is Cauchy implies S is bounded;

definition let M be non empty MetrSpace;
  cluster constant -> convergent sequence of M;
  cluster convergent -> Cauchy sequence of M;
  cluster Cauchy -> bounded sequence of M;
end;

definition let M be non empty MetrSpace;
  cluster constant convergent Cauchy bounded sequence of M;
end;