let L be non empty complete Poset; :: thesis: ( Scott-Convergence L is (ITERATED_LIMITS) implies L is continuous )
assume A1:
Scott-Convergence L is (ITERATED_LIMITS)
; :: thesis: L is continuous
set C = Scott-Convergence L;
now let I be non
empty set ;
:: thesis: ( I in the_universe_of the carrier of L implies for K being V5 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
;
:: thesis: for K being V5 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
V5 ManySortedSet of
I;
:: thesis: ( ( 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
;
:: thesis: 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;
:: thesis: ( ( 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
;
:: thesis: Inf = Sup set x =
Inf ;
A5:
Inf >= Sup
by WAYBEL_5:16;
reconsider r =
[:I,I:] as
Relation of
I by RELSET_1:def 1;
dom F = I
by PBOOLE:def 3;
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
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 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
L
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 PBOOLE:def 3;
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 14;
then A20:
Iterated J in NetUniv L
by A14, YELLOW_6:34;
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: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
X,
Element of
product (doms F))
-> set =
{ (G . i,$2) where i is Element of X : 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
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 D' =
{ H5(i,g) where i is Element of X, 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
X for
g being
Element of
product (doms F) holds
H4(
g)
= H5(
i,
g)
proof
let j be
Element of
X;
:: thesis: for g being Element of product (doms F) holds H4(g) = H5(j,g)let g be
Element of
product (doms F);
:: thesis: 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 ;
:: thesis: ( 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 A25:
x in dom ((Frege F) . g)
and A26:
y = ((Frege F) . g) . x
;
:: thesis: y in H3(j,g)
A27:
x in dom F
by A12, A25, WAYBEL_5:8;
reconsider i' =
x as
Element of
I by A25;
reconsider i =
i' as
Element of
X ;
A28:
i >= j
by A6;
y =
(F . x) . (g . x)
by A12, A26, A27, 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 A28;
:: thesis: verum
end;
hence
"/\" (rng ((Frege F) . g)),
L = "/\" H3(
j,
g),
L
by FUNCT_1:def 5;
:: thesis: verum
end; A29:
{ ("/\" 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
A30:
the
carrier of
(Iterated J) = [:the carrier of X,(product (Carrier J)):]
by YELLOW_6:35;
A31:
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);
:: thesis: 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),Llet i be
Element of
X;
:: thesis: 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);
:: thesis: ( p = [i,g] implies "/\" H2(p),L = "/\" H3(i,g),L )
assume A32:
p = [i,g]
;
:: thesis: "/\" H2(p),L = "/\" H3(i,g),L
A33:
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
(product J) by A11, YELLOW_1:def 4;
g' in the
carrier of
(product J)
;
then A34:
g' in product (Carrier J)
by YELLOW_1:def 4;
reconsider i' =
i as
Element of
X ;
for
i being
set st
i in the
carrier of
X holds
ex
R being
RelStr ex
xi,
yi being
Element of
R st
(
R = J . i &
xi = g' . i &
yi = g' . i &
xi <= yi )
proof
let i be
set ;
:: thesis: ( i in the carrier of X implies ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = g' . i & yi = g' . i & xi <= yi ) )
assume
i in the
carrier of
X
;
:: thesis: ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = g' . i & yi = g' . i & xi <= yi )
then reconsider ii =
i as
Element of
X ;
reconsider i' =
ii as
Element of
I ;
A35:
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 A35;
then reconsider x =
g' . i as
Element of
(Net-Str (K . i'),(F . i')) ;
take
Net-Str (K . i'),
(F . i')
;
:: thesis: ex xi, yi being Element of (Net-Str (K . i'),(F . i')) st
( Net-Str (K . i'),(F . i') = J . i & xi = g' . i & yi = g' . i & xi <= yi )
take
x
;
:: thesis: ex yi being Element of (Net-Str (K . i'),(F . i')) st
( Net-Str (K . i'),(F . i') = J . i & x = g' . i & yi = g' . i & x <= yi )
take
x
;
:: thesis: ( 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;
:: thesis: verum
end;
then A36:
g' <= g'
by A34, YELLOW_1:def 4;
H3(
i,
g)
c= H2(
p)
proof
let u be
set ;
:: according to TARSKI:def 3 :: thesis: ( not u in H3(i,g) or u in H2(p) )
assume
u in H3(
i,
g)
;
:: thesis: u in H2(p)
then consider j being
Element of
X such that A37:
u = the
mapping of
(Iterated J) . j,
g
and A38:
j >= i
;
reconsider j' =
j as
Element of
X ;
reconsider q =
[j,g] as
Element of
(Iterated J) by A11, YELLOW_6:35;
[j',g'] >= [i',g']
by A36, A38, YELLOW_3:11;
then A39:
q >= p
by A32, A33, Lm1;
u = (Iterated J) . q
by A37;
hence
u in H2(
p)
by A39;
:: thesis: verum
end;
then A40:
"/\" H2(
p),
L <= "/\" H3(
i,
g),
L
by WAYBEL_7:3;
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;
:: according to YELLOW_4:def 2 :: thesis: ( not b in B or ex b1 being Element of the carrier of L st
( b1 in A & b1 <= b ) )
assume
b in B
;
:: thesis: 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 A41:
b = (Iterated J) . q
and A42:
p <= q
;
consider k being
Element of
X,
f being
Element of
product (Carrier J) such that A43:
q = [k,f]
by A30, DOMAIN_1:9;
reconsider k' =
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
;
:: thesis: ( a in A & a <= b )
reconsider f' =
f as
Element of
(product J) by YELLOW_1:def 4;
A44:
[k',f'] >= [i',g']
by A32, A33, A42, A43, Lm1;
then
i <= k
by YELLOW_3:11;
hence
a in A
;
:: thesis: a <= b
reconsider k' =
k as
Element of
I ;
set N =
Net-Str (K . k'),
(F . k');
A45:
J . k = Net-Str (K . k'),
(F . k')
by A8;
reconsider g'k =
g' . k,
f'k =
f' . k as
Element of
(Net-Str (K . k'),(F . k')) by A8;
A46:
b = (Net-Str (K . k'),(F . k')) . f'k
by A41, A43, A45, YELLOW_6:36;
reconsider kg =
[k,g] as
Element of
(Iterated J) by A11, YELLOW_6:35;
A47:
a =
(Iterated J) . kg
.=
(Net-Str (K . k'),(F . k')) . g'k
by A45, YELLOW_6:36
;
g' <= f'
by A44, YELLOW_3:11;
then
g' . k <= f' . k
by WAYBEL_3:28;
hence
a <= b
by A45, A46, A47, Def10;
:: thesis: verum
end;
then
"/\" H3(
i,
g),
L <= "/\" H2(
p),
L
by Th1;
hence
"/\" H2(
p),
L = "/\" H3(
i,
g),
L
by A40, YELLOW_0:def 3;
:: thesis: 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] }
:: according to XBOOLE_0:def 10 :: thesis: { 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
set ;
:: according to TARSKI:def 3 :: thesis: ( 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 }
;
:: thesis: 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 A48:
e = "/\" H2(
p),
L
;
consider j being
Element of
X,
g being
Element of
product (doms F) such that A49:
p = [j,g]
by A11, A30, DOMAIN_1:9;
e = "/\" H3(
j,
g),
L
by A31, A48, A49;
hence
e in { H5(i,g) where i is Element of X, g is Element of product (doms F) : S1[g] }
;
:: thesis: verum
end;
let e be
set ;
:: according to TARSKI:def 3 :: thesis: ( 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] }
;
:: thesis: 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 A50:
e = "/\" H3(
i,
g),
L
;
reconsider j =
[i,g] as
Element of
(Iterated J) by A11, YELLOW_6:35;
e = "/\" H2(
j),
L
by A31, A50;
hence
e in { ("/\" H2(j),L) where j is Element of (Iterated J) : verum }
;
:: thesis: verum
end; A51:
{ 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
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 A56:
Sup = lim_inf (Iterated J)
by A29, A51, YELLOW_2:def 5;
reconsider x' =
Inf as
Element of
L ;
set X1 =
{ (Inf ) where j' 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 } ;
A57:
{ ("/\" { (X . i) where i is Element of X : i >= j } ,L) where j is Element of X : verum } = { (Inf ) where j' 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 {x'}
by A57, 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 A56, Def7;
hence
Inf = Sup
by A5, ORDERS_2:25;
:: thesis: verum end;
hence
L is continuous
by WAYBEL_5:18; :: thesis: verum