let X be 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 ) )
let x be 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 ) )
let S be sequence of X; ( S is_convergent_in_metrspace_to x iff ( dist_to_point (S,x) is convergent & lim (dist_to_point (S,x)) = 0 ) )
A1:
( S is_convergent_in_metrspace_to x implies ( dist_to_point (S,x) is convergent & lim (dist_to_point (S,x)) = 0 ) )
proof
assume A2:
S is_convergent_in_metrspace_to x
;
( dist_to_point (S,x) is convergent & lim (dist_to_point (S,x)) = 0 )
A3:
for
r being
Real st
0 < r holds
ex
m being
Nat st
for
n being
Nat st
m <= n holds
|.(((dist_to_point (S,x)) . n) - 0).| < r
proof
let r be
Real;
( 0 < r implies ex m being Nat st
for n being Nat st m <= n holds
|.(((dist_to_point (S,x)) . n) - 0).| < r )
assume A4:
0 < r
;
ex m being Nat st
for n being Nat st m <= n holds
|.(((dist_to_point (S,x)) . n) - 0).| < r
reconsider r =
r as
Real ;
consider m1 being
Nat such that A5:
for
n being
Nat st
m1 <= n holds
dist (
(S . n),
x)
< r
by A2, A4;
take k =
m1;
for n being Nat st k <= n holds
|.(((dist_to_point (S,x)) . n) - 0).| < r
let n be
Nat;
( k <= n implies |.(((dist_to_point (S,x)) . n) - 0).| < r )
assume
k <= n
;
|.(((dist_to_point (S,x)) . n) - 0).| < r
then
dist (
(S . n),
x)
< r
by A5;
then A6:
(dist_to_point (S,x)) . n < r
by Def6;
dist (
(S . n),
x)
= (dist_to_point (S,x)) . n
by Def6;
then
0 <= (dist_to_point (S,x)) . n
by METRIC_1:5;
hence
|.(((dist_to_point (S,x)) . n) - 0).| < r
by A6, ABSVALUE:def 1;
verum
end;
then
dist_to_point (
S,
x) is
convergent
by SEQ_2:def 6;
hence
(
dist_to_point (
S,
x) is
convergent &
lim (dist_to_point (S,x)) = 0 )
by A3, SEQ_2:def 7;
verum
end;
( dist_to_point (S,x) is convergent & lim (dist_to_point (S,x)) = 0 implies S is_convergent_in_metrspace_to x )
proof
assume A7:
(
dist_to_point (
S,
x) is
convergent &
lim (dist_to_point (S,x)) = 0 )
;
S is_convergent_in_metrspace_to x
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
proof
let r be
Real;
( 0 < r implies ex m being Nat st
for n being Nat st m <= n holds
dist ((S . n),x) < r )
assume
0 < r
;
ex m being Nat st
for n being Nat st m <= n holds
dist ((S . n),x) < r
then consider m1 being
Nat such that A8:
for
n being
Nat st
m1 <= n holds
|.(((dist_to_point (S,x)) . n) - 0).| < r
by A7, SEQ_2:def 7;
reconsider k =
m1 as
Element of
NAT by ORDINAL1:def 12;
take
k
;
for n being Nat st k <= n holds
dist ((S . n),x) < r
let n be
Nat;
( k <= n implies dist ((S . n),x) < r )
assume
k <= n
;
dist ((S . n),x) < r
then
|.(((dist_to_point (S,x)) . n) - 0).| < r
by A8;
then A9:
|.(dist ((S . n),x)).| < r
by Def6;
0 <= dist (
(S . n),
x)
by METRIC_1:5;
hence
dist (
(S . n),
x)
< r
by A9, ABSVALUE:def 1;
verum
end;
hence
S is_convergent_in_metrspace_to x
;
verum
end;
hence
( S is_convergent_in_metrspace_to x iff ( dist_to_point (S,x) is convergent & lim (dist_to_point (S,x)) = 0 ) )
by A1; verum