let X be 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
let x be 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
let S be sequence of X; ( ( for V being Subset of X st x in V & V in Family_open_set X holds
V contains_almost_all_sequence S ) implies S is_convergent_in_metrspace_to x )
A1:
for r being Real st 0 < r holds
x in Ball (x,r)
assume A2:
for V being Subset of X st x in V & V in Family_open_set X holds
V contains_almost_all_sequence S
; 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
x in Ball (
x,
r)
by A1;
then
Ball (
x,
r)
contains_almost_all_sequence S
by A2, PCOMPS_1:29;
then consider m1 being
Nat such that A3:
for
n being
Nat st
m1 <= n holds
S . n in Ball (
x,
r)
;
take k =
m1;
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
S . n in Ball (
x,
r)
by A3;
hence
dist (
(S . n),
x)
< r
by METRIC_1:11;
verum
end;
hence
S is_convergent_in_metrspace_to x
; verum