let X be non empty MetrSpace; :: thesis: for S being sequence of X

for F being Subset of (TopSpaceMetr X) st S is convergent & ( for n being Nat holds S . n in F ) & F is closed holds

lim S in F

let S be sequence of X; :: thesis: for F being Subset of (TopSpaceMetr X) st S is convergent & ( for n being Nat holds S . n in F ) & F is closed holds

lim S in F

let F be Subset of (TopSpaceMetr X); :: thesis: ( S is convergent & ( for n being Nat holds S . n in F ) & F is closed implies lim S in F )

assume that

A1: S is convergent and

A2: for n being Nat holds S . n in F and

A3: F is closed ; :: thesis: lim S in F

A4: for G being Subset of (TopSpaceMetr X) st G is open & lim S in G holds

F meets G

lim S in the carrier of X ;

then lim S in the carrier of (TopSpaceMetr X) by TOPMETR:12;

then lim S in Cl F0 by A4, PRE_TOPC:def 7;

hence lim S in F by A3, PRE_TOPC:22; :: thesis: verum

for F being Subset of (TopSpaceMetr X) st S is convergent & ( for n being Nat holds S . n in F ) & F is closed holds

lim S in F

let S be sequence of X; :: thesis: for F being Subset of (TopSpaceMetr X) st S is convergent & ( for n being Nat holds S . n in F ) & F is closed holds

lim S in F

let F be Subset of (TopSpaceMetr X); :: thesis: ( S is convergent & ( for n being Nat holds S . n in F ) & F is closed implies lim S in F )

assume that

A1: S is convergent and

A2: for n being Nat holds S . n in F and

A3: F is closed ; :: thesis: lim S in F

A4: for G being Subset of (TopSpaceMetr X) st G is open & lim S in G holds

F meets G

proof

reconsider F0 = F as Subset of (TopSpaceMetr X) ;
let G be Subset of (TopSpaceMetr X); :: thesis: ( G is open & lim S in G implies F meets G )

assume A5: G is open ; :: thesis: ( not lim S in G or F meets G )

end;assume A5: G is open ; :: thesis: ( not lim S in G or F meets G )

now :: thesis: ( lim S in G implies F meets G )

hence
( not lim S in G or F meets G )
; :: thesis: verumassume
lim S in G
; :: thesis: F meets G

then consider r1 being Real such that

A6: r1 > 0 and

A7: Ball ((lim S),r1) c= G by A5, TOPMETR:15;

reconsider r2 = r1 as Real ;

consider n being Nat such that

A8: for m being Nat st m >= n holds

dist ((S . m),(lim S)) < r2 by A1, A6, TBSP_1:def 3;

dist ((S . n),(lim S)) < r2 by A8;

then A9: S . n in Ball ((lim S),r1) by METRIC_1:11;

S . n in F by A2;

then S . n in F /\ G by A7, A9, XBOOLE_0:def 4;

hence F meets G by XBOOLE_0:def 7; :: thesis: verum

end;then consider r1 being Real such that

A6: r1 > 0 and

A7: Ball ((lim S),r1) c= G by A5, TOPMETR:15;

reconsider r2 = r1 as Real ;

consider n being Nat such that

A8: for m being Nat st m >= n holds

dist ((S . m),(lim S)) < r2 by A1, A6, TBSP_1:def 3;

dist ((S . n),(lim S)) < r2 by A8;

then A9: S . n in Ball ((lim S),r1) by METRIC_1:11;

S . n in F by A2;

then S . n in F /\ G by A7, A9, XBOOLE_0:def 4;

hence F meets G by XBOOLE_0:def 7; :: thesis: verum

lim S in the carrier of X ;

then lim S in the carrier of (TopSpaceMetr X) by TOPMETR:12;

then lim S in Cl F0 by A4, PRE_TOPC:def 7;

hence lim S in F by A3, PRE_TOPC:22; :: thesis: verum