let n be Nat; for A, B being SetSequence of the carrier of (TOP-REAL n)
for C being SetSequence of the carrier of [:(TOP-REAL n),(TOP-REAL n):] st ( for i being Nat holds C . i = [:(A . i),(B . i):] ) holds
[:(Lim_inf A),(Lim_inf B):] = Lim_inf C
let A, B be SetSequence of the carrier of (TOP-REAL n); for C being SetSequence of the carrier of [:(TOP-REAL n),(TOP-REAL n):] st ( for i being Nat holds C . i = [:(A . i),(B . i):] ) holds
[:(Lim_inf A),(Lim_inf B):] = Lim_inf C
let C be SetSequence of the carrier of [:(TOP-REAL n),(TOP-REAL n):]; ( ( for i being Nat holds C . i = [:(A . i),(B . i):] ) implies [:(Lim_inf A),(Lim_inf B):] = Lim_inf C )
assume A1:
for i being Nat holds C . i = [:(A . i),(B . i):]
; [:(Lim_inf A),(Lim_inf B):] = Lim_inf C
thus
[:(Lim_inf A),(Lim_inf B):] c= Lim_inf C
XBOOLE_0:def 10 Lim_inf C c= [:(Lim_inf A),(Lim_inf B):]proof
let x be
object ;
TARSKI:def 3 ( not x in [:(Lim_inf A),(Lim_inf B):] or x in Lim_inf C )
assume A2:
x in [:(Lim_inf A),(Lim_inf B):]
;
x in Lim_inf C
then consider x1,
x2 being
object such that A3:
x1 in Lim_inf A
and A4:
x2 in Lim_inf B
and A5:
x = [x1,x2]
by ZFMISC_1:def 2;
reconsider p =
x as
Point of
[:(TOP-REAL n),(TOP-REAL n):] by A2;
reconsider x1 =
x1,
x2 =
x2 as
Point of
(TOP-REAL n) by A3, A4;
for
G being
a_neighborhood of
p ex
k being
Nat st
for
m being
Nat st
m > k holds
C . m meets G
proof
let G be
a_neighborhood of
p;
ex k being Nat st
for m being Nat st m > k holds
C . m meets G
G is
a_neighborhood of
[:{x1},{x2}:]
by A5, Th11;
then consider V being
a_neighborhood of
{x1},
W being
a_neighborhood of
x2 such that A6:
[:V,W:] c= G
by BORSUK_1:25;
consider k2 being
Nat such that A7:
for
m being
Nat st
m > k2 holds
B . m meets W
by A4, Def1;
V is
a_neighborhood of
x1
by CONNSP_2:8;
then consider k1 being
Nat such that A8:
for
m being
Nat st
m > k1 holds
A . m meets V
by A3, Def1;
reconsider k =
max (
k1,
k2) as
Nat by TARSKI:1;
take
k
;
for m being Nat st m > k holds
C . m meets G
let m be
Nat;
( m > k implies C . m meets G )
assume A9:
m > k
;
C . m meets G
k >= k2
by XXREAL_0:25;
then
m > k2
by A9, XXREAL_0:2;
then A10:
B . m meets W
by A7;
k >= k1
by XXREAL_0:25;
then
m > k1
by A9, XXREAL_0:2;
then
A . m meets V
by A8;
then
[:(A . m),(B . m):] meets [:V,W:]
by A10, KURATO_0:2;
then
C . m meets [:V,W:]
by A1;
hence
C . m meets G
by A6, XBOOLE_1:63;
verum
end;
hence
x in Lim_inf C
by Def1;
verum
end;
thus
Lim_inf C c= [:(Lim_inf A),(Lim_inf B):]
verumproof
let x be
object ;
TARSKI:def 3 ( not x in Lim_inf C or x in [:(Lim_inf A),(Lim_inf B):] )
assume A11:
x in Lim_inf C
;
x in [:(Lim_inf A),(Lim_inf B):]
then
x in the
carrier of
[:(TOP-REAL n),(TOP-REAL n):]
;
then A12:
x in [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):]
by BORSUK_1:def 2;
then reconsider p1 =
x `1 ,
p2 =
x `2 as
Point of
(TOP-REAL n) by MCART_1:10;
set H = the
a_neighborhood of
p2;
set F = the
a_neighborhood of
p1;
A13:
x = [p1,p2]
by A12, MCART_1:21;
for
G being
a_neighborhood of
p2 ex
k being
Nat st
for
m being
Nat st
m > k holds
B . m meets G
then A18:
p2 in Lim_inf B
by Def1;
for
G being
a_neighborhood of
p1 ex
k being
Nat st
for
m being
Nat st
m > k holds
A . m meets G
then
p1 in Lim_inf A
by Def1;
hence
x in [:(Lim_inf A),(Lim_inf B):]
by A13, A18, ZFMISC_1:87;
verum
end;