Journal of Formalized Mathematics
Volume 3, 1991
University of Bialystok
Copyright (c) 1991 Association of Mizar Users

### Sequences in Metric Spaces

by
Stanislawa Kanas, and

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;

```