:: 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);