:: 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 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 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 b₁ being sequence of M st b₁ is constant holds
b₁ 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 b₁ being sequence of M st b₁ is Cauchy holds
b₁ 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 b₁ being sequence of M st
( b₁ is constant & b₁ is convergent & b₁ is Cauchy & b₁ is bounded )

proof end;

end;