let T be non empty 1-sorted ; :: thesis: for C being Convergence-Class of T holds
( Convergence (ConvergenceSpace C) = C iff C is topological )
let C be Convergence-Class of T; :: thesis: ( 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 Def27;
A2:
for N being net of T holds N is net of ConvergenceSpace C
by Def27;
A3:
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
hereby :: thesis: ( C is topological implies Convergence (ConvergenceSpace C) = C )
assume A9:
Convergence (ConvergenceSpace C) = C
;
:: thesis: C is topological thus
C is
topological
:: thesis: verumproof
thus
C is
(CONSTANTS)
:: according to YELLOW_6:def 28 :: thesis: ( C is (SUBNETS) & C is (DIVERGENCE) & C is (ITERATED_LIMITS) )
thus
C is
(SUBNETS)
:: thesis: ( C is (DIVERGENCE) & C is (ITERATED_LIMITS) )proof
let N be
net of
T;
:: according to YELLOW_6:def 24 :: thesis: 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;
:: thesis: ( 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 Def27;
reconsider X =
Y as
subnet of
M by A3;
assume
Y in NetUniv T
;
:: thesis: for p being Element of T st [N,p] in C holds
[Y,p] in C
then A11:
X in NetUniv (ConvergenceSpace C)
by A1, Lm7;
let p be
Element of
T;
:: thesis: ( [N,p] in C implies [Y,p] in C )
reconsider q =
p as
Element of
(ConvergenceSpace C) by Def27;
assume
[N,p] in C
;
:: thesis: [Y,p] in C
then
[M,q] in Convergence (ConvergenceSpace C)
by A9;
hence
[Y,p] in C
by A9, A11, Def24;
:: thesis: verum
end;
thus
C is
(DIVERGENCE)
:: thesis: C is (ITERATED_LIMITS) proof
let X be
net of
T;
:: according to YELLOW_6:def 25 :: thesis: 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;
:: thesis: ( 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 x =
X as
net of
ConvergenceSpace C by Def27;
reconsider q =
p as
Element of
(ConvergenceSpace C) by Def27;
assume
X in NetUniv T
;
:: thesis: ( [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 A12:
x in NetUniv (ConvergenceSpace C)
by A1, Lm7;
assume
not
[X,p] in C
;
:: thesis: 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 A13:
y in NetUniv (ConvergenceSpace C)
and A14:
for
z being
subnet of
y holds not
[z,q] in Convergence (ConvergenceSpace C)
by A9, A12, Def25;
reconsider Y =
y as
subnet of
X by A6;
take
Y
;
:: thesis: ( Y in NetUniv T & ( for Z being subnet of Y holds not [Z,p] in C ) )
thus
Y in NetUniv T
by A1, A13, Lm7;
:: thesis: for Z being subnet of Y holds not [Z,p] in C
let Z be
subnet of
Y;
:: thesis: not [Z,p] in C
reconsider z =
Z as
subnet of
y by A3;
not
[z,q] in Convergence (ConvergenceSpace C)
by A14;
hence
not
[Z,p] in C
by A9;
:: thesis: verum
end;
thus
C is
(ITERATED_LIMITS)
:: thesis: verumproof
let X be
net of
T;
:: according to YELLOW_6:def 26 :: thesis: 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;
:: thesis: ( [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 x =
X as
net of
ConvergenceSpace C by Def27;
reconsider q =
p as
Element of
(ConvergenceSpace C) by Def27;
assume A15:
[X,p] in C
;
:: thesis: 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;
:: thesis: ( ( 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 ;
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
;
:: thesis: [(Iterated J),p] in C
then A17:
[(Iterated I),q] in Convergence (ConvergenceSpace C)
by A9, A15, Def26;
A18:
RelStr(# the
carrier of
(Iterated I),the
InternalRel of
(Iterated I) #) =
[:X,(product J):]
by Def16
.=
RelStr(# the
carrier of
(Iterated J),the
InternalRel of
(Iterated J) #)
by Def16
;
dom the
mapping of
(Iterated I) = the
carrier of
(Iterated I)
by FUNCT_2:def 1;
then A19:
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:9;
hence
[(Iterated J),p] in C
by A9, A17, A18;
:: thesis: verum
end;
end;
end;
assume A23:
( C is (CONSTANTS) & C is (SUBNETS) & C is (DIVERGENCE) & C is (ITERATED_LIMITS) )
; :: according to YELLOW_6:def 28 :: thesis: Convergence (ConvergenceSpace C) = C
then reconsider C' = C as topological Convergence-Class of T ;
A24:
Convergence (ConvergenceSpace C) c= C
proof
let x be
set ;
:: according to RELAT_1:def 3 :: thesis: for b1 being set holds
( not [x,b1] in Convergence (ConvergenceSpace C) or [x,b1] in C )let y be
set ;
:: thesis: ( not [x,y] in Convergence (ConvergenceSpace C) or [x,y] in C )
A25:
Convergence (ConvergenceSpace C) c= [:(NetUniv (ConvergenceSpace C)),the carrier of (ConvergenceSpace C):]
by Def21;
assume A26:
[x,y] in Convergence (ConvergenceSpace C)
;
:: thesis: [x,y] in C
then consider M being
Element of
NetUniv (ConvergenceSpace C),
p being
Element of
(ConvergenceSpace C) such that A27:
[x,y] = [M,p]
by A25, DOMAIN_1:9;
A28:
M in NetUniv (ConvergenceSpace C)
;
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 Def14;
then reconsider M =
M as
net of
ConvergenceSpace C ;
reconsider N =
M as
net of
T by Def27;
reconsider q =
p as
Point of
T by Def27;
A29:
N in NetUniv T
by A1, A28, Lm7;
assume
not
[x,y] in C
;
:: thesis: contradiction
then consider Y being
subnet of
N such that A30:
Y in NetUniv T
and A31:
for
Z being
subnet of
Y holds not
[Z,q] in C
by A23, A27, A29, Def25;
reconsider YY =
RelStr(# the
carrier of
Y,the
InternalRel of
Y #) as non
empty transitive directed RelStr by Lm1, Lm2;
set X =
YY --> q;
A32:
RelStr(# the
carrier of
(YY --> q),the
InternalRel of
(YY --> q) #)
= YY
by Def7;
reconsider X =
YY --> q as non
empty strict constant net of
T ;
A33:
ex
N0 being
strict net of
T st
(
N0 = Y & the
carrier of
N0 in the_universe_of the
carrier of
T )
by A30, Def14;
RelStr(# the
carrier of
X,the
InternalRel of
X #)
= RelStr(# the
carrier of
Y,the
InternalRel of
Y #)
by Def7;
then A34:
X in NetUniv T
by A33, Def14;
reconsider X' =
X as
net of
ConvergenceSpace C by Def27;
the
mapping of
X' is
constant
;
then reconsider X' =
X' as
constant net of
ConvergenceSpace C by Def6;
the_value_of X = q
by Th22;
then A35:
[X,q] in C
by A23, A34, Def23;
A36:
p in Lim M
by A26, A27, Def22;
reconsider Y' =
Y as
subnet of
M by A3;
defpred S1[
set ,
set ]
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 } );
A37:
for
x being
set st
x in the
carrier of
X holds
ex
j being
set st
S1[
x,
j]
consider J being
ManySortedSet of
such that A44:
for
x being
set st
x in the
carrier of
X holds
S1[
x,
J . x]
from PBOOLE:sch 3(A37);
reconsider J =
J as
yielding_non-empty_carriers net_set of the
carrier of
X,
T by A48, Th33;
for
i being
Element of
X holds
[(J . i),(X . i)] in C
then A49:
[(Iterated J),q] in C
by A23, A35, Def26;
A50:
RelStr(# the
carrier of
(Iterated J),the
InternalRel of
(Iterated J) #)
= [:X,(product J):]
by Def16;
then A51:
the
carrier of
(Iterated J) = [:the carrier of X,the carrier of (product J):]
by YELLOW_3:def 2;
Iterated J is
subnet of
Y
proof
deffunc H1(
Element of
Y)
-> set =
{ c where c is Element of Y : $1 <= c } ;
consider B being
ManySortedSet of
such that A52:
for
i being
Element of
Y holds
B . i = H1(
i)
from PBOOLE:sch 5();
then reconsider B =
B as
V2()
ManySortedSet of
by RELAT_1:def 9;
reconsider B' =
B as
V2()
ManySortedSet of
by A32;
deffunc H2(
Element of
X)
-> set = the
carrier of
(J . $1);
consider M being
ManySortedSet of
such that A56:
for
x being
Element of
X holds
M . x = H2(
x)
from PBOOLE:sch 5();
defpred S2[
set ,
set ,
set ]
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 );
A57:
for
i being
set st
i in the
carrier of
X holds
for
x being
set st
x in M . i holds
ex
y being
set st
(
y in B' . i &
S2[
y,
x,
i] )
proof
let i be
set ;
:: thesis: ( i in the carrier of X implies for x being set st x in M . i holds
ex y being set st
( y in B' . i & S2[y,x,i] ) )
assume A58:
i in the
carrier of
X
;
:: thesis: for x being set st x in M . i holds
ex y being set st
( y in B' . i & S2[y,x,i] )
let x be
set ;
:: thesis: ( x in M . i implies ex y being set st
( y in B' . i & S2[y,x,i] ) )
assume A59:
x in M . i
;
:: thesis: ex y being set st
( y in B' . i & S2[y,x,i] )
consider e being
Element of
Y,
Ji being
net of
T such that A60:
i = e
and A61:
Ji = J . i
and
[Ji,p] in C
and A62:
rng the
mapping of
Ji c= { (Y . c) where c is Element of Y : e <= c }
by A44, A58;
reconsider i' =
i as
Element of
X by A58;
defpred S3[
set ,
set ]
means the
mapping of
Ji . $1
= the
mapping of
Y . $2;
A63:
for
ji being
Element of
Ji ex
u being
Element of
B' . i' st
S3[
ji,
u]
consider f being
Function of the
carrier of
Ji,
(B' . i') such that A66:
for
ji being
Element of
Ji holds
S3[
ji,
f . ji]
from FUNCT_2:sch 3(A63);
reconsider f =
f as
Function of the
carrier of
Ji,
(B . i) ;
reconsider ji =
x as
Element of
Ji by A56, A58, A59, A61;
take
f . x
;
:: thesis: ( f . x in B' . i & S2[f . x,x,i] )
f . ji in B . i
;
hence
f . x in B' . i
;
:: thesis: S2[f . x,x,i]
take
f
;
:: thesis: 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
i'
;
:: thesis: ( f . x = f . x & i' = i & the mapping of (J . i') . x = the mapping of Y . (f . x) )
thus
(
f . x = f . x &
i' = i )
;
:: thesis: the mapping of (J . i') . x = the mapping of Y . (f . x)
thus the
mapping of
(J . i') . x =
the
mapping of
Ji . ji
by A61
.=
the
mapping of
Y . (f . x)
by A66
;
:: thesis: verum
end;
consider u being
ManySortedFunction of
M,
B' such that A67:
for
i being
set st
i in the
carrier of
X holds
ex
f being
Function of
(M . i),
(B' . i) st
(
f = u . i & ( for
x being
set st
x in M . i holds
S2[
f . x,
x,
i] ) )
from MSSUBFAM:sch 1(A57);
A68:
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)
deffunc H3(
Element of
X,
Element of
(product J))
-> set =
(u . $1) . ($2 . $1);
A71:
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):],the
carrier of
Y such that A76:
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(A71);
reconsider f =
f as
Function of
(Iterated J),
Y by A51;
take
f
;
:: according to YELLOW_6:def 12 :: thesis: ( 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 ) )
set h = the
mapping of
(Iterated J);
set g = the
mapping of
Y';
A77:
for
x being
set holds
(
x in dom the
mapping of
(Iterated J) iff (
x in dom f &
f . x in dom the
mapping of
Y' ) )
for
x being
set st
x in dom the
mapping of
(Iterated J) holds
the
mapping of
(Iterated J) . x = the
mapping of
Y' . (f . x)
hence
the
mapping of
(Iterated J) = the
mapping of
Y * f
by A77, FUNCT_1:20;
:: thesis: 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;
:: thesis: ex n being Element of (Iterated J) st
for p being Element of (Iterated J) st n <= p holds
m <= f . p
consider F being
Element of
(product J);
reconsider n =
[m,F] as
Element of
(Iterated J) by A32, A51, ZFMISC_1:106;
reconsider F =
F as
Element of
(product J) ;
reconsider m' =
m as
Element of
X by A32;
take
n
;
:: thesis: for p being Element of (Iterated J) st n <= p holds
m <= f . p
let p be
Element of
(Iterated J);
:: thesis: ( n <= p implies m <= f . p )
consider k' being
Element of
X,
G being
Element of
(product J) such that A82:
p = [k',G]
by A51, DOMAIN_1:9;
reconsider k =
k' as
Element of
Y by A32;
reconsider k'' =
k' as
Element of
X' ;
A83:
f . k',
G = (u . k) . (G . k)
by A76;
A84:
u . k is
Function of
(M . k),
(B . k)
by PBOOLE:def 18;
then A85:
dom (u . k) =
M . k
by FUNCT_2:def 1
.=
the
carrier of
(J . k')
by A56
.=
(Carrier J) . k''
by Th9
;
A86:
dom (Carrier J) = the
carrier of
X'
by PARTFUN1:def 4;
G in the
carrier of
(product J)
;
then
G in product (Carrier J)
by YELLOW_1:def 4;
then
G . k'' in dom (u . k)
by A85, A86, CARD_3:18;
then A87:
f . p in rng (u . k)
by A82, A83, FUNCT_1:def 5;
rng (u . k) c= B . k
by A84, RELAT_1:def 19;
then
f . p in B . k
by A87;
then
f . p in { c where c is Element of Y : k <= c }
by A52;
then consider c being
Element of
Y such that A88:
c = f . p
and A89:
k <= c
;
reconsider G =
G as
Element of
(product J) ;
reconsider k' =
k as
Element of
X ;
assume
n <= p
;
:: thesis: m <= f . p
then
[m',F] <= [k',G]
by A50, A82, Lm3;
then
m' <= k'
by YELLOW_3:11;
then
m <= k
by A32, Lm3;
hence
m <= f . p
by A88, A89, YELLOW_0:def 2;
:: thesis: verum
end;
hence
contradiction
by A31, A49;
:: thesis: verum
end;
C c= Convergence (ConvergenceSpace C)
by Th49;
hence
Convergence (ConvergenceSpace C) = C
by A24, XBOOLE_0:def 10; :: thesis: verum