set C = Convergence T;
thus Convergence T is (CONSTANTS) :: thesis: ( Convergence T is (SUBNETS) & Convergence T is (DIVERGENCE) & Convergence T is (ITERATED_LIMITS) )
proof
let N be constant net of T; :: according to YELLOW_6:def 20 :: thesis: ( N in NetUniv T implies [N,(the_value_of N)] in Convergence T )
assume A1: N in NetUniv T ; :: thesis: [N,(the_value_of N)] in Convergence T
the_value_of N in Lim N by Th33;
hence [N,(the_value_of N)] in Convergence T by A1, Def19; :: thesis: verum
end;
thus Convergence T is (SUBNETS) :: thesis: ( Convergence T is (DIVERGENCE) & Convergence T is (ITERATED_LIMITS) )
proof
let N be net of T; :: according to YELLOW_6:def 21 :: thesis: 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 T
let Y be subnet of N; :: thesis: ( 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 ; :: thesis: for p being Element of T st [N,p] in Convergence T holds
[Y,p] in Convergence T
let p be Element of T; :: thesis: ( [N,p] in Convergence T implies [Y,p] in Convergence T )
assume [N,p] in Convergence T ; :: thesis: [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; :: thesis: verum
end;
thus Convergence T is (DIVERGENCE) :: thesis: Convergence T is (ITERATED_LIMITS)
proof
let X be net of T; :: according to YELLOW_6:def 22 :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( [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 ; :: thesis: 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 ; :: thesis: ( Y in NetUniv T & ( for Z being subnet of Y holds not [Z,p] in Convergence T ) )
thus Y in NetUniv T by A5; :: thesis: for Z being subnet of Y holds not [Z,p] in Convergence T
let Z be subnet of Y; :: thesis: not [Z,p] in Convergence T
not p in Lim Z by A6;
hence not [Z,p] in Convergence T by Def19; :: thesis: verum
end;
let X be net of T; :: according to YELLOW_6:def 23 :: thesis: 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; :: thesis: ( [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 ; :: 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 Convergence T ) holds
[(Iterated J),p] in Convergence T
let J be net_set of the carrier of X,T; :: thesis: ( ( 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 ; :: thesis: [(Iterated J),p] in Convergence T
A9: now :: thesis: for i being Element of X holds
( X . i in Lim (J . i) & J . i in NetUniv T )
let i be Element of X; :: thesis: ( X . i in Lim (J . i) & J . i in NetUniv T )
[(J . i),(X . i)] in Convergence T by A8;
hence ( X . i in Lim (J . i) & J . i in NetUniv T ) by Def19; :: thesis: verum
end;
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; :: thesis: verum