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

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 b₁ being Function of [:A,A:], REAL st
for a, b being Element of A holds b₁ . a,b = (G . a,b) / (1 + (G . a,b))

proof end;

uniqueness
for b₁, b₂ being Function of [:A,A:], REAL st ( for a, b being Element of A holds b₁ . a,b = (G . a,b) / (1 + (G . a,b)) ) & ( for a, b being Element of A holds b₂ . a,b = (G . a,b) / (1 + (G . a,b)) ) holds
b₁ = b₂

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, b₃ being Function of [:A,A:], REAL holds
( b₃ = bounded_metric A,G iff for a, b being Element of A holds b₃ . 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 b₁ being Real_Sequence st
for n being Element of NAT holds b₁ . n = dist (S . n),x

proof end;

uniqueness
for b₁, b₂ being Real_Sequence st ( for n being Element of NAT holds b₁ . n = dist (S . n),x ) & ( for n being Element of NAT holds b₂ . n = dist (S . n),x ) holds
b₁ = b₂

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 b₄ being Real_Sequence holds
( b₄ = dist_to_point S,x iff for n being Element of NAT holds b₄ . 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 b₁ being Real_Sequence st
for n being Element of NAT holds b₁ . n = dist (S . n),(T . n)

proof end;

uniqueness
for b₁, b₂ being Real_Sequence st ( for n being Element of NAT holds b₁ . n = dist (S . n),(T . n) ) & ( for n being Element of NAT holds b₂ . n = dist (S . n),(T . n) ) holds
b₁ = b₂

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 b₄ being Real_Sequence holds
( b₄ = sequence_of_dist S,T iff for n being Element of NAT holds b₄ . 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 Th31, Th30, 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 V9 -> convergent M5( NAT ,the carrier of M);
coherence
for b₁ being sequence of M st b₁ is constant holds
b₁ is convergent by Th38;
cluster Cauchy -> bounded M5( NAT ,the carrier of M);
coherence
for b₁ being sequence of M st b₁ is Cauchy holds
b₁ is bounded by Th44;

end;

registration

let M be non empty MetrSpace;
cluster V9 convergent Cauchy bounded M5( NAT ,the carrier of M);
existence
ex b₁ being sequence of M st
( b₁ is constant & b₁ is convergent & b₁ is Cauchy & b₁ is bounded )

proof end;

end;