:: Sequences in Metric Spaces :: by Stanis{\l}awa Kanas and Adam Lecko :: :: Received December 12, 1991 :: Copyright (c) 1991-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, METRIC_1, SUBSET_1, XBOOLE_0, FUNCT_1, ZFMISC_1, REAL_1, COMPLEX1, ARYTM_1, XXREAL_0, ARYTM_3, PCOMPS_1, CARD_1, RELAT_1, RELAT_2, STRUCT_0, NAT_1, ORDINAL2, XXREAL_2, TARSKI, SEQ_2, SEQ_1, VALUED_0, BHSP_3, METRIC_6, FUNCT_7; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, RELAT_1, FUNCT_1, FUNCT_2, BINOP_1, DOMAIN_1, REAL_1, NAT_1, STRUCT_0, METRIC_1, SEQ_1, SEQ_2, VALUED_0, PCOMPS_1, TBSP_1, XXREAL_0, RECDEF_1; constructors DOMAIN_1, REAL_1, COMPLEX1, SEQ_2, PCOMPS_1, TBSP_1, RECDEF_1, RELSET_1, RVSUM_1, COMSEQ_2, BINOP_1, NUMBERS; registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, XREAL_0, STRUCT_0, METRIC_1, VALUED_0, FUNCT_2, TBSP_1, NAT_1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin :: Preliminaries 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 |.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, G; func bounded_metric(A,G) -> Function of [:A,A:],REAL means :: METRIC_6:def 1 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 sequence of NAT; theorem :: METRIC_6:7 for x ex S st rng S = {x}; definition let X be non empty MetrStruct; let S be sequence of X; let x be Element of X; pred S is_convergent_in_metrspace_to x means :: METRIC_6:def 2 for r st 0 < r 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; redefine attr V is bounded means :: METRIC_6:def 3 ex r being Real, x being Element of X st 0 < r & V c= Ball(x,r); end; definition let X be non empty MetrStruct; let S be sequence of X; attr S is bounded means :: METRIC_6:def 4 ex r being Real, x being Element of X st 0 < r & rng S c= Ball(x,r); end; definition let X, V, S; pred V contains_almost_all_sequence S means :: METRIC_6:def 5 ex m st for n st m <= n holds S.n in V; end; theorem :: METRIC_6:8 S is bounded iff ex r,x st (0 < r & for n holds S.n in Ball(x,r)); theorem :: METRIC_6:9 S is_convergent_in_metrspace_to x implies S is convergent; theorem :: METRIC_6:10 S is convergent implies ex x st S is_convergent_in_metrspace_to x; definition let X, S, x; func dist_to_point(S,x) -> Real_Sequence means :: METRIC_6:def 6 for n holds it.n = dist(S.n,x); end; definition let X, S, T; func sequence_of_dist(S,T) -> Real_Sequence means :: METRIC_6:def 7 for n holds it.n = dist(S.n,T.n); end; theorem :: METRIC_6:11 S is_convergent_in_metrspace_to x implies lim S = x; theorem :: METRIC_6:12 S is_convergent_in_metrspace_to x iff S is convergent & lim S = x; theorem :: METRIC_6:13 S is convergent implies ex x st S is_convergent_in_metrspace_to x & lim S = x ; theorem :: METRIC_6:14 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:15 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:16 (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:17 (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:18 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: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; 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 ; theorem :: METRIC_6:21 S is convergent & T is convergent implies dist(lim S,lim T) = lim sequence_of_dist(S,T); theorem :: METRIC_6:22 S is_convergent_in_metrspace_to x & S is_convergent_in_metrspace_to y implies x = y; theorem :: METRIC_6:23 S is constant implies S is convergent; theorem :: METRIC_6:24 S is_convergent_in_metrspace_to x & S1 is subsequence of S implies S1 is_convergent_in_metrspace_to x; theorem :: METRIC_6:25 S is Cauchy & S1 is subsequence of S implies S1 is Cauchy; theorem :: METRIC_6:26 S is constant implies S is Cauchy; theorem :: METRIC_6:27 S is convergent implies S is bounded; theorem :: METRIC_6:28 S is Cauchy implies S is bounded; registration let M be non empty MetrSpace; cluster constant -> convergent for sequence of M; cluster Cauchy -> bounded for sequence of M; end; registration let M be non empty MetrSpace; cluster constant convergent Cauchy bounded for sequence of M; end; :: missing, 2011.08.01, A.T. theorem :: METRIC_6:29 for X being symmetric triangle non empty Reflexive MetrStruct, V being bounded Subset of X, x being Element of X ex r being Real st 0 < r & V c= Ball(x,r);