:: Sequences in Metric Spaces :: by Stanis{\l}awa Kanas and Adam Lecko :: :: Received December 12, 1991 :: Copyright (c) 1991-2017 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; definitions TBSP_1, TARSKI; expansions TBSP_1, TARSKI; theorems ABSVALUE, BINOP_1, METRIC_1, FUNCT_1, FUNCT_2, SEQ_2, NAT_1, PCOMPS_1, SEQM_3, SEQ_4, TBSP_1, SUBSET_1, XCMPLX_1, XREAL_1, COMPLEX1, XXREAL_0, VALUED_0, ORDINAL1; schemes SEQ_1, BINOP_1; 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 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 Th2: G is_metric_of A implies for a,b being 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 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 being 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 being 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 being 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 being 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 being 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,def 3,def 4,def 5; hence thesis by PCOMPS_1:def 6; end; hence thesis by A1; end; theorem for X being 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 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)) proof A1: (G is Reflexive discerning & for a,b,c being 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 being Element of A holds G.(b,c) <= G.(a,b) + G.(a,c); A4: for b,c being 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 being 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 ,def 5; hence thesis by Th3; end; G is_metric_of A implies (G is Reflexive discerning & for a,b,c being 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; func bounded_metric(A,G) -> Function of [:A,A:],REAL means :Def1: for a,b being 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 being Function of [:A,A:],REAL such that A1: for a,b being 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 being Element of A holds f1.(a,b) = G.(a,b)/(1 + G.(a,b)) and A3: for a,b being Element of A holds f2.(a,b) = G.(a,b)/(1 + G.(a,b)); for a,b being 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 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 being 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 being 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 being 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; :: 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 Th7: for x 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; pred S is_convergent_in_metrspace_to x means 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 :Def3: ex r being Real, x being 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 being Element of X such that A2: x in V by SUBSET_1:4; consider r such that A3: 0 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; attr S is bounded means 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 :Def5: ex m st for n st m <= n holds S.n in V; end; theorem 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 being 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 being 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 being 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 S is_convergent_in_metrspace_to x implies S is convergent; theorem 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 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; 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 being Real_Sequence such that A1: for n being 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; 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 being Real_Sequence such that A1: for n being 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 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 ex m st for n st m <= n holds dist(S.n, x) < r; hence thesis by TBSP_1:def 3; end; theorem Th12: S is_convergent_in_metrspace_to x iff S is convergent & lim S = x by TBSP_1:def 3,Th11; theorem 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 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 ex m being Nat st for n being 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 ex m st for n st m <= n holds dist(S.n,x) < r proof let r; assume 0 < r; then consider m1 being Nat such that A8: for n being 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 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 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 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 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 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 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 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 (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 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 ex m being Nat st for n being 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 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 being 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 Th23: S is constant implies S is convergent proof assume S is constant; then consider x such that A1: for n being 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 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 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 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 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 S is constant implies S is Cauchy by Th23,TBSP_1:5; theorem 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 being 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 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 being 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 being Real such that A5: 0 < r1 and A6: for m2 being 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 being 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; :: missing, 2011.08.01, A.T. theorem 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) proof let X be symmetric triangle non empty Reflexive MetrStruct, V be bounded Subset of X, y be Element of X; consider r being Real, x being 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;