:: Sequences in Metric Spaces
:: by Stanis{\l}awa Kanas and Adam Lecko
::
:: Received December 12, 1991
:: Copyright (c) 1991-2011 Association of Mizar Users


begin

theorem Th1: :: METRIC_6:1
for X being MetrSpace
for x, z, y being Element of X holds abs ((dist (x,z)) - (dist (y,z))) <= dist (x,y)
proof end;

theorem Th2: :: METRIC_6:2
for A being non empty set
for G being Function of [:A,A:],REAL st G is_metric_of A holds
for a, b being Element of A holds 0 <= G . (a,b)
proof end;

theorem Th3: :: METRIC_6:3
for A being non empty set
for G being Function of [:A,A:],REAL holds
( G is_metric_of A iff ( G is Reflexive & G is discerning & G is symmetric & G is triangle ) )
proof end;

theorem :: METRIC_6:4
for X being non empty strict MetrSpace holds
( the distance of X is Reflexive & the distance of X is discerning & the distance of X is symmetric & the distance of X is triangle )
proof end;

theorem :: METRIC_6:5
for A being non empty set
for G being Function of [:A,A:],REAL holds
( G is_metric_of A iff ( G is Reflexive & G is discerning & ( for a, b, c being Element of A holds G . (b,c) <= (G . (a,b)) + (G . (a,c)) ) ) )
proof end;

definition
let A be non empty set ;
let G be Function of [:A,A:],REAL;
canceled;
canceled;
canceled;
func bounded_metric (A,G) -> Function of [:A,A:],REAL means :Def4: :: METRIC_6:def 4
for a, b being Element of A holds it . (a,b) = (G . (a,b)) / (1 + (G . (a,b)));
existence
ex b1 being Function of [:A,A:],REAL st
for a, b being Element of A holds b1 . (a,b) = (G . (a,b)) / (1 + (G . (a,b)))
proof end;
uniqueness
for b1, b2 being Function of [:A,A:],REAL st ( for a, b being Element of A holds b1 . (a,b) = (G . (a,b)) / (1 + (G . (a,b))) ) & ( for a, b being Element of A holds b2 . (a,b) = (G . (a,b)) / (1 + (G . (a,b))) ) holds
b1 = b2
proof end;
end;

:: deftheorem METRIC_6:def 1 :
canceled;

:: deftheorem METRIC_6:def 2 :
canceled;

:: deftheorem METRIC_6:def 3 :
canceled;

:: deftheorem Def4 defines bounded_metric METRIC_6:def 4 :
for A being non empty set
for G, b3 being Function of [:A,A:],REAL holds
( b3 = bounded_metric (A,G) iff for a, b being Element of A holds b3 . (a,b) = (G . (a,b)) / (1 + (G . (a,b))) );

theorem :: METRIC_6:6
for A being non empty set
for G being Function of [:A,A:],REAL st G is_metric_of A holds
bounded_metric (A,G) is_metric_of A
proof end;

theorem :: METRIC_6:7
canceled;

theorem :: METRIC_6:8
canceled;

theorem :: METRIC_6:9
canceled;

theorem Th10: :: METRIC_6:10
for X being non empty MetrSpace
for x being Element of X ex S being sequence of X st rng S = {x}
proof end;

definition
let X be non empty MetrStruct ;
let S be sequence of X;
let x be Element of X;
canceled;
canceled;
canceled;
pred S is_convergent_in_metrspace_to x means :Def8: :: METRIC_6:def 8
for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
dist ((S . n),x) < r;
end;

:: deftheorem METRIC_6:def 5 :
canceled;

:: deftheorem METRIC_6:def 6 :
canceled;

:: deftheorem METRIC_6:def 7 :
canceled;

:: deftheorem Def8 defines is_convergent_in_metrspace_to METRIC_6:def 8 :
for X being non empty MetrStruct
for S being sequence of X
for x being Element of X holds
( S is_convergent_in_metrspace_to x iff for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
dist ((S . n),x) < r );

definition
let X be non empty symmetric triangle MetrStruct ;
let V be Subset of X;
canceled;
redefine attr V is bounded means :: METRIC_6:def 10
ex r being Real ex x being Element of X st
( 0 < r & V c= Ball (x,r) );
compatibility
( V is bounded iff ex r being Real ex x being Element of X st
( 0 < r & V c= Ball (x,r) ) )
proof end;
end;

:: deftheorem METRIC_6:def 9 :
canceled;

:: deftheorem defines bounded METRIC_6:def 10 :
for X being non empty symmetric triangle MetrStruct
for V being Subset of X holds
( V is bounded iff ex r being Real ex x being Element of X st
( 0 < r & V c= Ball (x,r) ) );

definition
let X be non empty MetrStruct ;
let S be sequence of X;
attr S is bounded means :Def11: :: METRIC_6:def 11
ex r being Real ex x being Element of X st
( 0 < r & rng S c= Ball (x,r) );
end;

:: deftheorem Def11 defines bounded METRIC_6:def 11 :
for X being non empty MetrStruct
for S being sequence of X holds
( S is bounded iff ex r being Real ex x being Element of X st
( 0 < r & rng S c= Ball (x,r) ) );

definition
let X be non empty MetrSpace;
let V be Subset of X;
let S be sequence of X;
pred V contains_almost_all_sequence S means :Def12: :: METRIC_6:def 12
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
S . n in V;
end;

:: deftheorem Def12 defines contains_almost_all_sequence METRIC_6:def 12 :
for X being non empty MetrSpace
for V being Subset of X
for S being sequence of X holds
( V contains_almost_all_sequence S iff ex m being Element of NAT st
for n being Element of NAT st m <= n holds
S . n in V );

theorem :: METRIC_6:11
canceled;

theorem :: METRIC_6:12
canceled;

theorem :: METRIC_6:13
canceled;

theorem :: METRIC_6:14
canceled;

theorem :: METRIC_6:15
canceled;

theorem :: METRIC_6:16
canceled;

theorem :: METRIC_6:17
canceled;

theorem :: METRIC_6:18
canceled;

theorem :: METRIC_6:19
canceled;

theorem Th20: :: METRIC_6:20
for X being non empty MetrSpace
for S being sequence of X holds
( S is bounded iff ex r being Real ex x being Element of X st
( 0 < r & ( for n being Element of NAT holds S . n in Ball (x,r) ) ) )
proof end;

theorem Th21: :: METRIC_6:21
for X being non empty MetrSpace
for x being Element of X
for S being sequence of X st S is_convergent_in_metrspace_to x holds
S is convergent
proof end;

theorem Th22: :: METRIC_6:22
for X being non empty MetrSpace
for S being sequence of X st S is convergent holds
ex x being Element of X st S is_convergent_in_metrspace_to x
proof end;

definition
let X be non empty MetrSpace;
let S be sequence of X;
let x be Element of X;
canceled;
func dist_to_point (S,x) -> Real_Sequence means :Def14: :: METRIC_6:def 14
for n being Element of NAT holds it . n = dist ((S . n),x);
existence
ex b1 being Real_Sequence st
for n being Element of NAT holds b1 . n = dist ((S . n),x)
proof end;
uniqueness
for b1, b2 being Real_Sequence st ( for n being Element of NAT holds b1 . n = dist ((S . n),x) ) & ( for n being Element of NAT holds b2 . n = dist ((S . n),x) ) holds
b1 = b2
proof end;
end;

:: deftheorem METRIC_6:def 13 :
canceled;

:: deftheorem Def14 defines dist_to_point METRIC_6:def 14 :
for X being non empty MetrSpace
for S being sequence of X
for x being Element of X
for b4 being Real_Sequence holds
( b4 = dist_to_point (S,x) iff for n being Element of NAT holds b4 . n = dist ((S . n),x) );

definition
let X be non empty MetrSpace;
let S, T be sequence of X;
func sequence_of_dist (S,T) -> Real_Sequence means :Def15: :: METRIC_6:def 15
for n being Element of NAT holds it . n = dist ((S . n),(T . n));
existence
ex b1 being Real_Sequence st
for n being Element of NAT holds b1 . n = dist ((S . n),(T . n))
proof end;
uniqueness
for b1, b2 being Real_Sequence st ( for n being Element of NAT holds b1 . n = dist ((S . n),(T . n)) ) & ( for n being Element of NAT holds b2 . n = dist ((S . n),(T . n)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines sequence_of_dist METRIC_6:def 15 :
for X being non empty MetrSpace
for S, T being sequence of X
for b4 being Real_Sequence holds
( b4 = sequence_of_dist (S,T) iff for n being Element of NAT holds b4 . n = dist ((S . n),(T . n)) );

theorem :: METRIC_6:23
canceled;

theorem :: METRIC_6:24
canceled;

theorem :: METRIC_6:25
canceled;

theorem Th26: :: METRIC_6:26
for X being non empty MetrSpace
for x being Element of X
for S being sequence of X st S is_convergent_in_metrspace_to x holds
lim S = x
proof end;

theorem Th27: :: METRIC_6:27
for X being non empty MetrSpace
for x being Element of X
for S being sequence of X holds
( S is_convergent_in_metrspace_to x iff ( S is convergent & lim S = x ) )
proof end;

theorem Th28: :: METRIC_6:28
for X being non empty MetrSpace
for S being sequence of X st S is convergent holds
ex x being Element of X st
( S is_convergent_in_metrspace_to x & lim S = x )
proof end;

theorem Th29: :: METRIC_6:29
for X being non empty MetrSpace
for x being Element of X
for S being sequence of X holds
( S is_convergent_in_metrspace_to x iff ( dist_to_point (S,x) is convergent & lim (dist_to_point (S,x)) = 0 ) )
proof end;

theorem Th30: :: METRIC_6:30
for X being non empty MetrSpace
for x being Element of X
for S being sequence of X st S is_convergent_in_metrspace_to x holds
for r being Real st 0 < r holds
Ball (x,r) contains_almost_all_sequence S
proof end;

theorem Th31: :: METRIC_6:31
for X being non empty MetrSpace
for x being Element of X
for S being sequence of X st ( for r being Real st 0 < r holds
Ball (x,r) contains_almost_all_sequence S ) holds
for V being Subset of X st x in V & V in Family_open_set X holds
V contains_almost_all_sequence S
proof end;

theorem Th32: :: METRIC_6:32
for X being non empty MetrSpace
for x being Element of X
for S being sequence of X st ( for V being Subset of X st x in V & V in Family_open_set X holds
V contains_almost_all_sequence S ) holds
S is_convergent_in_metrspace_to x
proof end;

theorem :: METRIC_6:33
for X being non empty MetrSpace
for x being Element of X
for S being sequence of X holds
( S is_convergent_in_metrspace_to x iff for r being Real st 0 < r holds
Ball (x,r) contains_almost_all_sequence S )
proof end;

theorem :: METRIC_6:34
for X being non empty MetrSpace
for x being Element of X
for S being sequence of X holds
( S is_convergent_in_metrspace_to x iff for V being Subset of X st x in V & V in Family_open_set X holds
V contains_almost_all_sequence S )
proof end;

theorem :: METRIC_6:35
for X being non empty MetrSpace
for x being Element of X
for S being sequence of X holds
( ( for r being Real st 0 < r holds
Ball (x,r) contains_almost_all_sequence S ) iff for V being Subset of X st x in V & V in Family_open_set X holds
V contains_almost_all_sequence S ) by Th30, Th31, Th32;

theorem Th36: :: METRIC_6:36
for X being non empty MetrSpace
for S, T being sequence of X st S is convergent & T is convergent holds
dist ((lim S),(lim T)) = lim (sequence_of_dist (S,T))
proof end;

theorem :: METRIC_6:37
for X being non empty MetrSpace
for x, y being Element of X
for S being sequence of X st S is_convergent_in_metrspace_to x & S is_convergent_in_metrspace_to y holds
x = y
proof end;

theorem Th38: :: METRIC_6:38
for X being non empty MetrSpace
for S being sequence of X st S is constant holds
S is convergent
proof end;

theorem :: METRIC_6:39
for X being non empty MetrSpace
for x being Element of X
for S, S1 being sequence of X st S is_convergent_in_metrspace_to x & S1 is subsequence of S holds
S1 is_convergent_in_metrspace_to x
proof end;

theorem :: METRIC_6:40
for X being non empty MetrSpace
for S, S1 being sequence of X st S is Cauchy & S1 is subsequence of S holds
S1 is Cauchy
proof end;

theorem :: METRIC_6:41
canceled;

theorem :: METRIC_6:42
for X being non empty MetrSpace
for S being sequence of X st S is constant holds
S is Cauchy by Th38, TBSP_1:7;

theorem :: METRIC_6:43
for X being non empty MetrSpace
for S being sequence of X st S is convergent holds
S is bounded
proof end;

theorem Th44: :: METRIC_6:44
for X being non empty MetrSpace
for S being sequence of X st S is Cauchy holds
S is bounded
proof end;

registration
let M be non empty MetrSpace;
cluster Function-like V11() V27( NAT , the carrier of M) -> convergent Element of bool [:NAT, the carrier of M:];
coherence
for b1 being sequence of M st b1 is constant holds
b1 is convergent
by Th38;
cluster Function-like V27( NAT , the carrier of M) Cauchy -> bounded Element of bool [:NAT, the carrier of M:];
coherence
for b1 being sequence of M st b1 is Cauchy holds
b1 is bounded
by Th44;
end;

registration
let M be non empty MetrSpace;
cluster Relation-like NAT -defined the carrier of M -valued Function-like V11() V27( NAT , the carrier of M) convergent Cauchy bounded Element of bool [:NAT, the carrier of M:];
existence
ex b1 being sequence of M st
( b1 is constant & b1 is convergent & b1 is Cauchy & b1 is bounded )
proof end;
end;