:: 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)

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)

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 ) )

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 )

( 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)) ) ) )

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;

ex b_{1} being Function of [:A,A:],REAL st

for a, b being Element of A holds b_{1} . (a,b) = (G . (a,b)) / (1 + (G . (a,b)))

for b_{1}, b_{2} being Function of [:A,A:],REAL st ( for a, b being Element of A holds b_{1} . (a,b) = (G . (a,b)) / (1 + (G . (a,b))) ) & ( for a, b being Element of A holds b_{2} . (a,b) = (G . (a,b)) / (1 + (G . (a,b))) ) holds

b_{1} = b_{2}

end;
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 for a, b being Element of A holds it . (a,b) = (G . (a,b)) / (1 + (G . (a,b)));

ex b

for a, b being Element of A holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines bounded_metric METRIC_6:def 1 :

for A being non empty set

for G, b_{3} being Function of [:A,A:],REAL holds

( b_{3} = bounded_metric (A,G) iff for a, b being Element of A holds b_{3} . (a,b) = (G . (a,b)) / (1 + (G . (a,b))) );

for A being non empty set

for G, b

( 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

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;

:: 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 );

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;

( V is bounded iff ex r being Real ex x being Element of X st

( 0 < r & V c= Ball (x,r) ) )

end;
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 ex r being Real ex x being Element of X st

( 0 < r & V c= Ball (x,r) );

( V is bounded iff ex r being Real ex x being Element of X st

( 0 < r & V c= Ball (x,r) ) )

proof 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) ) );

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) ) );

:: 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) ) );

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;

end;
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;

ex m being Nat st

for n being Nat st m <= n holds

S . n in V;

:: 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 );

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) ) ) )

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 ;

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

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;

ex b_{1} being Real_Sequence st

for n being Nat holds b_{1} . n = dist ((S . n),x)

for b_{1}, b_{2} being Real_Sequence st ( for n being Nat holds b_{1} . n = dist ((S . n),x) ) & ( for n being Nat holds b_{2} . n = dist ((S . n),x) ) holds

b_{1} = b_{2}

end;
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 for n being Nat holds it . n = dist ((S . n),x);

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof 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_{4} being Real_Sequence holds

( b_{4} = dist_to_point (S,x) iff for n being Nat holds b_{4} . n = dist ((S . n),x) );

for X being non empty MetrSpace

for S being sequence of X

for x being Element of X

for b

( b

definition

let X be non empty MetrSpace;

let S, T be sequence of X;

ex b_{1} being Real_Sequence st

for n being Nat holds b_{1} . n = dist ((S . n),(T . n))

for b_{1}, b_{2} being Real_Sequence st ( for n being Nat holds b_{1} . n = dist ((S . n),(T . n)) ) & ( for n being Nat holds b_{2} . n = dist ((S . n),(T . n)) ) holds

b_{1} = b_{2}

end;
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 for n being Nat holds it . n = dist ((S . n),(T . n));

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof 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_{4} being Real_Sequence holds

( b_{4} = sequence_of_dist (S,T) iff for n being Nat holds b_{4} . n = dist ((S . n),(T . n)) );

for X being non empty MetrSpace

for S, T being sequence of X

for b

( b

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

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;

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 )

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 ) )

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

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

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

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 )

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 )

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

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))

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

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 :: 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

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

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

registration

let M be non empty MetrSpace;

for b_{1} being sequence of M st b_{1} is constant holds

b_{1} is convergent
by Th23;

for b_{1} being sequence of M st b_{1} is Cauchy holds

b_{1} is bounded
by Th28;

end;
cluster Function-like constant V33( NAT , the carrier of M) -> convergent for Element of bool [:NAT, the carrier of M:];

coherence for b

b

cluster Function-like V33( NAT , the carrier of M) Cauchy -> bounded for Element of bool [:NAT, the carrier of M:];

coherence for b

b

registration

let M be non empty MetrSpace;

ex b_{1} being sequence of M st

( b_{1} is constant & b_{1} is convergent & b_{1} is Cauchy & b_{1} is bounded )

end;
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

( b

proof 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) )

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;