let X be RealNormSpace; :: thesis: for Y being Subset of X
for v being object holds
( v in Cl Y iff ex seq being sequence of X st
( rng seq c= Y & seq is convergent & lim seq = v ) )
let Y be Subset of X; :: thesis: for v being object holds
( v in Cl Y iff ex seq being sequence of X st
( rng seq c= Y & seq is convergent & lim seq = v ) )
let v be object ; :: thesis: ( v in Cl Y iff ex seq being sequence of X st
( rng seq c= Y & seq is convergent & lim seq = v ) )
reconsider Z = Y as Subset of (LinearTopSpaceNorm X) by NORMSP_2:def 4;
A1: Cl Z = Cl Y by EQCL1;
hereby :: thesis: ( ex seq being sequence of X st
( rng seq c= Y & seq is convergent & lim seq = v ) implies v in Cl Y )
assume A2: v in Cl Y ; :: thesis: ex seq being Function of NAT,X st
( rng seq c= Y & seq is convergent & lim seq = v )
then A3: for G being Subset of (LinearTopSpaceNorm X) st G is open & v in G holds
G meets Z by A1, PRE_TOPC:def 7;
reconsider v0 = v as Point of X by A2;
defpred S1[ Nat, Point of X] means ( ||.(v0 - $2).|| < 1 / ($1 + 1) & $2 in Y );
A4: for n being Element of NAT ex w being Element of X st S1[n,w]
proof
let n be Element of NAT ; :: thesis: ex w being Element of X st S1[n,w]
set e = 1 / (n + 1);
for x being object st x in { y where y is Point of X : ||.(v0 - y).|| < 1 / (n + 1) } holds
x in the carrier of (LinearTopSpaceNorm X)
proof
let x be object ; :: thesis: ( x in { y where y is Point of X : ||.(v0 - y).|| < 1 / (n + 1) } implies x in the carrier of (LinearTopSpaceNorm X) )
assume x in { y where y is Point of X : ||.(v0 - y).|| < 1 / (n + 1) } ; :: thesis: x in the carrier of (LinearTopSpaceNorm X)
then ex y being Point of X st
( x = y & ||.(v0 - y).|| < 1 / (n + 1) ) ;
then x in the carrier of X ;
hence x in the carrier of (LinearTopSpaceNorm X) by NORMSP_2:def 4; :: thesis: verum
end;
then reconsider G = { y where y is Point of X : ||.(v0 - y).|| < 1 / (n + 1) } as Subset of (LinearTopSpaceNorm X) by TARSKI:def 3;
||.(v0 - v0).|| < 1 / (n + 1) by NORMSP_1:6;
then v0 in G ;
then G meets Z by A3, NORMSP_2:23;
then consider w being object such that
A5: w in G /\ Z by XBOOLE_0:def 1;
A6: ( w in G & w in Z ) by A5, XBOOLE_0:def 4;
then A7: ex y being Point of X st
( w = y & ||.(v0 - y).|| < 1 / (n + 1) ) ;
reconsider w = w as Point of X by A6;
take w ; :: thesis: S1[n,w]
thus S1[n,w] by A5, A7, XBOOLE_0:def 4; :: thesis: verum
end;
consider seq being Function of NAT,X such that
A8: for n being Element of NAT holds S1[n,seq . n] from FUNCT_2:sch 3(A4);
take seq = seq; :: thesis: ( rng seq c= Y & seq is convergent & lim seq = v )
for y being object st y in rng seq holds
y in Y
proof
let y be object ; :: thesis: ( y in rng seq implies y in Y )
assume y in rng seq ; :: thesis: y in Y
then ex x being object st
( x in NAT & seq . x = y ) by FUNCT_2:11;
hence y in Y by A8; :: thesis: verum
end;
hence rng seq c= Y ; :: thesis: ( seq is convergent & lim seq = v )
A10: now :: thesis: for s being Real st 0 < s holds
ex k being Nat st
for m being Nat st k <= m holds
||.((seq . m) - v0).|| < s
let s be Real; :: thesis: ( 0 < s implies ex k being Nat st
for m being Nat st k <= m holds
||.((seq . m) - v0).|| < s )
consider n being Nat such that
A11: s " < n by SEQ_4:3;
assume A12: 0 < s ; :: thesis: ex k being Nat st
for m being Nat st k <= m holds
||.((seq . m) - v0).|| < s
(s ") + 0 < n + 1 by A11, XREAL_1:8;
then 1 / (n + 1) < 1 / (s ") by A12, XREAL_1:76;
then A13: 1 / (n + 1) < s by XCMPLX_1:216;
take k = n; :: thesis: for m being Nat st k <= m holds
||.((seq . m) - v0).|| < s
let m be Nat; :: thesis: ( k <= m implies ||.((seq . m) - v0).|| < s )
A14: m in NAT by ORDINAL1:def 12;
assume k <= m ; :: thesis: ||.((seq . m) - v0).|| < s
then k + 1 <= m + 1 by XREAL_1:6;
then 1 / (m + 1) <= 1 / (k + 1) by XREAL_1:118;
then 1 / (m + 1) < s by A13, XXREAL_0:2;
then ||.(v0 - (seq . m)).|| < s by A8, A14, XXREAL_0:2;
hence ||.((seq . m) - v0).|| < s by NORMSP_1:7; :: thesis: verum
end;
hence seq is convergent ; :: thesis: lim seq = v
hence lim seq = v by A10, NORMSP_1:def 7; :: thesis: verum
end;
given seq being sequence of X such that A15: rng seq c= Y and
A16: seq is convergent and
A17: lim seq = v ; :: thesis: v in Cl Y
v in the carrier of X by A17;
then A18: v in the carrier of (LinearTopSpaceNorm X) by NORMSP_2:def 4;
reconsider v0 = v as Point of X by A17;
for G being Subset of (LinearTopSpaceNorm X) st G is open & v in G holds
G meets Z
proof
let G be Subset of (LinearTopSpaceNorm X); :: thesis: ( G is open & v in G implies G meets Z )
assume ( G is open & v in G ) ; :: thesis: G meets Z
then consider r being Real such that
A20: ( r > 0 & { y where y is Point of X : ||.(v0 - y).|| < r } c= G ) by NORMSP_2:22;
consider m being Nat such that
A21: for n being Nat st m <= n holds
||.((seq . n) - v0).|| < r by A16, A17, A20, NORMSP_1:def 7;
||.((seq . m) - v0).|| < r by A21;
then ||.(v0 - (seq . m)).|| < r by NORMSP_1:7;
then A22: seq . m in { y where y is Point of X : ||.(v0 - y).|| < r } ;
seq . m in rng seq by FUNCT_2:4, ORDINAL1:def 12;
hence G meets Z by A15, A20, A22, XBOOLE_0:def 4; :: thesis: verum
end;
hence v in Cl Y by A1, A18, PRE_TOPC:def 7; :: thesis: verum