let X be RealNormSpace; :: thesis: for f being sequence of (DualSp X) st X is Reflexive holds
( f is weakly-convergent iff f is weakly*-convergent )
let f be sequence of (DualSp X); :: thesis: ( X is Reflexive implies ( f is weakly-convergent iff f is weakly*-convergent ) )
assume AS: X is Reflexive ; :: thesis: ( f is weakly-convergent iff f is weakly*-convergent )
thus ( f is weakly-convergent implies f is weakly*-convergent ) by Lm710A; :: thesis: ( f is weakly*-convergent implies f is weakly-convergent )
thus ( f is weakly*-convergent implies f is weakly-convergent ) :: thesis: verum
proof
assume AS1: f is weakly*-convergent ; :: thesis: f is weakly-convergent
reconsider f0 = w*-lim f as Point of (DualSp X) ;
for F being Lipschitzian linear-Functional of (DualSp X) holds
( F * f is convergent & lim (F * f) = F . f0 )
proof
let F be Lipschitzian linear-Functional of (DualSp X); :: thesis: ( F * f is convergent & lim (F * f) = F . f0 )
reconsider G = F as Point of (DualSp (DualSp X)) by DUALSP01:def 10;
consider x being Point of X such that
B1: for f being Point of (DualSp X) holds G . f = f . x by AS, DUALSP02:21;
C4: ( f # x is convergent & lim (f # x) = f0 . x ) by AS1, Def2;
B5: for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
|.(((F * f) . n) - (F . f0)).| < r
proof
let r be Real; :: thesis: ( 0 < r implies ex m being Nat st
for n being Nat st m <= n holds
|.(((F * f) . n) - (F . f0)).| < r )
assume 0 < r ; :: thesis: ex m being Nat st
for n being Nat st m <= n holds
|.(((F * f) . n) - (F . f0)).| < r
then consider m being Nat such that
C1: for n being Nat st m <= n holds
|.(((f # x) . n) - (f0 . x)).| < r by C4, SEQ_2:def 7;
take m ; :: thesis: for n being Nat st m <= n holds
|.(((F * f) . n) - (F . f0)).| < r
hereby :: thesis: verum
let n be Nat; :: thesis: ( m <= n implies |.(((F * f) . n) - (F . f0)).| < r )
assume D3: m <= n ; :: thesis: |.(((F * f) . n) - (F . f0)).| < r
(F * f) . n = G . (f . n) by FUNCT_2:15, ORDINAL1:def 12;
then (F * f) . n = (f . n) . x by B1;
then (F * f) . n = (f # x) . n by Def1;
then |.(((F * f) . n) - (F . f0)).| = |.(((f # x) . n) - (f0 . x)).| by B1;
hence |.(((F * f) . n) - (F . f0)).| < r by C1, D3; :: thesis: verum
end;
end;
then F * f is convergent ;
hence ( F * f is convergent & lim (F * f) = F . f0 ) by B5, SEQ_2:def 7; :: thesis: verum
end;
hence f is weakly-convergent ; :: thesis: verum
end;