let T be non empty 1-sorted ; for C being Convergence-Class of T holds
( Convergence (ConvergenceSpace C) = C iff C is topological )
let C be Convergence-Class of T; ( Convergence (ConvergenceSpace C) = C iff C is topological )
set CC = ConvergenceSpace C;
set CCC = Convergence (ConvergenceSpace C);
A1:
the carrier of (ConvergenceSpace C) = the carrier of T
by Def24;
A2:
for N being net of T
for n being net of ConvergenceSpace C st N = n holds
for x being subnet of n holds x is subnet of N
A6:
for N being net of T
for n being net of ConvergenceSpace C st N = n holds
for X being subnet of N holds X is subnet of n
A10:
for N being net of T holds N is net of ConvergenceSpace C
by Def24;
hereby ( C is topological implies Convergence (ConvergenceSpace C) = C )
assume A11:
Convergence (ConvergenceSpace C) = C
;
C is topological A12:
C is
(SUBNETS)
proof
let N be
net of
T;
YELLOW_6:def 21 for Y being subnet of N st Y in NetUniv T holds
for p being Element of T st [N,p] in C holds
[Y,p] in Clet Y be
subnet of
N;
( Y in NetUniv T implies for p being Element of T st [N,p] in C holds
[Y,p] in C )
reconsider M =
N as
net of
ConvergenceSpace C by Def24;
reconsider X =
Y as
subnet of
M by A6;
assume
Y in NetUniv T
;
for p being Element of T st [N,p] in C holds
[Y,p] in C
then A13:
X in NetUniv (ConvergenceSpace C)
by A1, Lm7;
let p be
Element of
T;
( [N,p] in C implies [Y,p] in C )
reconsider q =
p as
Element of
(ConvergenceSpace C) by Def24;
assume
[N,p] in C
;
[Y,p] in C
then
[M,q] in Convergence (ConvergenceSpace C)
by A11;
hence
[Y,p] in C
by A11, A13, Def21;
verum
end; A14:
C is
(ITERATED_LIMITS)
proof
let X be
net of
T;
YELLOW_6:def 23 for p being Element of T st [X,p] in C holds
for J being net_set of the carrier of X,T st ( for i being Element of X holds [(J . i),(X . i)] in C ) holds
[(Iterated J),p] in Clet p be
Element of
T;
( [X,p] in C implies for J being net_set of the carrier of X,T st ( for i being Element of X holds [(J . i),(X . i)] in C ) holds
[(Iterated J),p] in C )
reconsider q =
p as
Element of
(ConvergenceSpace C) by Def24;
reconsider x =
X as
net of
ConvergenceSpace C by Def24;
assume A15:
[X,p] in C
;
for J being net_set of the carrier of X,T st ( for i being Element of X holds [(J . i),(X . i)] in C ) holds
[(Iterated J),p] in C
let J be
net_set of the
carrier of
X,
T;
( ( for i being Element of X holds [(J . i),(X . i)] in C ) implies [(Iterated J),p] in C )
reconsider I =
J as
ManySortedSet of the
carrier of
x ;
I is
net_set of the
carrier of
x,
ConvergenceSpace C
then reconsider I =
J as
net_set of the
carrier of
x,
ConvergenceSpace C ;
assume A16:
for
i being
Element of
X holds
[(J . i),(X . i)] in C
;
[(Iterated J),p] in C
then A17:
[(Iterated I),q] in Convergence (ConvergenceSpace C)
by A11, A15, Def23;
A18:
RelStr(# the
carrier of
(Iterated I), the
InternalRel of
(Iterated I) #) =
[:X,(product J):]
by Def13
.=
RelStr(# the
carrier of
(Iterated J), the
InternalRel of
(Iterated J) #)
by Def13
;
dom the
mapping of
(Iterated I) = the
carrier of
(Iterated I)
by FUNCT_2:def 1;
then
dom the
mapping of
(Iterated I) = dom the
mapping of
(Iterated J)
by A18, FUNCT_2:def 1;
then
the
mapping of
(Iterated I) = the
mapping of
(Iterated J)
by A19, FUNCT_1:2;
hence
[(Iterated J),p] in C
by A11, A17, A18;
verum
end; A21:
C is
(DIVERGENCE)
proof
let X be
net of
T;
YELLOW_6:def 22 for p being Element of T st X in NetUniv T & not [X,p] in C holds
ex Y being subnet of X st
( Y in NetUniv T & ( for Z being subnet of Y holds not [Z,p] in C ) )let p be
Element of
T;
( X in NetUniv T & not [X,p] in C implies ex Y being subnet of X st
( Y in NetUniv T & ( for Z being subnet of Y holds not [Z,p] in C ) ) )
reconsider q =
p as
Element of
(ConvergenceSpace C) by Def24;
reconsider x =
X as
net of
ConvergenceSpace C by Def24;
assume
X in NetUniv T
;
( [X,p] in C or ex Y being subnet of X st
( Y in NetUniv T & ( for Z being subnet of Y holds not [Z,p] in C ) ) )
then A22:
x in NetUniv (ConvergenceSpace C)
by A1, Lm7;
assume
not
[X,p] in C
;
ex Y being subnet of X st
( Y in NetUniv T & ( for Z being subnet of Y holds not [Z,p] in C ) )
then consider y being
subnet of
x such that A23:
y in NetUniv (ConvergenceSpace C)
and A24:
for
z being
subnet of
y holds not
[z,q] in Convergence (ConvergenceSpace C)
by A11, A22, Def22;
reconsider Y =
y as
subnet of
X by A2;
take
Y
;
( Y in NetUniv T & ( for Z being subnet of Y holds not [Z,p] in C ) )
thus
Y in NetUniv T
by A1, A23, Lm7;
for Z being subnet of Y holds not [Z,p] in C
let Z be
subnet of
Y;
not [Z,p] in C
reconsider z =
Z as
subnet of
y by A6;
not
[z,q] in Convergence (ConvergenceSpace C)
by A24;
hence
not
[Z,p] in C
by A11;
verum
end;
C is
(CONSTANTS)
hence
C is
topological
by A12, A21, A14;
verum
end;
assume A26:
( C is (CONSTANTS) & C is (SUBNETS) & C is (DIVERGENCE) & C is (ITERATED_LIMITS) )
; YELLOW_6:def 25 Convergence (ConvergenceSpace C) = C
then reconsider C9 = C as topological Convergence-Class of T ;
A27:
Convergence (ConvergenceSpace C) c= C
proof
let x,
y be
object ;
RELAT_1:def 3 ( not [x,y] in Convergence (ConvergenceSpace C) or [x,y] in C )
assume A28:
[x,y] in Convergence (ConvergenceSpace C)
;
[x,y] in C
Convergence (ConvergenceSpace C) c= [:(NetUniv (ConvergenceSpace C)), the carrier of (ConvergenceSpace C):]
by Def18;
then consider M being
Element of
NetUniv (ConvergenceSpace C),
p being
Element of
(ConvergenceSpace C) such that A29:
[x,y] = [M,p]
by A28, DOMAIN_1:1;
reconsider q =
p as
Point of
T by Def24;
A30:
M in NetUniv (ConvergenceSpace C)
;
A31:
ex
N being
strict net of
ConvergenceSpace C st
(
N = M & the
carrier of
N in the_universe_of the
carrier of
(ConvergenceSpace C) )
by Def11;
assume A32:
not
[x,y] in C
;
contradiction
reconsider M =
M as
net of
ConvergenceSpace C by A31;
reconsider N =
M as
net of
T by Def24;
N in NetUniv T
by A1, A30, Lm7;
then consider Y being
subnet of
N such that A33:
Y in NetUniv T
and A34:
for
Z being
subnet of
Y holds not
[Z,q] in C
by A26, A29, A32;
reconsider Y9 =
Y as
subnet of
M by A6;
reconsider YY =
RelStr(# the
carrier of
Y, the
InternalRel of
Y #) as non
empty transitive directed RelStr by Lm1, Lm2;
set X =
ConstantNet (
YY,
q);
defpred S1[
object ,
object ]
means ex
i being
Element of
Y ex
Ji being
net of
T st
( $1
= i &
Ji = $2 &
[Ji,p] in C &
rng the
mapping of
Ji c= { (Y . c) where c is Element of Y : i <= c } );
A35:
RelStr(# the
carrier of
(ConstantNet (YY,q)), the
InternalRel of
(ConstantNet (YY,q)) #)
= YY
by Def5;
reconsider X =
ConstantNet (
YY,
q) as
strict constant net of
T ;
A36:
p in Lim M
by A28, A29, Def19;
A37:
for
x being
object st
x in the
carrier of
X holds
ex
j being
object st
S1[
x,
j]
consider J being
ManySortedSet of the
carrier of
X such that A44:
for
x being
object st
x in the
carrier of
X holds
S1[
x,
J . x]
from PBOOLE:sch 3(A37);
then reconsider J =
J as
yielding_non-empty_carriers net_set of the
carrier of
X,
T by Th24;
reconsider X9 =
X as
net of
ConvergenceSpace C by Def24;
A45:
the
mapping of
X9 is
constant
;
A46:
for
i being
Element of
X holds
[(J . i),(X . i)] in C
A47:
the_value_of X = q
by Th13;
reconsider X9 =
X9 as
constant net of
ConvergenceSpace C by A45, Def4;
A48:
RelStr(# the
carrier of
(Iterated J), the
InternalRel of
(Iterated J) #)
= [:X,(product J):]
by Def13;
then A49:
the
carrier of
(Iterated J) = [: the carrier of X, the carrier of (product J):]
by YELLOW_3:def 2;
A50:
Iterated J is
subnet of
Y
proof
set F = the
Element of
(product J);
set h = the
mapping of
(Iterated J);
set g = the
mapping of
Y9;
defpred S2[
object ,
object ,
object ]
means ex
f being
Function ex
x being
Element of
X st
(
f . $2
= $1 &
x = $3 & the
mapping of
(J . x) . $2
= the
mapping of
Y . $1 );
deffunc H1(
Element of
Y)
-> set =
{ c where c is Element of Y : $1 <= c } ;
consider B being
ManySortedSet of the
carrier of
Y such that A51:
for
i being
Element of
Y holds
B . i = H1(
i)
from PBOOLE:sch 5();
then reconsider B =
B as
V2()
ManySortedSet of the
carrier of
Y by RELAT_1:def 9;
deffunc H2(
Element of
X)
-> set = the
carrier of
(J . $1);
consider M being
ManySortedSet of the
carrier of
X such that A55:
for
x being
Element of
X holds
M . x = H2(
x)
from PBOOLE:sch 5();
reconsider B9 =
B as
V2()
ManySortedSet of the
carrier of
X by A35;
A56:
for
i being
object st
i in the
carrier of
X holds
for
x being
object st
x in M . i holds
ex
y being
object st
(
y in B9 . i &
S2[
y,
x,
i] )
proof
let i be
object ;
( i in the carrier of X implies for x being object st x in M . i holds
ex y being object st
( y in B9 . i & S2[y,x,i] ) )
assume A57:
i in the
carrier of
X
;
for x being object st x in M . i holds
ex y being object st
( y in B9 . i & S2[y,x,i] )
consider e being
Element of
Y,
Ji being
net of
T such that A58:
i = e
and A59:
Ji = J . i
and
[Ji,p] in C
and A60:
rng the
mapping of
Ji c= { (Y . c) where c is Element of Y : e <= c }
by A44, A57;
reconsider i9 =
i as
Element of
X by A57;
defpred S3[
object ,
object ]
means the
mapping of
Ji . $1
= the
mapping of
Y . $2;
A61:
for
ji being
Element of
Ji ex
u being
Element of
B9 . i9 st
S3[
ji,
u]
consider f being
Function of
Ji,
(B9 . i9) such that A64:
for
ji being
Element of
Ji holds
S3[
ji,
f . ji]
from FUNCT_2:sch 3(A61);
let x be
object ;
( x in M . i implies ex y being object st
( y in B9 . i & S2[y,x,i] ) )
assume
x in M . i
;
ex y being object st
( y in B9 . i & S2[y,x,i] )
then reconsider ji =
x as
Element of
Ji by A55, A57, A59;
reconsider f =
f as
Function of
Ji,
(B . i) ;
take
f . x
;
( f . x in B9 . i & S2[f . x,x,i] )
f . ji in B . i
;
hence
f . x in B9 . i
;
S2[f . x,x,i]
take
f
;
ex x being Element of X st
( f . x = f . x & x = i & the mapping of (J . x) . x = the mapping of Y . (f . x) )
take
i9
;
( f . x = f . x & i9 = i & the mapping of (J . i9) . x = the mapping of Y . (f . x) )
thus
(
f . x = f . x &
i9 = i )
;
the mapping of (J . i9) . x = the mapping of Y . (f . x)
thus the
mapping of
(J . i9) . x =
the
mapping of
Ji . ji
by A59
.=
the
mapping of
Y . (f . x)
by A64
;
verum
end;
consider u being
ManySortedFunction of
M,
B9 such that A65:
for
i being
object st
i in the
carrier of
X holds
ex
f being
Function of
(M . i),
(B9 . i) st
(
f = u . i & ( for
x being
object st
x in M . i holds
S2[
f . x,
x,
i] ) )
from MSSUBFAM:sch 1(A56);
deffunc H3(
Element of
X,
Element of
(product J))
-> set =
(u . $1) . ($2 . $1);
A66:
for
x being
Element of
X for
y being
Element of
(product J) holds
H3(
x,
y)
in the
carrier of
Y
consider f being
Function of
[: the carrier of X, the carrier of (product J):],
Y such that A70:
for
x being
Element of
X for
y being
Element of
(product J) holds
f . (
x,
y)
= H3(
x,
y)
from FUNCT_7:sch 1(A66);
reconsider f =
f as
Function of
(Iterated J),
Y by A49;
A71:
for
x being
Element of
X for
j being
Element of
M . x holds the
mapping of
(J . x) . j = the
mapping of
Y . ((u . x) . j)
A74:
for
x being
object st
x in dom the
mapping of
(Iterated J) holds
the
mapping of
(Iterated J) . x = the
mapping of
Y9 . (f . x)
take
f
;
YELLOW_6:def 9 ( the mapping of (Iterated J) = the mapping of Y * f & ( for m being Element of Y ex n being Element of (Iterated J) st
for p being Element of (Iterated J) st n <= p holds
m <= f . p ) )
for
x being
object holds
(
x in dom the
mapping of
(Iterated J) iff (
x in dom f &
f . x in dom the
mapping of
Y9 ) )
hence
the
mapping of
(Iterated J) = the
mapping of
Y * f
by A74, FUNCT_1:10;
for m being Element of Y ex n being Element of (Iterated J) st
for p being Element of (Iterated J) st n <= p holds
m <= f . p
let m be
Element of
Y;
ex n being Element of (Iterated J) st
for p being Element of (Iterated J) st n <= p holds
m <= f . p
reconsider n =
[m, the Element of (product J)] as
Element of
(Iterated J) by A35, A49, ZFMISC_1:87;
take
n
;
for p being Element of (Iterated J) st n <= p holds
m <= f . p
let p be
Element of
(Iterated J);
( n <= p implies m <= f . p )
consider k9 being
Element of
X,
G being
Element of
(product J) such that A79:
p = [k9,G]
by A49, DOMAIN_1:1;
reconsider m9 =
m as
Element of
X by A35;
reconsider F = the
Element of
(product J) as
Element of
(product J) ;
G in the
carrier of
(product J)
;
then A80:
(
dom (Carrier J) = the
carrier of
X9 &
G in product (Carrier J) )
by PARTFUN1:def 2, YELLOW_1:def 4;
reconsider k =
k9 as
Element of
Y by A35;
A81:
f . (
k9,
G)
= (u . k) . (G . k)
by A70;
reconsider k99 =
k9 as
Element of
X9 ;
A82:
u . k is
Function of
(M . k),
(B . k)
by PBOOLE:def 15;
then A83:
rng (u . k) c= B . k
by RELAT_1:def 19;
dom (u . k) =
M . k
by A82, FUNCT_2:def 1
.=
the
carrier of
(J . k9)
by A55
.=
(Carrier J) . k99
by Th2
;
then A84:
G . k99 in dom (u . k)
by A80, CARD_3:9;
reconsider k9 =
k as
Element of
X ;
reconsider G =
G as
Element of
(product J) ;
assume
n <= p
;
m <= f . p
then
[m9,F] <= [k9,G]
by A48, A79, Lm3;
then
m9 <= k9
by YELLOW_3:11;
then A85:
m <= k
by A35, Lm3;
f . p in rng (u . k)
by A79, A81, A84, FUNCT_1:def 3;
then
f . p in B . k
by A83;
then
f . p in { c where c is Element of Y : k <= c }
by A51;
then
ex
c being
Element of
Y st
(
c = f . p &
k <= c )
;
hence
m <= f . p
by A85, YELLOW_0:def 2;
verum
end;
A86:
RelStr(# the
carrier of
X, the
InternalRel of
X #)
= RelStr(# the
carrier of
Y, the
InternalRel of
Y #)
by Def5;
ex
N0 being
strict net of
T st
(
N0 = Y & the
carrier of
N0 in the_universe_of the
carrier of
T )
by A33, Def11;
then
X in NetUniv T
by A86, Def11;
then
[X,q] in C
by A26, A47;
then
[(Iterated J),q] in C
by A26, A46;
hence
contradiction
by A34, A50;
verum
end;
C c= Convergence (ConvergenceSpace C)
by Th40;
hence
Convergence (ConvergenceSpace C) = C
by A27; verum