let T be non empty TopSpace; 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; 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; ( 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
; 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; ( ( 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)
; 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;
Iterated J is_eventually_in 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, Def15;
then consider i being
Element of
N such that A3:
for
j being
Element of
N st
i <= j holds
N . j in W
;
defpred S1[
Element of
N,
object ]
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 ) );
A4:
Int V = Int (Int V)
;
A5:
for
j being
Element of
N ex
e being
object st
S1[
j,
e]
consider f being
ManySortedSet of the
carrier of
N such that A9:
for
j being
Element of
N holds
S1[
j,
f . j]
from PBOOLE:sch 6(A5);
A10:
for
x being
object st
x in dom (Carrier J) holds
f . x in (Carrier J) . x
dom (Carrier J) = the
carrier of
N
by PARTFUN1:def 2;
then
dom f = dom (Carrier J)
by PARTFUN1:def 2;
then A11:
f in product (Carrier J)
by A10, CARD_3:9;
A12:
the
carrier of
(Iterated J) = [: the carrier of N,(product (Carrier J)):]
by Th26;
then reconsider x =
[i,f] as
Element of
(Iterated J) by A11, ZFMISC_1:87;
take
x
;
WAYBEL_0:def 11 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);
( not x <= j or (Iterated J) . j in V )
assume A13:
x <= j
;
(Iterated J) . j in V
consider j1 being
Element of
N,
j2 being
Element of
product (Carrier J) such that A14:
j = [j1,j2]
by A12, DOMAIN_1:1;
reconsider j2 =
j2,
i2 =
f as
Element of
(product J) by A11, YELLOW_1:def 4;
reconsider i1 =
i,
j1 =
j1 as
Element of
N ;
i2 in the
carrier of
(product J)
;
then A15:
i2 in product (Carrier J)
by YELLOW_1:def 4;
RelStr(# the
carrier of
(Iterated J), the
InternalRel of
(Iterated J) #)
= [:N,(product J):]
by Def13;
then A16:
[i1,i2] <= [j1,j2]
by A13, A14, YELLOW_0:1;
then
i2 <= j2
by YELLOW_3:11;
then
ex
f,
g being
Function st
(
f = i2 &
g = j2 & ( for
i being
object 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 A15, YELLOW_1:def 4;
then A17:
ex
R being
RelStr ex
xi,
yi being
Element of
R st
(
R = J . j1 &
xi = i2 . j1 &
yi = j2 . j1 &
xi <= yi )
;
ex
m being
Element of
(J . j1) st
(
m = f . j1 & (
i <= j1 implies for
n being
Element of
(J . j1) st
m <= n holds
(J . j1) . n in W ) )
by A9;
then
(J . j1) . (j2 . j1) in W
by A16, A17, YELLOW_3:11;
then A18:
(Iterated J) . j in W
by A14, Th27;
W c= V
by TOPS_1:16;
hence
(Iterated J) . j in V
by A18;
verum
end;
hence
p in Lim (Iterated J)
by Def15; verum