let T be non empty 1-sorted ; 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; 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); 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); ( 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
; 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;
for N being net of T st [N,p] in C & N is_often_in F holds
p in F
reconsider q =
p as
Point of
(ConvergenceSpace C) by Def24;
let N be
net of
T;
( [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
;
p in F
C c= [:(NetUniv T), the carrier of T:]
by Def18;
then
N in NetUniv T
by A2, ZFMISC_1:87;
then A4:
ex
N0 being
strict net of
T st
(
N0 = N & the
carrier of
N0 in the_universe_of the
carrier of
T )
by Def11;
reconsider M =
N " F as
subnet of
N by A3, Th22;
defpred S2[
Element of
M,
object ]
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 the
carrier of
M 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 Th24;
set XX =
{ (rng the mapping of (J . i)) where i is Element of M : verum } ;
A12:
for
i being
Element of
M holds
(
[(J . i),(M . i)] in C &
rng the
mapping of
(J . i) c= S )
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 A13:
union { (rng the mapping of (J . i)) where i is Element of M : verum } c= S
by ZFMISC_1:76;
reconsider I =
Iterated J as
net of
ConvergenceSpace C by Def24;
rng the
mapping of
I c= union { (rng the mapping of (J . i)) where i is Element of M : verum }
by Th28;
then A14:
rng the
mapping of
I c= S
by A13;
the
carrier of
M = the
mapping of
N " F
by Def10;
then
the
carrier of
M in the_universe_of the
carrier of
T
by A4, CLASSES1:def 1;
then
M in NetUniv T
by Def11;
then
[M,p] in C
by A2, Def21;
then A15:
[I,p] in C
by A12, Def23;
C c= Convergence (ConvergenceSpace C)
by Th40;
then
q in Lim I
by A15, Def19;
hence
p in F
by A15, A14;
verum
end;
then A16:
F is closed
by Th42;
S c= F
proof
{} in {{}}
by TARSKI:def 1;
then reconsider r =
{[{},{}]} as
Relation of
{{}} by RELSET_1:3;
set R =
RelStr(#
{{}},
r #);
A18:
RelStr(#
{{}},
r #) is
transitive
by A17;
RelStr(#
{{}},
r #) is
directed
then reconsider R =
RelStr(#
{{}},
r #) as non
empty transitive directed RelStr by A18;
let x be
object ;
TARSKI:def 3 ( not x in S or x in F )
set V =
the_universe_of the
carrier of
T;
assume A19:
x in S
;
x in F
then reconsider q =
x as
Point of
(ConvergenceSpace C) ;
set N =
ConstantNet (
R,
q);
the
mapping of
(ConstantNet (R,q)) = the
carrier of
(ConstantNet (R,q)) --> q
by Def5;
then
rng the
mapping of
(ConstantNet (R,q)) = {q}
by FUNCOP_1:8;
then A20:
rng the
mapping of
(ConstantNet (R,q)) c= S
by A19, ZFMISC_1:31;
{} in the_universe_of the
carrier of
T
by CLASSES2:56;
then A21:
the
carrier of
R in the_universe_of the
carrier of
T
by CLASSES2:2;
the
carrier of
(ConvergenceSpace C) = the
carrier of
T
by Def24;
then reconsider M =
ConstantNet (
R,
q) as
strict constant net of
T by Lm6;
A22:
the_value_of (ConstantNet (R,q)) = q
by Th13;
then
the_value_of the
mapping of
M = q
by Def8;
then A23:
the_value_of M = q
by Def8;
RelStr(# the
carrier of
(ConstantNet (R,q)), the
InternalRel of
(ConstantNet (R,q)) #)
= RelStr(# the
carrier of
R, the
InternalRel of
R #)
by Def5;
then
M in NetUniv T
by A21, Def11;
then A24:
[M,q] in C
by A23, Def20;
q in Lim (ConstantNet (R,q))
by A22, Th33;
hence
x in F
by A24, A20;
verum
end;
then
Cl S c= F
by A16, TOPS_1:5;
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 )
; verum