:: 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 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 Def1 defines bounded_metric METRIC_6:def 1 :
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 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 b₁ being Real_Sequence st
for n being Nat holds b₁ . n = dist ((S . n),x)

proof end;

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

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 b₄ being Real_Sequence holds
( b₄ = dist_to_point (S,x) iff for n being 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 :Def7: :: METRIC_6:def 7
for n being Nat holds it . n = dist ((S . n),(T . n));

existence
ex b₁ being Real_Sequence st
for n being Nat holds b₁ . n = dist ((S . n),(T . n))

proof end;

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

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 b₄ being Real_Sequence holds
( b₄ = sequence_of_dist (S,T) iff for n being Nat holds b₄ . 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 b₁ being sequence of M st b₁ is constant holds
b₁ 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 b₁ being sequence of M st b₁ is Cauchy holds
b₁ 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 b₁ being sequence of M st
( b₁ is constant & b₁ is convergent & b₁ is Cauchy & b₁ 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;