let L be complete LATTICE; :: thesis: ( ( 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
; :: thesis: L is continuous
for J being non empty set
for K being V9() ManySortedSet of
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 ;
:: thesis: for K being V9() ManySortedSet of
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
V9()
ManySortedSet of ;
:: thesis: 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;
:: thesis: ( ( for j being Element of J holds rng (F . j) is directed ) implies Inf = Sup )
assume A2:
for
j being
Element of
J holds
rng (F . j) is
directed
;
:: thesis: Inf = Sup
consider j being
Element of
J;
consider k being
Element of
K . j;
j in J
;
then
j in dom K
by PARTFUN1:def 4;
then
(
k in K . j &
K . j in rng K )
by FUNCT_1:def 5;
then reconsider K' =
union (rng K) as non
empty set by TARSKI:def 4;
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 ) ) );
A3:
for
j being
Element of
J for
k' being
Element of
K' ex
z being
Element of
L st
S1[
j,
k',
z]
ex
G being
Function of
[:J,K':],the
carrier of
L st
for
j being
Element of
J for
k being
Element of
K' holds
S1[
j,
k,
G . j,
k]
from BINOP_1:sch 3(A3);
then consider G being
Function of
[:J,K':],the
carrier of
L such that A5:
for
j being
Element of
J for
k being
Element of
K' holds
S1[
j,
k,
G . j,
k]
;
A6:
for
j being
Element of
J holds
K . j c= K'
A8:
for
j being
Element of
J holds
rng (F . j) c= rng ((curry G) . j)
A13:
for
j being
Element of
J holds
rng ((curry G) . j) is
directed
A28:
dom (doms F) = dom F
by FUNCT_6:89;
A29:
dom F = J
by PARTFUN1:def 4;
A30:
dom (doms (curry G)) = dom (curry G)
by FUNCT_6:89;
A31:
dom (curry G) = J
by Th20;
product (doms F) c= product (doms (curry G))
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in product (doms F) or x in product (doms (curry G)) )
assume
x in product (doms F)
;
:: thesis: x in product (doms (curry G))
then consider g being
Function such that A32:
x = g
and A33:
dom g = dom (doms F)
and A34:
for
j being
set st
j in dom (doms F) holds
g . j in (doms F) . j
by CARD_3:def 5;
A35:
dom g = dom (doms (curry G))
by A28, A29, A30, A33, Th20;
for
j being
set st
j in dom (doms (curry G)) holds
g . j in (doms (curry G)) . j
proof
let j be
set ;
:: thesis: ( j in dom (doms (curry G)) implies g . j in (doms (curry G)) . j )
assume A36:
j in dom (doms (curry G))
;
:: thesis: g . j in (doms (curry G)) . j
then A37:
j in J
by A30, Th20;
reconsider j' =
j as
Element of
J by A30, A36, Th20;
A38:
g . j in (doms F) . j
by A28, A29, A34, A37;
A39:
(doms F) . j =
dom (F . j')
by A29, FUNCT_6:31
.=
K . j'
by FUNCT_2:def 1
;
A40:
K . j' c= K'
by A6;
(doms (curry G)) . j =
dom ((curry G) . j')
by A31, FUNCT_6:31
.=
K'
by Th20
;
hence
g . j in (doms (curry G)) . j
by A38, A39, A40;
:: thesis: verum
end;
hence
x in product (doms (curry G))
by A32, A35, CARD_3:def 5;
:: thesis: verum
end;
then
dom (Frege F) c= product (doms (curry G))
by PARTFUN1:def 4;
then A41:
dom (Frege F) c= dom (Frege (curry G))
by PARTFUN1:def 4;
A42:
for
f being
set st
f in dom (Frege F) holds
//\ ((Frege F) . f),
L = //\ ((Frege (curry G)) . f),
L
proof
let f' be
set ;
:: thesis: ( f' in dom (Frege F) implies //\ ((Frege F) . f'),L = //\ ((Frege (curry G)) . f'),L )
assume A43:
f' in dom (Frege F)
;
:: thesis: //\ ((Frege F) . f'),L = //\ ((Frege (curry G)) . f'),L
then reconsider f =
f' as
Element of
product (doms F) by PARTFUN1:def 4;
A44:
dom ((Frege F) . f) =
dom F
by A43, Th8
.=
J
by PARTFUN1:def 4
;
A45:
dom ((Frege (curry G)) . f) =
dom (curry G)
by A41, A43, Th8
.=
proj1 (dom G)
by FUNCT_5:def 3
.=
proj1 [:J,K':]
by FUNCT_2:def 1
.=
J
by FUNCT_5:11
;
for
j being
set st
j in J holds
((Frege F) . f) . j = ((Frege (curry G)) . f) . j
hence
//\ ((Frege F) . f'),
L = //\ ((Frege (curry G)) . f'),
L
by A44, A45, FUNCT_1:9;
:: thesis: verum
end;
A47:
Sup = Sup
proof
per cases
( for j being Element of J holds K . j = K' or ex j being Element of J st K . j <> K' )
;
suppose
ex
j being
Element of
J st
K . j <> K'
;
:: thesis: Sup = Sup then consider j being
Element of
J such that A50:
K . j <> K'
;
K . j c= K'
by A6;
then
not
K' c= K . j
by A50, XBOOLE_0:def 10;
then consider k being
set such that A51:
(
k in K' & not
k in K . j )
by TARSKI:def 3;
reconsider k =
k as
Element of
K' by A51;
A52:
rng (Infs ) c= (rng (Infs )) \/ {(Bottom L)}
A60:
(rng (Infs )) \/ {(Bottom L)} c= rng (Infs )
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in (rng (Infs )) \/ {(Bottom L)} or x in rng (Infs ) )
assume A61:
x in (rng (Infs )) \/ {(Bottom L)}
;
:: thesis: x in rng (Infs )
per cases
( x in rng (Infs ) or x in {(Bottom L)} )
by A61, XBOOLE_0:def 3;
suppose A64:
x in {(Bottom L)}
;
:: thesis: x in rng (Infs )then A65:
x = Bottom L
by TARSKI:def 1;
reconsider x' =
x as
Element of
L by A64;
set f =
J --> k;
A66:
dom (J --> k) =
J
by FUNCOP_1:19
.=
dom (doms (curry G))
by A30, Th20
;
for
x being
set st
x in dom (doms (curry G)) holds
(J --> k) . x in (doms (curry G)) . x
then
J --> k in product (doms (curry G))
by A66, CARD_3:18;
then A68:
J --> k in dom (Frege (curry G))
by PARTFUN1:def 4;
x =
G . j,
k
by A5, A51, A65
.=
((curry G) . j) . k
by Th20
.=
((curry G) . j) . ((J --> k) . j)
by FUNCOP_1:13
;
then
x in rng ((Frege (curry G)) . (J --> k))
by A68, Lm5;
then
x' >= "/\" (rng ((Frege (curry G)) . (J --> k))),
L
by YELLOW_2:24;
then A69:
x' >= //\ ((Frege (curry G)) . (J --> k)),
L
by YELLOW_2:def 6;
x' <= //\ ((Frege (curry G)) . (J --> k)),
L
by A65, YELLOW_0:44;
then
x' = //\ ((Frege (curry G)) . (J --> k)),
L
by A69, ORDERS_2:25;
hence
x in rng (Infs )
by A68, Th13;
:: thesis: verum end;
end; A70:
(
ex_sup_of rng (Infs ),
L &
ex_sup_of {(Bottom L)},
L )
by YELLOW_0:17;
A71:
Bottom L <= Sup
by YELLOW_0:44;
Sup =
sup (rng (Infs ))
by YELLOW_2:def 5
.=
sup ((rng (Infs )) \/ {(Bottom L)})
by A52, A60, XBOOLE_0:def 10
.=
(sup (rng (Infs ))) "\/" (sup {(Bottom L)})
by A70, YELLOW_2:3
.=
(sup (rng (Infs ))) "\/" (Bottom L)
by YELLOW_0:39
.=
(Sup ) "\/" (Bottom L)
by YELLOW_2:def 5
.=
Sup
by A71, YELLOW_0:24
;
hence
Sup = Sup
;
:: thesis: verum end;
end;
A72:
dom F =
J
by PARTFUN1:def 4
.=
dom (curry G)
by PARTFUN1:def 4
;
for
j being
set st
j in dom F holds
\\/ (F . j),
L = \\/ ((curry G) . j),
L
proof
let j' be
set ;
:: thesis: ( j' in dom F implies \\/ (F . j'),L = \\/ ((curry G) . j'),L )
assume
j' in dom F
;
:: thesis: \\/ (F . j'),L = \\/ ((curry G) . j'),L
then reconsider j =
j' as
Element of
J by PARTFUN1:def 4;
reconsider H =
(curry G) . j as
Function of
((J --> K') . j),the
carrier of
L ;
(J --> K') . j = K'
by FUNCOP_1:13;
then reconsider H =
H as
Function of
K',the
carrier of
L ;
(
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 A8, YELLOW_0:34;
then
Sup <= sup (rng H)
by YELLOW_2:def 5;
then A73:
Sup <= Sup
by YELLOW_2:def 5;
for
k being
Element of
K' holds
H . k <= Sup
then
Sup <= Sup
by YELLOW_2:56;
hence
\\/ (F . j'),
L = \\/ ((curry G) . j'),
L
by A73, ORDERS_2:25;
:: thesis: verum
end;
hence Inf =
Inf
by A72, Th11
.=
Sup
by A1, A13, A47
;
:: thesis: verum
end;
hence
L is continuous
by Lm9; :: thesis: verum