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 for I being non empty set st I in the_universe_of the carrier of L holds
for K being V8() ManySortedSet of I st ( for j being Element of I holds K . j in the_universe_of the carrier of L ) holds
for F being DoubleIndexedSet of K,L st ( for j being Element of I holds rng (F . j) is directed ) holds
Inf = Sup let I be non
empty set ;
( I in the_universe_of the carrier of L implies for K being V8() ManySortedSet of I st ( for j being Element of I holds K . j in the_universe_of the carrier of L ) holds
for F being DoubleIndexedSet of K,L 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 V8() ManySortedSet of I st ( for j being Element of I holds K . j in the_universe_of the carrier of L ) holds
for F being DoubleIndexedSet of K,L st ( for j being Element of I holds rng (F . j) is directed ) holds
Inf = Sup let K be
V8()
ManySortedSet of
I;
( ( for j being Element of I holds K . j in the_universe_of the carrier of L ) implies for F being DoubleIndexedSet of K,L 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 K,L st ( for j being Element of I holds rng (F . j) is directed ) holds
Inf = Sup let F be
DoubleIndexedSet of
K,
L;
( ( 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
I ;
dom F = I
by PARTFUN1:def 2;
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
NetStr(#
I,
r,
f #) holds
i <= j
A7:
NetStr(#
I,
r,
f #) is
transitive
by A6;
NetStr(#
I,
r,
f #) is
directed
then reconsider X =
NetStr(#
I,
r,
f #) as
strict net of
L by A7;
deffunc H1(
Element of
I)
-> non
empty strict NetStr over
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
L
then reconsider J =
J as
net_set of the
carrier of
X,
L by YELLOW_6:24;
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 15
;
A12:
dom (Frege F) = product (doms F)
by PARTFUN1:def 2;
then A13:
dom (Infs ) = product (doms F)
by FUNCT_2:def 1;
A14:
for
i being
Element of
X holds
J . i in NetUniv L
A16:
for
i being
Element of
X holds
[(J . i),(X . i)] in Scott-Convergence L
A19:
X in NetUniv L
by A2, YELLOW_6:def 11;
then A20:
Iterated J in NetUniv L
by A14, YELLOW_6:25;
deffunc H2(
Element of
(Iterated J))
-> set =
{ ((Iterated J) . p) where p is Element of (Iterated J) : p >= $1 } ;
the
carrier of
(Iterated J) = [: the carrier of X,(product (Carrier J)):]
by YELLOW_6:26;
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
X,
Element of
product (doms F))
-> set =
{ (G . (i,$2)) where i is Element of X : i >= $1 } ;
deffunc H4(
Element of
product (doms F))
-> Element of the
carrier of
L =
"/\" (
(rng ((Frege F) . $1)),
L);
deffunc H5(
Element of
X,
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 (Iterated J) : verum } ;
set D9 =
{ H5(i,g) where i is Element of X, g is Element of product (doms F) : S1[g] } ;
set E9 =
{ H4(g) where g is Element of product (doms F) : S1[g] } ;
A21:
for
i being
Element of
X for
g being
Element of
product (doms F) holds
H4(
g)
= H5(
i,
g)
proof
let j be
Element of
X;
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
object holds
(
y in H3(
j,
g) iff ex
x being
object st
(
x in dom ((Frege F) . g) &
y = ((Frege F) . g) . x ) )
proof
let y be
object ;
( y in H3(j,g) iff ex x being object 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
object 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 i9 =
x as
Element of
I by A26;
reconsider i =
i9 as
Element of
X ;
A29:
i >= j
by A6;
y =
(F . x) . (g . x)
by A12, A27, A28, WAYBEL_5:9
.=
the
mapping of
(Net-Str ((K . i9),(F . i9))) . (g . i)
by Def10
.=
the
mapping of
(J . i) . (g . i)
by A8
.=
G . (
i,
g)
by A22, YELLOW_6:def 13
;
hence
y in H3(
j,
g)
by A29;
verum
end;
hence
H4(
g)
= H5(
j,
g)
by FUNCT_1:def 3;
verum
end; A30:
{ ("/\" (H2(j),L)) where j is Element of (Iterated J) : verum } = { H5(i,g) where i is Element of X, 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:26;
A32:
for
p being
Element of
(Iterated J) for
i being
Element of
X 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
(Iterated J);
for i being Element of X
for g being Element of product (doms F) st p = [i,g] holds
"/\" (H2(p),L) = "/\" (H3(i,g),L)let i be
Element of
X;
for g being Element of product (doms F) st p = [i,g] holds
"/\" (H2(p),L) = "/\" (H3(i,g),L)let 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 13;
reconsider g9 =
g as
Element of
(product J) by A11, YELLOW_1:def 4;
g9 in the
carrier of
(product J)
;
then A35:
g9 in product (Carrier J)
by YELLOW_1:def 4;
reconsider i9 =
i as
Element of
X ;
for
i being
object st
i in the
carrier of
X holds
ex
R being
RelStr ex
xi,
yi being
Element of
R st
(
R = J . i &
xi = g9 . i &
yi = g9 . i &
xi <= yi )
proof
let i be
object ;
( i in the carrier of X implies ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = g9 . i & yi = g9 . i & xi <= yi ) )
assume
i in the
carrier of
X
;
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = g9 . i & yi = g9 . i & xi <= yi )
then reconsider ii =
i as
Element of
X ;
reconsider i9 =
ii as
Element of
I ;
A36:
J . i = Net-Str (
(K . i9),
(F . i9))
by A8;
set R =
Net-Str (
(K . i9),
(F . i9));
g9 . ii in the
carrier of
(Net-Str ((K . i9),(F . i9)))
by A36;
then reconsider x =
g9 . i as
Element of
(Net-Str ((K . i9),(F . i9))) ;
take
Net-Str (
(K . i9),
(F . i9))
;
ex xi, yi being Element of (Net-Str ((K . i9),(F . i9))) st
( Net-Str ((K . i9),(F . i9)) = J . i & xi = g9 . i & yi = g9 . i & xi <= yi )
take
x
;
ex yi being Element of (Net-Str ((K . i9),(F . i9))) st
( Net-Str ((K . i9),(F . i9)) = J . i & x = g9 . i & yi = g9 . i & x <= yi )
take
x
;
( Net-Str ((K . i9),(F . i9)) = J . i & x = g9 . i & x = g9 . i & x <= x )
x <= x
;
hence
(
Net-Str (
(K . i9),
(F . i9))
= J . i &
x = g9 . i &
x = g9 . i &
x <= x )
by A8;
verum
end;
then A37:
g9 <= g9
by A35, YELLOW_1:def 4;
H3(
i,
g)
c= H2(
p)
proof
let u be
object ;
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
X such that A38:
u = the
mapping of
(Iterated J) . (
j,
g)
and A39:
j >= i
;
reconsider j9 =
j as
Element of
X ;
reconsider q =
[j,g] as
Element of
(Iterated J) by A11, YELLOW_6:26;
[j9,g9] >= [i9,g9]
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:1;
defpred S2[
Element of
X]
means $1
>= i;
deffunc H6(
Element of
X)
-> Element of the
carrier of
L =
G . ($1,
g);
{ H6(k) where k is Element of X : S2[k] } is
Subset of
L
from DOMAIN_1:sch 8();
then reconsider A =
H3(
i,
g) as
Subset of
L ;
defpred S3[
Element of
(Iterated J)]
means $1
>= p;
deffunc H7(
Element of
(Iterated J))
-> Element of the
carrier of
L =
(Iterated J) . $1;
{ H7(z) where z is Element of (Iterated J) : S3[z] } is
Subset of
L
from DOMAIN_1:sch 8();
then reconsider B =
H2(
p) as
Subset of
L ;
B is_coarser_than A
proof
let b be
Element of
L;
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
(Iterated J) such that A42:
b = (Iterated J) . q
and A43:
p <= q
;
consider k being
Element of
X,
f being
Element of
product (Carrier J) such that A44:
q = [k,f]
by A31, DOMAIN_1:1;
reconsider k9 =
k as
Element of
X ;
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
L ;
take
a
;
( a in A & a <= b )
reconsider f9 =
f as
Element of
(product J) by YELLOW_1:def 4;
A45:
[k9,f9] >= [i9,g9]
by A33, A34, A43, A44, Lm1;
then
i <= k
by YELLOW_3:11;
hence
a in A
;
a <= b
reconsider k9 =
k as
Element of
I ;
set N =
Net-Str (
(K . k9),
(F . k9));
A46:
J . k = Net-Str (
(K . k9),
(F . k9))
by A8;
reconsider g9k =
g9 . k,
f9k =
f9 . k as
Element of
(Net-Str ((K . k9),(F . k9))) by A8;
A47:
b = (Net-Str ((K . k9),(F . k9))) . f9k
by A42, A44, A46, YELLOW_6:27;
reconsider kg =
[k,g] as
Element of
(Iterated J) by A11, YELLOW_6:26;
A48:
a =
(Iterated J) . kg
.=
(Net-Str ((K . k9),(F . k9))) . g9k
by A46, YELLOW_6:27
;
g9 <= f9
by A45, YELLOW_3:11;
then
g9 . k <= f9 . 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 (Iterated J) : verum } c= { H5(i,g) where i is Element of X, g is Element of product (doms F) : S1[g] }
XBOOLE_0:def 10 { H5(i,g) where i is Element of X, g is Element of product (doms F) : S1[g] } c= { ("/\" (H2(j),L)) where j is Element of (Iterated J) : verum } proof
let e be
object ;
TARSKI:def 3 ( not e in { ("/\" (H2(j),L)) where j is Element of (Iterated J) : verum } or e in { H5(i,g) where i is Element of X, g is Element of product (doms F) : S1[g] } )
assume
e in { ("/\" (H2(j),L)) where j is Element of (Iterated J) : verum }
;
e in { H5(i,g) where i is Element of X, g is Element of product (doms F) : S1[g] }
then consider p being
Element of
(Iterated J) such that A49:
e = "/\" (
H2(
p),
L)
;
consider j being
Element of
X,
g being
Element of
product (doms F) such that A50:
p = [j,g]
by A11, A31, DOMAIN_1:1;
e = "/\" (
H3(
j,
g),
L)
by A32, A49, A50;
hence
e in { H5(i,g) where i is Element of X, g is Element of product (doms F) : S1[g] }
;
verum
end;
let e be
object ;
TARSKI:def 3 ( not e in { H5(i,g) where i is Element of X, g is Element of product (doms F) : S1[g] } or e in { ("/\" (H2(j),L)) where j is Element of (Iterated J) : verum } )
assume
e in { H5(i,g) where i is Element of X, g is Element of product (doms F) : S1[g] }
;
e in { ("/\" (H2(j),L)) where j is Element of (Iterated J) : verum }
then consider i being
Element of
X,
g being
Element of
product (doms F) such that A51:
e = "/\" (
H3(
i,
g),
L)
;
reconsider j =
[i,g] as
Element of
(Iterated J) by A11, YELLOW_6:26;
e = "/\" (
H2(
j),
L)
by A32, A51;
hence
e in { ("/\" (H2(j),L)) where j is Element of (Iterated J) : verum }
;
verum
end; A52:
{ H4(g) where g is Element of product (doms F) : S1[g] } = { H5(i,g) where i is Element of X, g is Element of product (doms F) : S1[g] }
from WAYBEL11:sch 1(A21);
for
y being
object holds
(
y in { H4(g) where g is Element of product (doms F) : S1[g] } iff ex
x being
object 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 3;
then A57:
Sup = lim_inf (Iterated J)
by A30, A52, YELLOW_2:def 5;
reconsider x9 =
Inf as
Element of
L ;
set X1 =
{ (Inf ) where j9 is Element of X : verum } ;
set X2 =
{ ("/\" ( { (X . i) where i is Element of X : i >= j } ,L)) where j is Element of X : verum } ;
A58:
{ ("/\" ( { (X . i) where i is Element of X : i >= j } ,L)) where j is Element of X : verum } = { (Inf ) where j9 is Element of X : verum }
then "\/" (
{ ("/\" ( { (X . i) where i is Element of X : i >= j } ,L)) where j is Element of X : verum } ,
L) =
sup {x9}
by A58, TARSKI:2
.=
Inf
by YELLOW_0:39
;
then
Inf <= lim_inf X
;
then
Inf is_S-limit_of X
;
then
[X,(Inf )] in Scott-Convergence L
by A19, Def8;
then
[(Iterated J),(Inf )] in Scott-Convergence L
by A1, A16;
then
Inf is_S-limit_of Iterated J
by A20, Def8;
then
Inf <= Sup
by A57;
hence
Inf = Sup
by A5, ORDERS_2:2;
verum end;
hence
L is continuous
by WAYBEL_5:18; verum