let n be Element of NAT ; :: thesis: 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 Element of 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); :: thesis: for C being SetSequence of the carrier of [:(TOP-REAL n),(TOP-REAL n):] st ( for i being Element of 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):]; :: thesis: ( ( for i being Element of NAT holds C . i = [:(A . i),(B . i):] ) implies [:(Lim_inf A),(Lim_inf B):] = Lim_inf C )
assume A1:
for i being Element of NAT holds C . i = [:(A . i),(B . i):]
; :: thesis: [:(Lim_inf A),(Lim_inf B):] = Lim_inf C
thus
[:(Lim_inf A),(Lim_inf B):] c= Lim_inf C
:: according to XBOOLE_0:def 10 :: thesis: Lim_inf C c= [:(Lim_inf A),(Lim_inf B):]proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( 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):]
;
:: thesis: x in Lim_inf C
then consider x1,
x2 being
set such that A3:
(
x1 in Lim_inf A &
x2 in Lim_inf B &
x = [x1,x2] )
by ZFMISC_1:def 2;
reconsider x1 =
x1,
x2 =
x2 as
Point of
(TOP-REAL n) by A3;
reconsider p =
x as
Point of
[:(TOP-REAL n),(TOP-REAL n):] by A2;
for
G being
a_neighborhood of
p ex
k being
Element of
NAT st
for
m being
Element of
NAT st
m > k holds
C . m meets G
proof
let G be
a_neighborhood of
p;
:: thesis: ex k being Element of NAT st
for m being Element of NAT st m > k holds
C . m meets G
G is
a_neighborhood of
[:{x1},{x2}:]
by A3, Th41;
then consider V being
a_neighborhood of
{x1},
W being
a_neighborhood of
x2 such that A4:
[:V,W:] c= G
by BORSUK_1:67;
V is
a_neighborhood of
x1
by CONNSP_2:10;
then consider k1 being
Element of
NAT such that A5:
for
m being
Element of
NAT st
m > k1 holds
A . m meets V
by A3, Def11;
consider k2 being
Element of
NAT such that A6:
for
m being
Element of
NAT st
m > k2 holds
B . m meets W
by A3, Def11;
take k =
max k1,
k2;
:: thesis: for m being Element of NAT st m > k holds
C . m meets G
A7:
(
k >= k1 &
k >= k2 )
by XXREAL_0:25;
let m be
Element of
NAT ;
:: thesis: ( m > k implies C . m meets G )
assume A8:
m > k
;
:: thesis: C . m meets G
then
m > k1
by A7, XXREAL_0:2;
then A9:
A . m meets V
by A5;
m > k2
by A7, A8, XXREAL_0:2;
then
B . m meets W
by A6;
then
[:(A . m),(B . m):] meets [:V,W:]
by A9, Th4;
then
C . m meets [:V,W:]
by A1;
hence
C . m meets G
by A4, XBOOLE_1:63;
:: thesis: verum
end;
hence
x in Lim_inf C
by Def11;
:: thesis: verum
end;
thus
Lim_inf C c= [:(Lim_inf A),(Lim_inf B):]
:: thesis: verumproof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in Lim_inf C or x in [:(Lim_inf A),(Lim_inf B):] )
assume A10:
x in Lim_inf C
;
:: thesis: x in [:(Lim_inf A),(Lim_inf B):]
then
x in the
carrier of
[:(TOP-REAL n),(TOP-REAL n):]
;
then A11:
x in [:the carrier of (TOP-REAL n),the carrier of (TOP-REAL n):]
by BORSUK_1:def 5;
then reconsider p1 =
x `1 ,
p2 =
x `2 as
Point of
(TOP-REAL n) by MCART_1:10;
A12:
x = [p1,p2]
by A11, MCART_1:23;
consider H being
a_neighborhood of
p2;
consider F being
a_neighborhood of
p1;
for
G being
a_neighborhood of
p1 ex
k being
Element of
NAT st
for
m being
Element of
NAT st
m > k holds
A . m meets G
then A16:
p1 in Lim_inf A
by Def11;
for
G being
a_neighborhood of
p2 ex
k being
Element of
NAT st
for
m being
Element of
NAT st
m > k holds
B . m meets G
then
p2 in Lim_inf B
by Def11;
hence
x in [:(Lim_inf A),(Lim_inf B):]
by A12, A16, ZFMISC_1:106;
:: thesis: verum
end;