let T be non empty 1-sorted ; :: thesis: for C being topological Convergence-Class of T
for S being Subset of (ConvergenceSpace C)
for p being Point of (ConvergenceSpace C) st p in Cl S holds
ex N being net of ConvergenceSpace C st
( [N,p] in C & rng the mapping of N c= S & p in Lim N )
let C be topological Convergence-Class of T; :: thesis: for S being Subset of (ConvergenceSpace C)
for p being Point of (ConvergenceSpace C) st p in Cl S holds
ex N being net of ConvergenceSpace C st
( [N,p] in C & rng the mapping of N c= S & p in Lim N )
let S be Subset of (ConvergenceSpace C); :: thesis: for p being Point of (ConvergenceSpace C) st p in Cl S holds
ex N being net of ConvergenceSpace C st
( [N,p] in C & rng the mapping of N c= S & p in Lim N )
let p be Point of (ConvergenceSpace C); :: thesis: ( p in Cl S implies ex N being net of ConvergenceSpace C st
( [N,p] in C & rng the mapping of N c= S & p in Lim N ) )
assume A1:
p in Cl S
; :: thesis: ex N being net of ConvergenceSpace C st
( [N,p] in C & rng the mapping of N c= S & p in Lim N )
set CC = ConvergenceSpace C;
defpred S1[ Point of (ConvergenceSpace C)] means ex N being net of ConvergenceSpace C st
( [N,$1] in C & rng the mapping of N c= S & $1 in Lim N );
set F = { q where q is Point of (ConvergenceSpace C) : S1[q] } ;
{ q where q is Point of (ConvergenceSpace C) : S1[q] } is Subset of (ConvergenceSpace C)
from DOMAIN_1:sch 7();
then reconsider F = { q where q is Point of (ConvergenceSpace C) : S1[q] } as Subset of (ConvergenceSpace C) ;
for p being Element of T
for N being net of T st [N,p] in C & N is_often_in F holds
p in F
proof
let p be
Element of
T;
:: thesis: for N being net of T st [N,p] in C & N is_often_in F holds
p in Flet N be
net of
T;
:: thesis: ( [N,p] in C & N is_often_in F implies p in F )
assume that A2:
[N,p] in C
and A3:
N is_often_in F
;
:: thesis: p in F
C c= [:(NetUniv T),the carrier of T:]
by Def21;
then A4:
N in NetUniv T
by A2, ZFMISC_1:106;
reconsider M =
N " F as
subnet of
N by A3, Th31;
defpred S2[
Element of
M,
set ]
means (
[$2,(M . $1)] in C & ex
X being
net of
T st
(
X = $2 &
rng the
mapping of
X c= S ) );
consider J being
ManySortedSet of
such that A11:
for
i being
Element of
M holds
S2[
i,
J . i]
from PBOOLE:sch 6(A5);
for
i being
set st
i in the
carrier of
M holds
J . i is
net of
T
then reconsider J =
J as
net_set of the
carrier of
M,
T by Th33;
A12:
for
i being
Element of
M holds
(
[(J . i),(M . i)] in C &
rng the
mapping of
(J . i) c= S )
reconsider I =
Iterated J as
net of
ConvergenceSpace C by Def27;
A13:
ex
N0 being
strict net of
T st
(
N0 = N & the
carrier of
N0 in the_universe_of the
carrier of
T )
by A4, Def14;
the
carrier of
M = the
mapping of
N " F
by Def13;
then
the
carrier of
M in the_universe_of the
carrier of
T
by A13, CLASSES1:def 1;
then
M in NetUniv T
by Def14;
then
[M,p] in C
by A2, Def24;
then A14:
[I,p] in C
by A12, Def26;
set XX =
{ (rng the mapping of (J . i)) where i is Element of M : verum } ;
A15:
rng the
mapping of
I c= union { (rng the mapping of (J . i)) where i is Element of M : verum }
by Th37;
for
x being
set st
x in { (rng the mapping of (J . i)) where i is Element of M : verum } holds
x c= S
then
union { (rng the mapping of (J . i)) where i is Element of M : verum } c= S
by ZFMISC_1:94;
then A16:
rng the
mapping of
I c= S
by A15, XBOOLE_1:1;
reconsider q =
p as
Point of
(ConvergenceSpace C) by Def27;
C c= Convergence (ConvergenceSpace C)
by Th49;
then
q in Lim I
by A14, Def22;
hence
p in F
by A14, A16;
:: thesis: verum
end;
then A17:
F is closed
by Th51;
S c= F
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in S or x in F )
assume A18:
x in S
;
:: thesis: x in F
then reconsider q =
x as
Point of
(ConvergenceSpace C) ;
{} in {{} }
by TARSKI:def 1;
then reconsider r =
{[{} ,{} ]} as
Relation of
{{} } by RELSET_1:8;
set R =
RelStr(#
{{} },
r #);
A20:
RelStr(#
{{} },
r #) is
transitive
RelStr(#
{{} },
r #) is
directed
then reconsider R =
RelStr(#
{{} },
r #) as non
empty transitive directed RelStr by A20;
set N =
R --> q;
A21:
the_value_of (R --> q) = q
by Th22;
the
carrier of
(ConvergenceSpace C) = the
carrier of
T
by Def27;
then reconsider M =
R --> q as
strict constant net of
T by Lm6;
the_value_of the
mapping of
M = q
by A21, Def10;
then A22:
the_value_of M = q
by Def10;
set V =
the_universe_of the
carrier of
T;
A23:
RelStr(# the
carrier of
(R --> q),the
InternalRel of
(R --> q) #)
= RelStr(# the
carrier of
R,the
InternalRel of
R #)
by Def7;
{} in the_universe_of the
carrier of
T
by CLASSES2:62;
then
the
carrier of
R in the_universe_of the
carrier of
T
by CLASSES2:3;
then
M in NetUniv T
by A23, Def14;
then A24:
[M,q] in C
by A22, Def23;
the
mapping of
(R --> q) = the
carrier of
(R --> q) --> q
by Def7;
then
rng the
mapping of
(R --> q) = {q}
by FUNCOP_1:14;
then A25:
rng the
mapping of
(R --> q) c= S
by A18, ZFMISC_1:37;
q in Lim (R --> q)
by A21, Th42;
hence
x in F
by A24, A25;
:: thesis: verum
end;
then
Cl S c= F
by A17, TOPS_1:31;
then
p in F
by A1;
then
ex q being Point of (ConvergenceSpace C) st
( p = q & ex N being net of ConvergenceSpace C st
( [N,q] in C & rng the mapping of N c= S & q in Lim N ) )
;
hence
ex N being net of ConvergenceSpace C st
( [N,p] in C & rng the mapping of N c= S & p in Lim N )
; :: thesis: verum