let X be set ; :: thesis: for A being Subset of X
for A1 being SetSequence of X st A1 is convergent holds
lim_inf (A (\+\) A1) = A \+\ (lim_inf A1)
let A be Subset of X; :: thesis: for A1 being SetSequence of X st A1 is convergent holds
lim_inf (A (\+\) A1) = A \+\ (lim_inf A1)
let A1 be SetSequence of X; :: thesis: ( A1 is convergent implies lim_inf (A (\+\) A1) = A \+\ (lim_inf A1) )
assume A1: A1 is convergent ; :: thesis: lim_inf (A (\+\) A1) = A \+\ (lim_inf A1)
thus lim_inf (A (\+\) A1) c= A \+\ (lim_inf A1) by Th78; :: according to XBOOLE_0:def 10 :: thesis: A \+\ (lim_inf A1) c= lim_inf (A (\+\) A1)
thus A \+\ (lim_inf A1) c= lim_inf (A (\+\) A1) :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A \+\ (lim_inf A1) or x in lim_inf (A (\+\) A1) )
assume A2: x in A \+\ (lim_inf A1) ; :: thesis: x in lim_inf (A (\+\) A1)

per cases ( ( x in A & not x in lim_inf A1 ) or ( not x in A & x in lim_inf A1 ) ) by A2, XBOOLE_0:1;

suppose A3: ( x in A & not x in lim_inf A1 ) ; :: thesis: x in lim_inf (A (\+\) A1)

then not x in lim_sup A1 by A1, KURATO_2:def 7;
then consider n1 being Element of NAT such that
A4: for k being Element of NAT holds not x in A1 . (n1 + k) by KURATO_2:8;

now

let k be Element of NAT ; :: thesis: x in (A (\+\) A1) . (n1 + k)
not x in A1 . (n1 + k) by A4;
then x in A \+\ (A1 . (n1 + k)) by A3, XBOOLE_0:1;
hence x in (A (\+\) A1) . (n1 + k) by Def9; :: thesis: verum

end;

hence x in lim_inf (A (\+\) A1) by KURATO_2:7; :: thesis: verum

end;

suppose A5: ( not x in A & x in lim_inf A1 ) ; :: thesis: x in lim_inf (A (\+\) A1)

then consider n2 being Element of NAT such that
A6: for k being Element of NAT holds x in A1 . (n2 + k) by KURATO_2:7;

now

let k be Element of NAT ; :: thesis: x in (A (\+\) A1) . (n2 + k)
x in A1 . (n2 + k) by A6;
then x in A \+\ (A1 . (n2 + k)) by A5, XBOOLE_0:1;
hence x in (A (\+\) A1) . (n2 + k) by Def9; :: thesis: verum

end;

hence x in lim_inf (A (\+\) A1) by KURATO_2:7; :: thesis: verum

end;

end;

end;