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


theorem Th1: :: METRIC_6:1
for X being MetrSpace
for x, y, z being Element of X holds |.((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;
func bounded_metric (A,G) -> Function of [:A,A:],REAL means :Def1: :: METRIC_6:def 1
 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 Def1 defines bounded_metric METRIC_6:def 1 :
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 Th7: :: METRIC_6:7
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;
pred S is_convergent_in_metrspace_to x means :: METRIC_6:def 2
 for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
dist ((S . n),x) < r;
end;

:: deftheorem defines is_convergent_in_metrspace_to METRIC_6:def 2 :
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 Nat st
for n being 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;
redefine attr V is bounded means :Def3: :: METRIC_6:def 3
 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 Def3 defines bounded METRIC_6:def 3 :
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 :: METRIC_6:def 4
 ex r being Real ex x being Element of X st
( 0 < r & rng S c= Ball (x,r) );
end;

:: deftheorem defines bounded METRIC_6:def 4 :
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 :Def5: :: METRIC_6:def 5
 ex m being Nat st
for n being Nat st m <= n holds
S . n in V;
end;

:: deftheorem Def5 defines contains_almost_all_sequence METRIC_6:def 5 :
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 Nat st
for n being Nat st m <= n holds
S . n in V );

theorem Th8: :: METRIC_6:8
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 Nat holds S . n in Ball (x,r) ) ) )
proof end;

theorem :: METRIC_6:9
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 ;

theorem Th10: :: METRIC_6:10
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;
func dist_to_point (S,x) -> Real_Sequence means :Def6: :: METRIC_6:def 6
 for n being Nat holds it . n = dist ((S . n),x);
existence
ex b1 being Real_Sequence st
for n being Nat holds b1 . n = dist ((S . n),x)
proof end;
uniqueness
for b1, b2 being Real_Sequence st ( for n being Nat holds b1 . n = dist ((S . n),x) ) & ( for n being Nat holds b2 . n = dist ((S . n),x) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines dist_to_point METRIC_6:def 6 :
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 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 :Def7: :: METRIC_6:def 7
 for n being Nat holds it . n = dist ((S . n),(T . n));
existence
ex b1 being Real_Sequence st
for n being Nat holds b1 . n = dist ((S . n),(T . n))
proof end;
uniqueness
for b1, b2 being Real_Sequence st ( for n being Nat holds b1 . n = dist ((S . n),(T . n)) ) & ( for n being Nat holds b2 . n = dist ((S . n),(T . n)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines sequence_of_dist METRIC_6:def 7 :
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 Nat holds b4 . n = dist ((S . n),(T . n)) );

theorem Th11: :: METRIC_6:11
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 Th12: :: METRIC_6:12
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 ) ) by TBSP_1:def 3, Th11;

theorem Th13: :: METRIC_6:13
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 Th14: :: METRIC_6:14
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 Th15: :: METRIC_6:15
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 Th16: :: METRIC_6:16
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 Th17: :: METRIC_6:17
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:18
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:19
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:20
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 Th15, Th16, Th17;

theorem Th21: :: METRIC_6:21
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:22
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 Th23: :: METRIC_6:23
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:24
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:25
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:26
for X being non empty MetrSpace
for S being sequence of X st S is constant holds
S is Cauchy by Th23, TBSP_1:5;

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

theorem Th28: :: METRIC_6:28
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 constant V33( NAT , the carrier of M) -> convergent for Element of bool [:NAT, the carrier of M:];
coherence
for b1 being sequence of M st b1 is constant holds
b1 is convergent by Th23;
cluster Function-like V33( NAT , the carrier of M) Cauchy -> bounded for Element of bool [:NAT, the carrier of M:];
coherence
for b1 being sequence of M st b1 is Cauchy holds
b1 is bounded by Th28;
end;

registration
let M be non empty MetrSpace;
cluster non empty Relation-like NAT -defined the carrier of M -valued Function-like constant V32( NAT ) V33( NAT , the carrier of M) convergent Cauchy bounded for 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;

:: missing, 2011.08.01, A.T.
theorem :: METRIC_6:29
for X being non empty Reflexive symmetric triangle MetrStruct
for V being bounded Subset of X
for x being Element of X ex r being Real st
( 0 < r & V c= Ball (x,r) )
proof end;