let L be non empty complete Poset; ( Scott-Convergence L is (ITERATED_LIMITS) implies L is continuous )
assume A1:
Scott-Convergence L is (ITERATED_LIMITS)
; L is continuous
set C = Scott-Convergence L;
now let I be non
empty set ;
( I in the_universe_of the carrier of L implies for K being V5() ManySortedSet of st ( for j being Element of I holds K . j in the_universe_of the carrier of L ) holds
for F being DoubleIndexedSet of I, st ( for j being Element of I holds rng (F . j) is directed ) holds
Inf = Sup )assume A2:
I in the_universe_of the
carrier of
L
;
for K being V5() ManySortedSet of st ( for j being Element of I holds K . j in the_universe_of the carrier of L ) holds
for F being DoubleIndexedSet of I, st ( for j being Element of I holds rng (F . j) is directed ) holds
Inf = Sup let K be
V5()
ManySortedSet of ;
( ( for j being Element of I holds K . j in the_universe_of the carrier of L ) implies for F being DoubleIndexedSet of I, st ( for j being Element of I holds rng (F . j) is directed ) holds
Inf = Sup )assume A3:
for
j being
Element of
I holds
K . j in the_universe_of the
carrier of
L
;
for F being DoubleIndexedSet of I, st ( for j being Element of I holds rng (F . j) is directed ) holds
Inf = Sup let F be
DoubleIndexedSet of
I,;
( ( for j being Element of I holds rng (F . j) is directed ) implies Inf = Sup )assume A4:
for
j being
Element of
I holds
rng (F . j) is
directed
;
Inf = Sup set x =
Inf ;
A5:
Inf >= Sup
by WAYBEL_5:16;
[:I,I:] c= [:I,I:]
;
then reconsider r =
[:I,I:] as
Relation of ;
dom F = I
by PARTFUN1:def 4;
then reconsider f =
Sups as
Function of
I,the
carrier of
L ;
set X =
NetStr(#
I,
r,
f #);
A6:
for
i,
j being
Element of holds
i <= j
A7:
NetStr(#
I,
r,
f #) is
transitive
NetStr(#
I,
r,
f #) is
directed
then reconsider X =
NetStr(#
I,
r,
f #) as
strict net of
strict by A7;
deffunc H1(
Element of
I)
-> non
empty strict NetStr of
L =
Net-Str (K . $1),
(F . $1);
consider J being
ManySortedSet of
I such that A8:
for
i being
Element of
I holds
J . i = H1(
i)
from PBOOLE:sch 5();
for
i being
set st
i in the
carrier of
X holds
J . i is
net of
then reconsider J =
J as
net_set of the
carrier of
X,
L by YELLOW_6:33;
A10:
for
j being
set st
j in I holds
ex
R being
1-sorted st
(
R = J . j &
K . j = the
carrier of
R )
A11:
doms F =
K
by YELLOW_7:45
.=
Carrier J
by A10, PRALG_1:def 13
;
A12:
dom (Frege F) = product (doms F)
by PARTFUN1:def 4;
then A13:
dom (Infs ) = product (doms F)
by FUNCT_2:def 1;
A14:
for
i being
Element of holds
J . i in NetUniv L
A16:
for
i being
Element of holds
[(J . i),(X . i)] in Scott-Convergence L
A19:
X in NetUniv L
by A2, YELLOW_6:def 14;
then A20:
Iterated J in NetUniv L
by A14, YELLOW_6:34;
deffunc H2(
Element of )
-> set =
{ ((Iterated J) . p) where p is Element of : p >= $1 } ;
the
carrier of
(Iterated J) = [:the carrier of X,(product (Carrier J)):]
by YELLOW_6:35;
then reconsider G = the
mapping of
(Iterated J) as
Function of
[:the carrier of X,(product (doms F)):],the
carrier of
L by A11;
deffunc H3(
Element of ,
Element of
product (doms F))
-> set =
{ (G . i,$2) where i is Element of : i >= $1 } ;
defpred S1[
set ]
means verum;
deffunc H4(
Element of
product (doms F))
-> Element of the
carrier of
L =
"/\" (rng ((Frege F) . $1)),
L;
deffunc H5(
Element of ,
Element of
product (doms F))
-> Element of the
carrier of
L =
"/\" H3($1,$2),
L;
set D =
{ ("/\" H2(j),L) where j is Element of : verum } ;
set D' =
{ H5(i,g) where i is Element of , g is Element of product (doms F) : S1[g] } ;
set E' =
{ H4(g) where g is Element of product (doms F) : S1[g] } ;
A21:
for
i being
Element of
for
g being
Element of
product (doms F) holds
H4(
g)
= H5(
i,
g)
proof
let j be
Element of ;
for g being Element of product (doms F) holds H4(g) = H5(j,g)let g be
Element of
product (doms F);
H4(g) = H5(j,g)
for
y being
set holds
(
y in H3(
j,
g) iff ex
x being
set st
(
x in dom ((Frege F) . g) &
y = ((Frege F) . g) . x ) )
proof
let y be
set ;
( y in H3(j,g) iff ex x being set st
( x in dom ((Frege F) . g) & y = ((Frege F) . g) . x ) )
g in product (Carrier J)
by A11;
then A22:
g in the
carrier of
(product J)
by YELLOW_1:def 4;
given x being
set such that A26:
x in dom ((Frege F) . g)
and A27:
y = ((Frege F) . g) . x
;
y in H3(j,g)
A28:
x in dom F
by A12, A26, WAYBEL_5:8;
reconsider i' =
x as
Element of
I by A26;
reconsider i =
i' as
Element of ;
A29:
i >= j
by A6;
y =
(F . x) . (g . x)
by A12, A27, A28, WAYBEL_5:9
.=
the
mapping of
(Net-Str (K . i'),(F . i')) . (g . i)
by Def10
.=
the
mapping of
(J . i) . (g . i)
by A8
.=
G . i,
g
by A22, YELLOW_6:def 16
;
hence
y in H3(
j,
g)
by A29;
verum
end;
hence
H4(
g)
= H5(
j,
g)
by FUNCT_1:def 5;
verum
end; A30:
{ ("/\" H2(j),L) where j is Element of : verum } = { H5(i,g) where i is Element of , g is Element of product (doms F) : S1[g] }
proof
A31:
the
carrier of
(Iterated J) = [:the carrier of X,(product (Carrier J)):]
by YELLOW_6:35;
A32:
for
p being
Element of
for
i being
Element of
for
g being
Element of
product (doms F) st
p = [i,g] holds
"/\" H2(
p),
L = "/\" H3(
i,
g),
L
proof
let p be
Element of ;
for i being Element of
for g being Element of product (doms F) st p = [i,g] holds
"/\" H2(p),L = "/\" H3(i,g),Llet i be
Element of ;
for g being Element of product (doms F) st p = [i,g] holds
"/\" H2(p),L = "/\" H3(i,g),Llet g be
Element of
product (doms F);
( p = [i,g] implies "/\" H2(p),L = "/\" H3(i,g),L )
assume A33:
p = [i,g]
;
"/\" H2(p),L = "/\" H3(i,g),L
A34:
RelStr(# the
carrier of
(Iterated J),the
InternalRel of
(Iterated J) #)
= RelStr(# the
carrier of
[:X,(product J):],the
InternalRel of
[:X,(product J):] #)
by YELLOW_6:def 16;
reconsider g' =
g as
Element of
by A11, YELLOW_1:def 4;
g' in the
carrier of
(product J)
;
then A35:
g' in product (Carrier J)
by YELLOW_1:def 4;
reconsider i' =
i as
Element of ;
for
i being
set st
i in the
carrier of
X holds
ex
R being
RelStr ex
xi,
yi being
Element of st
(
R = J . i &
xi = g' . i &
yi = g' . i &
xi <= yi )
proof
let i be
set ;
( i in the carrier of X implies ex R being RelStr ex xi, yi being Element of st
( R = J . i & xi = g' . i & yi = g' . i & xi <= yi ) )
assume
i in the
carrier of
X
;
ex R being RelStr ex xi, yi being Element of st
( R = J . i & xi = g' . i & yi = g' . i & xi <= yi )
then reconsider ii =
i as
Element of ;
reconsider i' =
ii as
Element of
I ;
A36:
J . i = Net-Str (K . i'),
(F . i')
by A8;
set R =
Net-Str (K . i'),
(F . i');
g' . ii in the
carrier of
(Net-Str (K . i'),(F . i'))
by A36;
then reconsider x =
g' . i as
Element of ;
take
Net-Str (K . i'),
(F . i')
;
ex xi, yi being Element of st
( Net-Str (K . i'),(F . i') = J . i & xi = g' . i & yi = g' . i & xi <= yi )
take
x
;
ex yi being Element of st
( Net-Str (K . i'),(F . i') = J . i & x = g' . i & yi = g' . i & x <= yi )
take
x
;
( Net-Str (K . i'),(F . i') = J . i & x = g' . i & x = g' . i & x <= x )
x <= x
;
hence
(
Net-Str (K . i'),
(F . i') = J . i &
x = g' . i &
x = g' . i &
x <= x )
by A8;
verum
end;
then A37:
g' <= g'
by A35, YELLOW_1:def 4;
H3(
i,
g)
c= H2(
p)
proof
let u be
set ;
TARSKI:def 3 ( not u in H3(i,g) or u in H2(p) )
assume
u in H3(
i,
g)
;
u in H2(p)
then consider j being
Element of
such that A38:
u = the
mapping of
(Iterated J) . j,
g
and A39:
j >= i
;
reconsider j' =
j as
Element of ;
reconsider q =
[j,g] as
Element of
by A11, YELLOW_6:35;
[j',g'] >= [i',g']
by A37, A39, YELLOW_3:11;
then A40:
q >= p
by A33, A34, Lm1;
u = (Iterated J) . q
by A38;
hence
u in H2(
p)
by A40;
verum
end;
then A41:
"/\" H2(
p),
L <= "/\" H3(
i,
g),
L
by WAYBEL_7:3;
defpred S2[
Element of ]
means $1
>= i;
deffunc H6(
Element of )
-> Element of the
carrier of
L =
G . $1,
g;
{ H6(k) where k is Element of : S2[k] } is
Subset of
from DOMAIN_1:sch 8();
then reconsider A =
H3(
i,
g) as
Subset of ;
defpred S3[
Element of ]
means $1
>= p;
deffunc H7(
Element of )
-> Element of the
carrier of
L =
(Iterated J) . $1;
{ H7(z) where z is Element of : S3[z] } is
Subset of
from DOMAIN_1:sch 8();
then reconsider B =
H2(
p) as
Subset of ;
B is_coarser_than A
proof
let b be
Element of ;
YELLOW_4:def 2 ( not b in B or ex b1 being Element of the carrier of L st
( b1 in A & b1 <= b ) )
assume
b in B
;
ex b1 being Element of the carrier of L st
( b1 in A & b1 <= b )
then consider q being
Element of
such that A42:
b = (Iterated J) . q
and A43:
p <= q
;
consider k being
Element of ,
f being
Element of
product (Carrier J) such that A44:
q = [k,f]
by A31, DOMAIN_1:9;
reconsider k' =
k as
Element of ;
set a = the
mapping of
(Iterated J) . k,
g;
the
mapping of
(Iterated J) . k,
g = G . k,
g
;
then reconsider a = the
mapping of
(Iterated J) . k,
g as
Element of ;
take
a
;
( a in A & a <= b )
reconsider f' =
f as
Element of
by YELLOW_1:def 4;
A45:
[k',f'] >= [i',g']
by A33, A34, A43, A44, Lm1;
then
i <= k
by YELLOW_3:11;
hence
a in A
;
a <= b
reconsider k' =
k as
Element of
I ;
set N =
Net-Str (K . k'),
(F . k');
A46:
J . k = Net-Str (K . k'),
(F . k')
by A8;
reconsider g'k =
g' . k,
f'k =
f' . k as
Element of
by A8;
A47:
b = (Net-Str (K . k'),(F . k')) . f'k
by A42, A44, A46, YELLOW_6:36;
reconsider kg =
[k,g] as
Element of
by A11, YELLOW_6:35;
A48:
a =
(Iterated J) . kg
.=
(Net-Str (K . k'),(F . k')) . g'k
by A46, YELLOW_6:36
;
g' <= f'
by A45, YELLOW_3:11;
then
g' . k <= f' . k
by WAYBEL_3:28;
hence
a <= b
by A46, A47, A48, Def10;
verum
end;
then
"/\" H3(
i,
g),
L <= "/\" H2(
p),
L
by Th1;
hence
"/\" H2(
p),
L = "/\" H3(
i,
g),
L
by A41, YELLOW_0:def 3;
verum
end;
thus
{ ("/\" H2(j),L) where j is Element of : verum } c= { H5(i,g) where i is Element of , g is Element of product (doms F) : S1[g] }
XBOOLE_0:def 10 { H5(i,g) where i is Element of , g is Element of product (doms F) : S1[g] } c= { ("/\" H2(j),L) where j is Element of : verum } proof
let e be
set ;
TARSKI:def 3 ( not e in { ("/\" H2(j),L) where j is Element of : verum } or e in { H5(i,g) where i is Element of , g is Element of product (doms F) : S1[g] } )
assume
e in { ("/\" H2(j),L) where j is Element of : verum }
;
e in { H5(i,g) where i is Element of , g is Element of product (doms F) : S1[g] }
then consider p being
Element of
such that A49:
e = "/\" H2(
p),
L
;
consider j being
Element of ,
g being
Element of
product (doms F) such that A50:
p = [j,g]
by A11, A31, DOMAIN_1:9;
e = "/\" H3(
j,
g),
L
by A32, A49, A50;
hence
e in { H5(i,g) where i is Element of , g is Element of product (doms F) : S1[g] }
;
verum
end;
let e be
set ;
TARSKI:def 3 ( not e in { H5(i,g) where i is Element of , g is Element of product (doms F) : S1[g] } or e in { ("/\" H2(j),L) where j is Element of : verum } )
assume
e in { H5(i,g) where i is Element of , g is Element of product (doms F) : S1[g] }
;
e in { ("/\" H2(j),L) where j is Element of : verum }
then consider i being
Element of ,
g being
Element of
product (doms F) such that A51:
e = "/\" H3(
i,
g),
L
;
reconsider j =
[i,g] as
Element of
by A11, YELLOW_6:35;
e = "/\" H2(
j),
L
by A32, A51;
hence
e in { ("/\" H2(j),L) where j is Element of : verum }
;
verum
end; A52:
{ H4(g) where g is Element of product (doms F) : S1[g] } = { H5(i,g) where i is Element of , g is Element of product (doms F) : S1[g] }
from WAYBEL11:sch 1(A21);
for
y being
set holds
(
y in { H4(g) where g is Element of product (doms F) : S1[g] } iff ex
x being
set st
(
x in dom (Infs ) &
y = (Infs ) . x ) )
then
rng (Infs ) = { H4(g) where g is Element of product (doms F) : S1[g] }
by FUNCT_1:def 5;
then A57:
Sup = lim_inf (Iterated J)
by A30, A52, YELLOW_2:def 5;
reconsider x' =
Inf as
Element of ;
set X1 =
{ (Inf ) where j' is Element of : verum } ;
set X2 =
{ ("/\" { (X . i) where i is Element of : i >= j } ,L) where j is Element of : verum } ;
A58:
{ ("/\" { (X . i) where i is Element of : i >= j } ,L) where j is Element of : verum } = { (Inf ) where j' is Element of : verum }
then "\/" { ("/\" { (X . i) where i is Element of : i >= j } ,L) where j is Element of : verum } ,
L =
sup {x'}
by A58, TARSKI:2
.=
Inf
by YELLOW_0:39
;
then
Inf <= lim_inf X
;
then
Inf is_S-limit_of X
by Def7;
then
[X,(Inf )] in Scott-Convergence L
by A19, Def8;
then
[(Iterated J),(Inf )] in Scott-Convergence L
by A1, A16, YELLOW_6:def 26;
then
Inf is_S-limit_of Iterated J
by A20, Def8;
then
Inf <= Sup
by A57, Def7;
hence
Inf = Sup
by A5, ORDERS_2:25;
verum end;
hence
L is continuous
by WAYBEL_5:18; verum