let X be set ; :: thesis: for A being SetSequence of X
for B being Subset of X st ( for n being Nat holds A . n = B ) holds
lim_sup A = B
let A be SetSequence of X; :: thesis: for B being Subset of X st ( for n being Nat holds A . n = B ) holds
lim_sup A = B
let B be Subset of X; :: thesis: ( ( for n being Nat holds A . n = B ) implies lim_sup A = B )
assume A1: for n being Nat holds A . n = B ; :: thesis: lim_sup A = B
thus lim_sup A c= B :: according to XBOOLE_0:def 10 :: thesis: B c= lim_sup A
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in lim_sup A or x in B )
assume x in lim_sup A ; :: thesis: x in B
then ex k being Nat st x in A . (0 + k) by Th5;
hence x in B by A1; :: thesis: verum
end;
thus B c= lim_sup A :: thesis: verum
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in lim_sup A )
assume A2: x in B ; :: thesis: x in lim_sup A
for m being Nat ex k being Nat st x in A . (m + k)
proof
let m be Nat; :: thesis: ex k being Nat st x in A . (m + k)
take 0 ; :: thesis: x in A . (m + 0)
thus x in A . (m + 0) by A1, A2; :: thesis: verum
end;
hence x in lim_sup A by Th5; :: thesis: verum
end;