let T be non empty TopSpace; :: thesis: for K being prebasis of T
for N being net of T
for p being Point of T st ( for A being Subset of T st p in A & A in K holds
N is_eventually_in A ) holds
p in Lim N
let K be prebasis of T; :: thesis: for N being net of T
for p being Point of T st ( for A being Subset of T st p in A & A in K holds
N is_eventually_in A ) holds
p in Lim N
let N be net of T; :: thesis: for p being Point of T st ( for A being Subset of T st p in A & A in K holds
N is_eventually_in A ) holds
p in Lim N
let x be Point of T; :: thesis: ( ( for A being Subset of T st x in A & A in K holds
N is_eventually_in A ) implies x in Lim N )
assume A1: for A being Subset of T st x in A & A in K holds
N is_eventually_in A ; :: thesis: x in Lim N
now :: thesis: for A being a_neighborhood of x holds N is_eventually_in A
defpred S1[ object , object ] means ex D1 being set st
( D1 = $1 & ( for i, j being Element of N st i = $2 & j >= i holds
N . j in D1 ) );
let A be a_neighborhood of x; :: thesis: N is_eventually_in A
A2: Int A in the topology of T by PRE_TOPC:def 2;
FinMeetCl K is Basis of T by YELLOW_9:23;
then the topology of T = UniCl (FinMeetCl K) by YELLOW_9:22;
then consider Y being Subset-Family of T such that
A3: Y c= FinMeetCl K and
A4: Int A = union Y by A2, CANTOR_1:def 1;
x in Int A by CONNSP_2:def 1;
then consider y being set such that
A5: x in y and
A6: y in Y by A4, TARSKI:def 4;
consider Z being Subset-Family of T such that
A7: Z c= K and
A8: Z is finite and
A9: y = Intersect Z by A3, A6, CANTOR_1:def 3;
A10: for a being object st a in Z holds
ex b being object st
( b in the carrier of N & S1[a,b] )
proof
let a be object ; :: thesis: ( a in Z implies ex b being object st
( b in the carrier of N & S1[a,b] ) )
assume A11: a in Z ; :: thesis: ex b being object st
( b in the carrier of N & S1[a,b] )
then reconsider a = a as Subset of T ;
x in a by A5, A9, A11, SETFAM_1:43;
then N is_eventually_in a by A1, A7, A11;
then consider i being Element of N such that
A12: for j being Element of N st j >= i holds
N . j in a ;
reconsider i = i as object ;
take i ; :: thesis: ( i in the carrier of N & S1[a,i] )
thus i in the carrier of N ; :: thesis: S1[a,i]
take a ; :: thesis: ( a = a & ( for i, j being Element of N st i = i & j >= i holds
N . j in a ) )
thus ( a = a & ( for i, j being Element of N st i = i & j >= i holds
N . j in a ) ) by A12; :: thesis: verum
end;
consider f being Function such that
A13: ( dom f = Z & rng f c= the carrier of N ) and
A14: for a being object st a in Z holds
S1[a,f . a] from FUNCT_1:sch 6(A10);
reconsider z = rng f as finite Subset of ([#] N) by A8, A13, FINSET_1:8;
[#] N is directed by WAYBEL_0:def 6;
then consider k being Element of N such that
k in [#] N and
A15: k is_>=_than z by WAYBEL_0:1;
thus N is_eventually_in A :: thesis: verum
proof
take k ; :: according to WAYBEL_0:def 11 :: thesis: for b1 being Element of the carrier of N holds
( not k <= b1 or N . b1 in A )
let i be Element of N; :: thesis: ( not k <= i or N . i in A )
A16: Int A c= A by TOPS_1:16;
assume A17: i >= k ; :: thesis: N . i in A
now :: thesis: for a being set st a in Z holds
N . i in a
let a be set ; :: thesis: ( a in Z implies N . i in a )
assume A18: a in Z ; :: thesis: N . i in a
then A19: f . a in z by A13, FUNCT_1:def 3;
then reconsider j = f . a as Element of N ;
A20: j <= k by A15, A19;
S1[a,f . a] by A14, A18;
then consider D1 being set such that
A21: ( D1 = a & ( for i, j being Element of N st i = f . a & j >= i holds
N . j in D1 ) ) ;
thus N . i in a by A17, ORDERS_2:3, A21, A20; :: thesis: verum
end;
then A22: N . i in y by A9, SETFAM_1:43;
y c= union Y by A6, ZFMISC_1:74;
then N . i in Int A by A22, A4;
hence N . i in A by A16; :: thesis: verum
end;
end;
hence x in Lim N by YELLOW_6:def 15; :: thesis: verum