let X be RealUnitarySpace; :: thesis: for Y being Subset of X holds
( Y is closed iff for s being sequence of X st rng s c= Y & s is convergent holds
lim s in Y )
let Y be Subset of X; :: thesis: ( Y is closed iff for s being sequence of X st rng s c= Y & s is convergent holds
lim s in Y )
hereby :: thesis: ( ( for s being sequence of X st rng s c= Y & s is convergent holds
lim s in Y ) implies Y is closed )
assume Y is closed ; :: thesis: for s being sequence of X st rng s c= Y & s is convergent holds
lim s in Y
then consider Z being Subset of (RUSp2RNSp X) such that
A1: ( Z = Y & Z is closed ) ;
thus for s being sequence of X st rng s c= Y & s is convergent holds
lim s in Y :: thesis: verum
proof
let s be sequence of X; :: thesis: ( rng s c= Y & s is convergent implies lim s in Y )
assume A3: ( rng s c= Y & s is convergent ) ; :: thesis: lim s in Y
reconsider s1 = s as sequence of (RUSp2RNSp X) ;
( rng s1 c= Z & s1 is convergent ) by A3, A1, RHS8;
then lim s1 in Z by A1;
hence lim s in Y by A1, A3, RHS9; :: thesis: verum
end;
end;
assume A4: for s being sequence of X st rng s c= Y & s is convergent holds
lim s in Y ; :: thesis: Y is closed
reconsider Z = Y as Subset of (RUSp2RNSp X) ;
for s1 being sequence of (RUSp2RNSp X) st rng s1 c= Z & s1 is convergent holds
lim s1 in Z
proof
let s1 be sequence of (RUSp2RNSp X); :: thesis: ( rng s1 c= Z & s1 is convergent implies lim s1 in Z )
assume A5: ( rng s1 c= Z & s1 is convergent ) ; :: thesis: lim s1 in Z
reconsider s = s1 as sequence of X ;
A6: ( rng s c= Y & s is convergent ) by A5, RHS8;
then lim s in Y by A4;
hence lim s1 in Z by A6, RHS9; :: thesis: verum
end;
then Z is closed ;
hence Y is closed ; :: thesis: verum