let T be non empty TopSpace; :: thesis: for N being net of T
for p being Point of T st p in Lim N holds
for J being net_set of the carrier of N,T st ( for i being Element of N holds N . i in Lim (J . i) ) holds
p in Lim (Iterated J)
let N be net of T; :: thesis: for p being Point of T st p in Lim N holds
for J being net_set of the carrier of N,T st ( for i being Element of N holds N . i in Lim (J . i) ) holds
p in Lim (Iterated J)
let p be Point of T; :: thesis: ( p in Lim N implies for J being net_set of the carrier of N,T st ( for i being Element of N holds N . i in Lim (J . i) ) holds
p in Lim (Iterated J) )
assume A1:
p in Lim N
; :: thesis: for J being net_set of the carrier of N,T st ( for i being Element of N holds N . i in Lim (J . i) ) holds
p in Lim (Iterated J)
let J be net_set of the carrier of N,T; :: thesis: ( ( for i being Element of N holds N . i in Lim (J . i) ) implies p in Lim (Iterated J) )
assume A2:
for i being Element of N holds N . i in Lim (J . i)
; :: thesis: p in Lim (Iterated J)
for V being a_neighborhood of p holds Iterated J is_eventually_in V
proof
let V be
a_neighborhood of
p;
:: thesis: Iterated J is_eventually_in V
A3:
Int V = Int (Int V)
;
p in Int (Int V)
by CONNSP_2:def 1;
then reconsider W =
Int V as
a_neighborhood of
p by CONNSP_2:def 1;
N is_eventually_in W
by A1, Def18;
then consider i being
Element of
N such that A4:
for
j being
Element of
N st
i <= j holds
N . j in W
by WAYBEL_0:def 11;
defpred S1[
Element of
N,
set ]
means ex
m being
Element of
(J . $1) st
(
m = $2 & (
i <= $1 implies for
n being
Element of
(J . $1) st
m <= n holds
(J . $1) . n in W ) );
A5:
for
j being
Element of
N ex
e being
set st
S1[
j,
e]
consider f being
ManySortedSet of the
carrier of
N such that A10:
for
j being
Element of
N holds
S1[
j,
f . j]
from PBOOLE:sch 6(A5);
A11:
the
carrier of
(Iterated J) = [:the carrier of N,(product (Carrier J)):]
by Th35;
dom (Carrier J) = the
carrier of
N
by PBOOLE:def 3;
then A12:
dom f = dom (Carrier J)
by PBOOLE:def 3;
for
x being
set st
x in dom (Carrier J) holds
f . x in (Carrier J) . x
then A13:
f in product (Carrier J)
by A12, CARD_3:18;
then reconsider x =
[i,f] as
Element of
(Iterated J) by A11, ZFMISC_1:106;
take
x
;
:: according to WAYBEL_0:def 11 :: thesis: for b1 being Element of the carrier of (Iterated J) holds
( not x <= b1 or (Iterated J) . b1 in V )
let j be
Element of
(Iterated J);
:: thesis: ( not x <= j or (Iterated J) . j in V )
assume A14:
x <= j
;
:: thesis: (Iterated J) . j in V
consider j1 being
Element of
N,
j2 being
Element of
product (Carrier J) such that A15:
j = [j1,j2]
by A11, DOMAIN_1:9;
reconsider j2 =
j2,
i2 =
f as
Element of
(product J) by A13, YELLOW_1:def 4;
reconsider i1 =
i,
j1 =
j1 as
Element of
N ;
RelStr(# the
carrier of
(Iterated J),the
InternalRel of
(Iterated J) #)
= [:N,(product J):]
by Def16;
then A16:
[i1,i2] <= [j1,j2]
by A14, A15, YELLOW_0:1;
then A17:
(
i1 <= j1 &
i2 <= j2 )
by YELLOW_3:11;
consider m being
Element of
(J . j1) such that A18:
m = f . j1
and A19:
(
i <= j1 implies for
n being
Element of
(J . j1) st
m <= n holds
(J . j1) . n in W )
by A10;
i2 in the
carrier of
(product J)
;
then
i2 in product (Carrier J)
by YELLOW_1:def 4;
then
ex
f,
g being
Function st
(
f = i2 &
g = j2 & ( for
i being
set st
i in the
carrier of
N holds
ex
R being
RelStr ex
xi,
yi being
Element of
R st
(
R = J . i &
xi = f . i &
yi = g . i &
xi <= yi ) ) )
by A17, YELLOW_1:def 4;
then
ex
R being
RelStr ex
xi,
yi being
Element of
R st
(
R = J . j1 &
xi = i2 . j1 &
yi = j2 . j1 &
xi <= yi )
;
then
(J . j1) . (j2 . j1) in W
by A16, A18, A19, YELLOW_3:11;
then A20:
(Iterated J) . j in W
by A15, Th36;
W c= V
by TOPS_1:44;
hence
(Iterated J) . j in V
by A20;
:: thesis: verum
end;
hence
p in Lim (Iterated J)
by Def18; :: thesis: verum