set C = Convergence T;
thus
Convergence T is (CONSTANTS)
( Convergence T is (SUBNETS) & Convergence T is (DIVERGENCE) & Convergence T is (ITERATED_LIMITS) )
thus
Convergence T is (SUBNETS)
( Convergence T is (DIVERGENCE) & Convergence T is (ITERATED_LIMITS) )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 Convergence T holds
[Y,p] in Convergence Tlet Y be
subnet of
N;
( Y in NetUniv T implies for p being Element of T st [N,p] in Convergence T holds
[Y,p] in Convergence T )
assume A2:
Y in NetUniv T
;
for p being Element of T st [N,p] in Convergence T holds
[Y,p] in Convergence T
let p be
Element of
T;
( [N,p] in Convergence T implies [Y,p] in Convergence T )
assume
[N,p] in Convergence T
;
[Y,p] in Convergence T
then A3:
p in Lim N
by Def19;
Lim N c= Lim Y
by Th32;
hence
[Y,p] in Convergence T
by A2, A3, Def19;
verum
end;
thus
Convergence T is (DIVERGENCE)
Convergence T is (ITERATED_LIMITS) 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 Convergence T holds
ex Y being subnet of X st
( Y in NetUniv T & ( for Z being subnet of Y holds not [Z,p] in Convergence T ) )let p be
Element of
T;
( X in NetUniv T & not [X,p] in Convergence T implies ex Y being subnet of X st
( Y in NetUniv T & ( for Z being subnet of Y holds not [Z,p] in Convergence T ) ) )
assume A4:
X in NetUniv T
;
( [X,p] in Convergence T or ex Y being subnet of X st
( Y in NetUniv T & ( for Z being subnet of Y holds not [Z,p] in Convergence T ) ) )
assume
not
[X,p] in Convergence T
;
ex Y being subnet of X st
( Y in NetUniv T & ( for Z being subnet of Y holds not [Z,p] in Convergence T ) )
then
not
p in Lim X
by A4, Def19;
then consider Y being
subnet of
X such that A5:
Y in NetUniv T
and A6:
for
Z being
subnet of
Y holds not
p in Lim Z
by A4, Th38;
take
Y
;
( Y in NetUniv T & ( for Z being subnet of Y holds not [Z,p] in Convergence T ) )
thus
Y in NetUniv T
by A5;
for Z being subnet of Y holds not [Z,p] in Convergence T
let Z be
subnet of
Y;
not [Z,p] in Convergence T
not
p in Lim Z
by A6;
hence
not
[Z,p] in Convergence T
by Def19;
verum
end;
let X be net of T; YELLOW_6:def 23 for p being Element of T st [X,p] in Convergence T 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 Convergence T ) holds
[(Iterated J),p] in Convergence T
let p be Element of T; ( [X,p] in Convergence T 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 Convergence T ) holds
[(Iterated J),p] in Convergence T )
assume A7:
[X,p] in Convergence T
; for J being net_set of the carrier of X,T st ( for i being Element of X holds [(J . i),(X . i)] in Convergence T ) holds
[(Iterated J),p] in Convergence T
let J be net_set of the carrier of X,T; ( ( for i being Element of X holds [(J . i),(X . i)] in Convergence T ) implies [(Iterated J),p] in Convergence T )
assume A8:
for i being Element of X holds [(J . i),(X . i)] in Convergence T
; [(Iterated J),p] in Convergence T
X in NetUniv T
by A7, Def19;
then A10:
Iterated J in NetUniv T
by A9, Th25;
p in Lim X
by A7, Def19;
then
p in Lim (Iterated J)
by A9, Th39;
hence
[(Iterated J),p] in Convergence T
by A10, Def19; verum