let L be complete LATTICE; ( ( 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 J st
( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st
( ( for j being Element of J
for x being object 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 J st
( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st
( ( for j being Element of J
for x being object st x in f . j holds
(G . j) . x = F . (j,x) ) & a = Inf ) ) } holds
Inf = sup X
; 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 ;
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;
( ( 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
;
Inf = Sup
defpred S1[
Element of
L]
means ex
f being
V9()
ManySortedSet of
J st
(
f in Funcs (
J,
(Fin K)) & ex
G being
DoubleIndexedSet of
f,
L st
( ( for
j being
Element of
J for
x being
object 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 a9 be
Element of
L;
LATTICE3:def 9 ( not a9 in X or a9 <= Sup )
assume
a9 in X
;
a9 <= Sup
then consider a being
Element of
L such that A3:
a9 = a
and A4:
ex
f being
V9()
ManySortedSet of
J st
(
f in Funcs (
J,
(Fin K)) & ex
G being
DoubleIndexedSet of
f,
L st
( ( for
j being
Element of
J for
x being
object st
x in f . j holds
(G . j) . x = F . (
j,
x) ) &
a = Inf ) )
;
defpred S2[
object ,
object ]
means ( $1
in J & $2
in K & ex
b being
Element of
L st
(
b = ((curry F) . $1) . $2 &
a <= b ) );
consider f being
V9()
ManySortedSet of
J 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
object 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
object st
x in f . j holds
(G . j) . x = F . (
j,
x)
and A8:
a = Inf
by A6;
A9:
for
x being
object st
x in J holds
ex
y being
object st
(
y in K &
S2[
x,
y] )
proof
let x be
object ;
( x in J implies ex y being object st
( y in K & S2[x,y] ) )
assume
x in J
;
ex y being object st
( y in K & S2[x,y] )
then reconsider j =
x as
Element of
J ;
Sup in rng (Sups )
by Th14;
then
inf (rng (Sups )) <= Sup
by YELLOW_2:22;
then A10:
Inf <= Sup
by YELLOW_2:def 6;
( not
rng ((curry F) . j) is
empty &
rng ((curry F) . j) is
directed &
rng (G . j) is
finite Subset of
(rng ((curry F) . j)) )
by A2, 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 WAYBEL_0:1;
consider k being
object such that A13:
k in dom ((curry F) . j)
and A14:
y = ((curry F) . j) . k
by A11, FUNCT_1:def 3;
reconsider k =
k as
Element of
K by A13;
take
k
;
( k in K & S2[x,k] )
sup (rng (G . j)) <= y
by A12, YELLOW_0:32;
then
Sup <= y
by YELLOW_2:def 5;
hence
(
k in K &
S2[
x,
k] )
by A8, A14, A10, ORDERS_2:3;
verum
end;
consider g being
Function such that A15:
dom g = J
and
rng g c= K
and A16:
for
x being
object st
x in J holds
S2[
x,
g . x]
from FUNCT_1:sch 6(A9);
A17:
dom (doms (curry F)) = dom (curry F)
by FUNCT_6:59;
then A18:
dom g = dom (doms (curry F))
by A15, Th20;
for
x being
object 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 A18, CARD_3:9;
for
j being
Element of
J holds
a <= ((Frege (curry F)) . g) . j
then A20:
a <= Inf
by YELLOW_2:55;
Inf in rng (Infs )
by Th14;
then
Inf <= sup (rng (Infs ))
by YELLOW_2:22;
then
Inf <= Sup
by YELLOW_2:def 5;
hence
a9 <= Sup
by A3, A20, ORDERS_2:3;
verum
end;
then
sup X <= Sup
by YELLOW_0:32;
then A21:
Inf <= Sup
by A1;
Inf >= Sup
by Th16;
hence
Inf = Sup
by A21, ORDERS_2:2;
verum
end;
hence
L is continuous
by Lm10; verum