let X be RealBanachSpace; :: thesis: for X0 being non empty Subset of X st not X is trivial & X is Reflexive holds
( X0 is weakly-sequentially-compact iff ex S being non empty Subset of REAL st
( S = { ||.x.|| where x is Point of X : x in X0 } & S is bounded_above ) )
let X0 be non empty Subset of X; :: thesis: ( not X is trivial & X is Reflexive implies ( X0 is weakly-sequentially-compact iff ex S being non empty Subset of REAL st
( S = { ||.x.|| where x is Point of X : x in X0 } & S is bounded_above ) ) )
assume AS: ( not X is trivial & X is Reflexive ) ; :: thesis: ( X0 is weakly-sequentially-compact iff ex S being non empty Subset of REAL st
( S = { ||.x.|| where x is Point of X : x in X0 } & S is bounded_above ) )
hence ( X0 is weakly-sequentially-compact implies ex S being non empty Subset of REAL st
( S = { ||.x.|| where x is Point of X : x in X0 } & S is bounded_above ) ) by Th713A; :: thesis: ( ex S being non empty Subset of REAL st
( S = { ||.x.|| where x is Point of X : x in X0 } & S is bounded_above ) implies X0 is weakly-sequentially-compact )
given S being non empty Subset of REAL such that B0: ( S = { ||.x.|| where x is Point of X : x in X0 } & S is bounded_above ) ; :: thesis: X0 is weakly-sequentially-compact
for seq being sequence of X0 ex seq1 being sequence of X st
( seq1 is subsequence of seq & seq1 is weakly-convergent & w-lim seq1 in X )
proof
let seq0 be sequence of X0; :: thesis: ex seq1 being sequence of X st
( seq1 is subsequence of seq0 & seq1 is weakly-convergent & w-lim seq1 in X )
reconsider seq = seq0 as sequence of X by FUNCT_2:7;
consider r being Real such that
B1: r is UpperBound of S by B0;
B2: r + 0 < r + 1 by XREAL_1:8;
for n being Nat holds ||.seq.|| . n < r + 1
proof
let n be Nat; :: thesis: ||.seq.|| . n < r + 1
seq0 . n in X0 ;
then ||.(seq . n).|| in S by B0;
then ||.(seq . n).|| <= r by B1, XXREAL_2:def 1;
then ||.seq.|| . n <= r by NORMSP_0:def 4;
hence ||.seq.|| . n < r + 1 by B2, XXREAL_0:2; :: thesis: verum
end;
then B5: ||.seq.|| is bounded_above ;
for n being Nat holds - 1 < ||.seq.|| . n
proof
let n be Nat; :: thesis: - 1 < ||.seq.|| . n
||.(seq . n).|| = ||.seq.|| . n by NORMSP_0:def 4;
hence - 1 < ||.seq.|| . n ; :: thesis: verum
end;
then ||.seq.|| is bounded_below ;
then consider seq1 being sequence of X such that
P1: ( seq1 is subsequence of seq & seq1 is weakly-convergent ) by AS, Th813, B5;
w-lim seq1 in X ;
hence ex seq1 being sequence of X st
( seq1 is subsequence of seq0 & seq1 is weakly-convergent & w-lim seq1 in X ) by P1; :: thesis: verum
end;
hence X0 is weakly-sequentially-compact ; :: thesis: verum