:: Sequences in Metric Spaces
:: by Stanis{\l}awa Kanas and Adam Lecko
::
:: Received December 12, 1991
:: Copyright (c) 1991-2026 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 :: redefines bounded (TBSP_1, definition)
: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<r and
A4: for x,y being Element of X st x in V & y in V holds dist(x,y)
<=r by A1;
reconsider dr=2*r as Real;
take s=dr,x;
thus 0 < s by A3,XREAL_1:129;
thus V c= Ball(x,s)
proof
let u be object;
assume
A5: u in V;
then reconsider v = u as Element of X;
A6: 1*r < s by A3,XREAL_1:68;
dist(x,v) <= r by A4,A2,A5;
then dist(x,v) < s by A6,XXREAL_0:2;
hence thesis by METRIC_1:11;
end;
end;
suppose
A7: V = {};
set x = the Element of X;
reconsider jd=1/2 as Real;
take r=jd,x;
thus 0 < r & V c= Ball(x,r) by A7;
end;
end;
given r be Real,x be Element of X such that
A8: 0 < r and
A9: V c= Ball(x,r);
take 2*r;
thus 2*r > 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;