let L be complete LATTICE; ( ( 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 ) implies L is continuous )
assume A1:
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
; L is continuous
for J being non empty set
for K being non-empty ManySortedSet of J
for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds
Inf = Sup
proof
let J be non
empty set ;
for K being non-empty ManySortedSet of J
for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds
Inf = Sup let K be
non-empty ManySortedSet of
J;
for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds
Inf = Sup let F be
DoubleIndexedSet of
K,
L;
( ( for j being Element of J holds rng (F . j) is directed ) implies Inf = Sup )
set j = the
Element of
J;
set k = the
Element of
K . the
Element of
J;
defpred S1[
set ,
set ,
set ]
means ( $1
in J & ( ( $2
in K . $1 & $3
= (F . $1) . $2 ) or ( not $2
in K . $1 & $3
= Bottom L ) ) );
A2:
dom (doms F) = dom F
by FUNCT_6:59;
the
Element of
J in J
;
then
the
Element of
J in dom K
by PARTFUN1:def 2;
then
( the
Element of
K . the
Element of
J in K . the
Element of
J &
K . the
Element of
J in rng K )
by FUNCT_1:def 3;
then reconsider K9 =
union (rng K) as non
empty set by TARSKI:def 4;
A3:
dom F = J
by PARTFUN1:def 2;
A4:
for
j being
Element of
J for
k9 being
Element of
K9 ex
z being
Element of
L st
S1[
j,
k9,
z]
proof
let j be
Element of
J;
for k9 being Element of K9 ex z being Element of L st S1[j,k9,z]let k9 be
Element of
K9;
ex z being Element of L st S1[j,k9,z]
per cases
( k9 in K . j or not k9 in K . j )
;
suppose
k9 in K . j
;
ex z being Element of L st S1[j,k9,z]then reconsider k =
k9 as
Element of
K . j ;
take
(F . j) . k
;
S1[j,k9,(F . j) . k]thus
S1[
j,
k9,
(F . j) . k]
;
verum end;
end;
ex
G being
Function of
[:J,K9:], the
carrier of
L st
for
j being
Element of
J for
k being
Element of
K9 holds
S1[
j,
k,
G . (
j,
k)]
from BINOP_1:sch 3(A4);
then consider G being
Function of
[:J,K9:], the
carrier of
L such that A6:
for
j being
Element of
J for
k being
Element of
K9 holds
S1[
j,
k,
G . (
j,
k)]
;
A7:
for
j being
Element of
J holds
K . j c= K9
A9:
for
j being
Element of
J holds
rng (F . j) c= rng ((curry G) . j)
A15:
for
j being
object st
j in dom F holds
\\/ (
(F . j),
L)
= \\/ (
((curry G) . j),
L)
proof
let j9 be
object ;
( j9 in dom F implies \\/ ((F . j9),L) = \\/ (((curry G) . j9),L) )
assume
j9 in dom F
;
\\/ ((F . j9),L) = \\/ (((curry G) . j9),L)
then reconsider j =
j9 as
Element of
J ;
reconsider H =
(curry G) . j as
Function of
((J --> K9) . j), the
carrier of
L ;
reconsider H =
H as
Function of
K9, the
carrier of
L ;
for
k being
Element of
K9 holds
H . k <= Sup
then A18:
Sup <= Sup
by YELLOW_2:54;
(
ex_sup_of rng (F . j),
L &
ex_sup_of rng ((curry G) . j),
L )
by YELLOW_0:17;
then
sup (rng (F . j)) <= sup (rng ((curry G) . j))
by A9, YELLOW_0:34;
then
Sup <= sup (rng H)
by YELLOW_2:def 5;
then
Sup <= Sup
by YELLOW_2:def 5;
hence
\\/ (
(F . j9),
L)
= \\/ (
((curry G) . j9),
L)
by A18, ORDERS_2:2;
verum
end;
A19:
dom (doms (curry G)) = dom (curry G)
by FUNCT_6:59;
A20:
dom (curry G) = J
by Th20;
product (doms F) c= product (doms (curry G))
then
dom (Frege F) c= product (doms (curry G))
;
then A29:
dom (Frege F) c= dom (Frege (curry G))
by PARTFUN1:def 2;
A30:
for
f being
object st
f in dom (Frege F) holds
//\ (
((Frege F) . f),
L)
= //\ (
((Frege (curry G)) . f),
L)
proof
let f9 be
object ;
( f9 in dom (Frege F) implies //\ (((Frege F) . f9),L) = //\ (((Frege (curry G)) . f9),L) )
assume A31:
f9 in dom (Frege F)
;
//\ (((Frege F) . f9),L) = //\ (((Frege (curry G)) . f9),L)
then reconsider f =
f9 as
Element of
product (doms F) ;
A32:
dom ((Frege F) . f) =
dom F
by A31, Th8
.=
J
by PARTFUN1:def 2
;
A33:
for
j being
object st
j in J holds
((Frege F) . f) . j = ((Frege (curry G)) . f) . j
dom ((Frege (curry G)) . f) =
dom (curry G)
by A29, A31, Th8
.=
proj1 (dom G)
by FUNCT_5:def 1
.=
proj1 [:J,K9:]
by FUNCT_2:def 1
.=
J
by FUNCT_5:9
;
hence
//\ (
((Frege F) . f9),
L)
= //\ (
((Frege (curry G)) . f9),
L)
by A32, A33, FUNCT_1:2;
verum
end;
A35:
Sup = Sup
proof
per cases
( for j being Element of J holds K . j = K9 or ex j being Element of J st K . j <> K9 )
;
suppose
ex
j being
Element of
J st
K . j <> K9
;
Sup = Sup then consider j being
Element of
J such that A38:
K . j <> K9
;
K . j c= K9
by A7;
then
not
K9 c= K . j
by A38, XBOOLE_0:def 10;
then consider k being
object such that A39:
k in K9
and A40:
not
k in K . j
;
reconsider k =
k as
Element of
K9 by A39;
A41:
(rng (Infs )) \/ {(Bottom L)} c= rng (Infs )
proof
let x be
object ;
TARSKI:def 3 ( not x in (rng (Infs )) \/ {(Bottom L)} or x in rng (Infs ) )
assume A42:
x in (rng (Infs )) \/ {(Bottom L)}
;
x in rng (Infs )
per cases
( x in rng (Infs ) or x in {(Bottom L)} )
by A42, XBOOLE_0:def 3;
suppose A45:
x in {(Bottom L)}
;
x in rng (Infs )then reconsider x9 =
x as
Element of
L ;
set f =
J --> k;
A46:
for
x being
object st
x in dom (doms (curry G)) holds
(J --> k) . x in (doms (curry G)) . x
dom (J --> k) =
J
.=
dom (doms (curry G))
by A19, Th20
;
then
J --> k in product (doms (curry G))
by A46, CARD_3:9;
then A48:
J --> k in dom (Frege (curry G))
by PARTFUN1:def 2;
A49:
x = Bottom L
by A45, TARSKI:def 1;
then x =
G . (
j,
k)
by A6, A40
.=
((curry G) . j) . k
by Th20
.=
((curry G) . j) . ((J --> k) . j)
;
then
x in rng ((Frege (curry G)) . (J --> k))
by A48, Lm5;
then
x9 >= "/\" (
(rng ((Frege (curry G)) . (J --> k))),
L)
by YELLOW_2:22;
then A50:
x9 >= //\ (
((Frege (curry G)) . (J --> k)),
L)
by YELLOW_2:def 6;
x9 <= //\ (
((Frege (curry G)) . (J --> k)),
L)
by A49, YELLOW_0:44;
then
x9 = //\ (
((Frege (curry G)) . (J --> k)),
L)
by A50, ORDERS_2:2;
hence
x in rng (Infs )
by A48, Th13;
verum end;
end; A51:
(
ex_sup_of rng (Infs ),
L &
ex_sup_of {(Bottom L)},
L )
by YELLOW_0:17;
A52:
rng (Infs ) c= (rng (Infs )) \/ {(Bottom L)}
A60:
Bottom L <= Sup
by YELLOW_0:44;
Sup =
sup (rng (Infs ))
by YELLOW_2:def 5
.=
sup ((rng (Infs )) \/ {(Bottom L)})
by A52, A41, XBOOLE_0:def 10
.=
(sup (rng (Infs ))) "\/" (sup {(Bottom L)})
by A51, YELLOW_2:3
.=
(sup (rng (Infs ))) "\/" (Bottom L)
by YELLOW_0:39
.=
(Sup ) "\/" (Bottom L)
by YELLOW_2:def 5
.=
Sup
by A60, YELLOW_0:24
;
hence
Sup = Sup
;
verum end;
end;
assume A61:
for
j being
Element of
J holds
rng (F . j) is
directed
;
Inf = Sup
A62:
for
j being
Element of
J holds
rng ((curry G) . j) is
directed
dom F =
J
by PARTFUN1:def 2
.=
dom (curry G)
by PARTFUN1:def 2
;
hence Inf =
Inf
by A15, Th11
.=
Sup
by A1, A62, A35
;
verum
end;
hence
L is continuous
by Lm9; verum