let X be set ; :: thesis: for A, B, C being SetSequence of X st ( for n being Nat holds C . n = (A . n) /\ (B . n) ) holds
lim_inf C = (lim_inf A) /\ (lim_inf B)
let A, B, C be SetSequence of X; :: thesis: ( ( for n being Nat holds C . n = (A . n) /\ (B . n) ) implies lim_inf C = (lim_inf A) /\ (lim_inf B) )
assume A1: for n being Nat holds C . n = (A . n) /\ (B . n) ; :: thesis: lim_inf C = (lim_inf A) /\ (lim_inf B)
thus lim_inf C c= (lim_inf A) /\ (lim_inf B) :: according to XBOOLE_0:def 10 :: thesis: (lim_inf A) /\ (lim_inf B) c= lim_inf C
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in lim_inf C or x in (lim_inf A) /\ (lim_inf B) )
assume x in lim_inf C ; :: thesis: x in (lim_inf A) /\ (lim_inf B)
then consider n being Nat such that
A2: for k being Nat holds x in C . (n + k) by Th4;
for k being Nat holds x in B . (n + k)
proof
let k be Nat; :: thesis: x in B . (n + k)
( C . (n + k) = (A . (n + k)) /\ (B . (n + k)) & x in C . (n + k) ) by A1, A2;
hence x in B . (n + k) by XBOOLE_0:def 4; :: thesis: verum
end;
then A3: x in lim_inf B by Th4;
for k being Nat holds x in A . (n + k)
proof
let k be Nat; :: thesis: x in A . (n + k)
( C . (n + k) = (A . (n + k)) /\ (B . (n + k)) & x in C . (n + k) ) by A1, A2;
hence x in A . (n + k) by XBOOLE_0:def 4; :: thesis: verum
end;
then x in lim_inf A by Th4;
hence x in (lim_inf A) /\ (lim_inf B) by A3, XBOOLE_0:def 4; :: thesis: verum
end;
thus (lim_inf A) /\ (lim_inf B) c= lim_inf C :: thesis: verum
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (lim_inf A) /\ (lim_inf B) or x in lim_inf C )
assume A4: x in (lim_inf A) /\ (lim_inf B) ; :: thesis: x in lim_inf C
then x in lim_inf A by XBOOLE_0:def 4;
then consider n1 being Nat such that
A5: for k being Nat holds x in A . (n1 + k) by Th4;
x in lim_inf B by A4, XBOOLE_0:def 4;
then consider n2 being Nat such that
A6: for k being Nat holds x in B . (n2 + k) by Th4;
set n = max (n1,n2);
A0: max (n1,n2) is Nat by TARSKI:1;
A7: for k being Nat holds x in B . ((max (n1,n2)) + k)
proof
let k be Nat; :: thesis: x in B . ((max (n1,n2)) + k)
consider g being Nat such that
A8: max (n1,n2) = n2 + g by NAT_1:10, XXREAL_0:25;
reconsider g = g as Nat ;
x in B . (n2 + (g + k)) by A6;
hence x in B . ((max (n1,n2)) + k) by A8; :: thesis: verum
end;
A9: for k being Nat holds x in A . ((max (n1,n2)) + k)
proof
let k be Nat; :: thesis: x in A . ((max (n1,n2)) + k)
consider g being Nat such that
A10: max (n1,n2) = n1 + g by NAT_1:10, XXREAL_0:25;
reconsider g = g as Nat ;
x in A . (n1 + (g + k)) by A5;
hence x in A . ((max (n1,n2)) + k) by A10; :: thesis: verum
end;
for k being Nat holds x in C . ((max (n1,n2)) + k)
proof
let k be Nat; :: thesis: x in C . ((max (n1,n2)) + k)
( x in A . ((max (n1,n2)) + k) & x in B . ((max (n1,n2)) + k) ) by A9, A7;
then x in (A . ((max (n1,n2)) + k)) /\ (B . ((max (n1,n2)) + k)) by XBOOLE_0:def 4;
hence x in C . ((max (n1,n2)) + k) by A1; :: thesis: verum
end;
hence x in lim_inf C by A0, Th4; :: thesis: verum
end;