let L be complete LATTICE; :: thesis: ( ( for J, K being non empty set
for F being Function of [:J,K:],the carrier of L
for X being Subset of L st X = { a where a is Element of L : ex f being V9() ManySortedSet of st
( f in Funcs J,(Fin K) & ex G being DoubleIndexedSet of f,L st
( ( for j being Element of J
for x being set st x in f . j holds
(G . j) . x = F . j,x ) & a = Inf ) ) } holds
Inf = sup X ) implies L is continuous )
assume A1:
for J, K being non empty set
for F being Function of [:J,K:],the carrier of L
for X being Subset of L st X = { a where a is Element of L : ex f being V9() ManySortedSet of st
( f in Funcs J,(Fin K) & ex G being DoubleIndexedSet of f,L st
( ( for j being Element of J
for x being set st x in f . j holds
(G . j) . x = F . j,x ) & a = Inf ) ) } holds
Inf = sup X
; :: thesis: L is continuous
for J, K being non empty set
for F being Function of [:J,K:],the carrier of L st ( for j being Element of J holds rng ((curry F) . j) is directed ) holds
Inf = Sup
proof
let J,
K be non
empty set ;
:: thesis: for F being Function of [:J,K:],the carrier of L st ( for j being Element of J holds rng ((curry F) . j) is directed ) holds
Inf = Sup let F be
Function of
[:J,K:],the
carrier of
L;
:: thesis: ( ( for j being Element of J holds rng ((curry F) . j) is directed ) implies Inf = Sup )
assume A2:
for
j being
Element of
J holds
rng ((curry F) . j) is
directed
;
:: thesis: Inf = Sup
defpred S1[
Element of
L]
means ex
f being
V9()
ManySortedSet of st
(
f in Funcs J,
(Fin K) & ex
G being
DoubleIndexedSet of
f,
L st
( ( for
j being
Element of
J for
x being
set st
x in f . j holds
(G . j) . x = F . j,
x ) & $1
= Inf ) );
reconsider X =
{ a where a is Element of L : S1[a] } as
Subset of
L from DOMAIN_1:sch 7();
X is_<=_than Sup
proof
let a' be
Element of
L;
:: according to LATTICE3:def 9 :: thesis: ( not a' in X or a' <= Sup )
assume
a' in X
;
:: thesis: a' <= Sup
then consider a being
Element of
L such that A3:
a' = a
and A4:
ex
f being
V9()
ManySortedSet of st
(
f in Funcs J,
(Fin K) & ex
G being
DoubleIndexedSet of
f,
L st
( ( for
j being
Element of
J for
x being
set st
x in f . j holds
(G . j) . x = F . j,
x ) &
a = Inf ) )
;
consider f being
V9()
ManySortedSet of
such that A5:
f in Funcs J,
(Fin K)
and A6:
ex
G being
DoubleIndexedSet of
f,
L st
( ( for
j being
Element of
J for
x being
set st
x in f . j holds
(G . j) . x = F . j,
x ) &
a = Inf )
by A4;
consider G being
DoubleIndexedSet of
f,
L such that A7:
for
j being
Element of
J for
x being
set st
x in f . j holds
(G . j) . x = F . j,
x
and A8:
a = Inf
by A6;
defpred S2[
set ,
set ]
means ( $1
in J & $2
in K & ex
b being
Element of
L st
(
b = ((curry F) . $1) . $2 &
a <= b ) );
A9:
for
x being
set st
x in J holds
ex
y being
set st
(
y in K &
S2[
x,
y] )
proof
let x be
set ;
:: thesis: ( x in J implies ex y being set st
( y in K & S2[x,y] ) )
assume
x in J
;
:: thesis: ex y being set st
( y in K & S2[x,y] )
then reconsider j =
x as
Element of
J ;
A10:
( not
rng ((curry F) . j) is
empty &
rng ((curry F) . j) is
directed )
by A2;
rng (G . j) is
finite Subset of
(rng ((curry F) . j))
by A5, A7, Lm12;
then consider y being
Element of
L such that A11:
y in rng ((curry F) . j)
and A12:
rng (G . j) is_<=_than y
by A10, WAYBEL_0:1;
consider k being
set such that A13:
k in dom ((curry F) . j)
and A14:
y = ((curry F) . j) . k
by A11, FUNCT_1:def 5;
reconsider k =
k as
Element of
K by A13, Th20;
take
k
;
:: thesis: ( k in K & S2[x,k] )
sup (rng (G . j)) <= y
by A12, YELLOW_0:32;
then A15:
Sup <= y
by YELLOW_2:def 5;
Sup in rng (Sups )
by Th14;
then
inf (rng (Sups )) <= Sup
by YELLOW_2:24;
then
Inf <= Sup
by YELLOW_2:def 6;
hence
(
k in K &
S2[
x,
k] )
by A8, A14, A15, ORDERS_2:26;
:: thesis: verum
end;
consider g being
Function such that A16:
dom g = J
and
rng g c= K
and A17:
for
x being
set st
x in J holds
S2[
x,
g . x]
from WELLORD2:sch 1(A9);
A18:
dom (doms (curry F)) = dom (curry F)
by FUNCT_6:89;
then A19:
dom g = dom (doms (curry F))
by A16, Th20;
for
x being
set st
x in dom (doms (curry F)) holds
g . x in (doms (curry F)) . x
then reconsider g =
g as
Element of
product (doms (curry F)) by A19, CARD_3:18;
for
j being
Element of
J holds
a <= ((Frege (curry F)) . g) . j
then A23:
a <= Inf
by YELLOW_2:57;
Inf in rng (Infs )
by Th14;
then
Inf <= sup (rng (Infs ))
by YELLOW_2:24;
then
Inf <= Sup
by YELLOW_2:def 5;
hence
a' <= Sup
by A3, A23, ORDERS_2:26;
:: thesis: verum
end;
then
sup X <= Sup
by YELLOW_0:32;
then A24:
Inf <= Sup
by A1;
Inf >= Sup
by Th16;
hence
Inf = Sup
by A24, ORDERS_2:25;
:: thesis: verum
end;
hence
L is continuous
by Lm10; :: thesis: verum