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
proof
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 )
now :: thesis: ( lim S in G implies F meets G )
assume 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;
hence ( not lim S in G or F meets G ) ; :: thesis: verum
end;
reconsider F0 = F as Subset of (TopSpaceMetr X) ;
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