Volume 3, 1991

University of Bialystok

Copyright (c) 1991 Association of Mizar Users

### 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;

Back to top