let L be complete LATTICE; ( L is continuous implies for S being non empty Poset st ex g being Function of L,S st
( g is infs-preserving & g is directed-sups-preserving & g is onto ) holds
S is continuous LATTICE )
assume A1:
L is continuous
; for S being non empty Poset st ex g being Function of L,S st
( g is infs-preserving & g is directed-sups-preserving & g is onto ) holds
S is continuous LATTICE
let S be non empty Poset; ( ex g being Function of L,S st
( g is infs-preserving & g is directed-sups-preserving & g is onto ) implies S is continuous LATTICE )
given g being Function of L,S such that A2:
( g is infs-preserving & g is directed-sups-preserving )
and
A3:
g is onto
; S is continuous LATTICE
reconsider S9 = S as complete LATTICE by A2, A3, Th29;
for J being non empty set
for K being V9() ManySortedSet of J
for F being DoubleIndexedSet of K,S9 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 V9() ManySortedSet of J
for F being DoubleIndexedSet of K,S9 st ( for j being Element of J holds rng (F . j) is directed ) holds
Inf = Sup let K be
V9()
ManySortedSet of
J;
for F being DoubleIndexedSet of K,S9 st ( for j being Element of J holds rng (F . j) is directed ) holds
Inf = Sup let F be
DoubleIndexedSet of
K,
S9;
( ( for j being Element of J holds rng (F . j) is directed ) implies Inf = Sup )
assume A4:
for
j being
Element of
J holds
rng (F . j) is
directed
;
Inf = Sup
consider d being
Function of
S,
L such that A5:
[g,d] is
Galois
and
for
t being
Element of
S holds
d . t is_minimum_of g " (uparrow t)
by A2, WAYBEL_1:15;
reconsider dF =
(J => d) ** F as
DoubleIndexedSet of
K,
L by Th31;
A6:
(
ex_inf_of rng (Sups ),
L &
g preserves_inf_of rng (Sups ) )
by A2, WAYBEL_0:def 32, YELLOW_0:17;
for
t being
Element of
S holds
d . t is_minimum_of g " {t}
by A3, A5, WAYBEL_1:23;
then A7:
g * d = id S
by WAYBEL_1:24;
A8:
for
f being
set st
f in dom (Frege dF) holds
rng ((Frege F) . f) = g .: (rng ((Frege dF) . f))
proof
let f be
set ;
( f in dom (Frege dF) implies rng ((Frege F) . f) = g .: (rng ((Frege dF) . f)) )
assume A9:
f in dom (Frege dF)
;
rng ((Frege F) . f) = g .: (rng ((Frege dF) . f))
then reconsider f =
f as
Element of
product (doms dF) by PARTFUN1:def 4;
A10:
dom (Frege dF) =
product (doms dF)
by PARTFUN1:def 4
.=
product (doms F)
by Th32
.=
dom (Frege F)
by PARTFUN1:def 4
;
A11:
dom ((Frege dF) . f) =
dom dF
by A9, Th8
.=
J
by PARTFUN1:def 4
;
A12:
now let i be
set ;
( i in J implies (g * ((Frege dF) . f)) . i = ((Frege F) . f) . i )assume A13:
i in J
;
(g * ((Frege dF) . f)) . i = ((Frege F) . f) . ithen reconsider j =
i as
Element of
J ;
A14:
j in dom F
by A13, PARTFUN1:def 4;
A15:
j in dom dF
by A13, PARTFUN1:def 4;
then
f . j in dom (dF . j)
by A9, Th9;
then
f . j in dom (((J => d) . j) * (F . j))
by MSUALG_3:2;
then A16:
f . j in dom (d * (F . j))
by FUNCOP_1:13;
(g * ((Frege dF) . f)) . j =
g . (((Frege dF) . f) . j)
by A11, FUNCT_1:23
.=
g . ((dF . j) . (f . j))
by A9, A15, Th9
.=
g . ((((J => d) . j) * (F . j)) . (f . j))
by MSUALG_3:2
.=
g . ((d * (F . j)) . (f . j))
by FUNCOP_1:13
.=
(g * (d * (F . j))) . (f . j)
by A16, FUNCT_1:23
.=
((id the carrier of S) * (F . j)) . (f . j)
by A7, RELAT_1:55
.=
(F . j) . (f . j)
by FUNCT_2:23
.=
((Frege F) . f) . j
by A9, A10, A14, Th9
;
hence
(g * ((Frege dF) . f)) . i = ((Frege F) . f) . i
;
verum end;
dom g = the
carrier of
L
by FUNCT_2:def 1;
then
rng ((Frege dF) . f) c= dom g
;
then A17:
dom (g * ((Frege dF) . f)) = dom ((Frege dF) . f)
by RELAT_1:46;
dom ((Frege F) . f) =
dom F
by A9, A10, Th8
.=
J
by PARTFUN1:def 4
;
then rng ((Frege F) . f) =
rng (g * ((Frege dF) . f))
by A11, A17, A12, FUNCT_1:9
.=
g .: (rng ((Frege dF) . f))
by RELAT_1:160
;
hence
rng ((Frege F) . f) = g .: (rng ((Frege dF) . f))
;
verum
end;
A18:
rng (Infs ) c= g .: (rng (Infs ))
proof
let y be
set ;
TARSKI:def 3 ( not y in rng (Infs ) or y in g .: (rng (Infs )) )
assume
y in rng (Infs )
;
y in g .: (rng (Infs ))
then consider f being
set such that A19:
f in dom (Frege F)
and A20:
y = //\ ((Frege F) . f),
S
by Th13;
reconsider f =
f as
Element of
product (doms F) by A19, PARTFUN1:def 4;
reconsider f9 =
f as
Element of
product (doms dF) by Th32;
set X =
rng ((Frege dF) . f9);
A21:
(
g preserves_inf_of rng ((Frege dF) . f9) &
ex_inf_of rng ((Frege dF) . f9),
L )
by A2, WAYBEL_0:def 32, YELLOW_0:17;
A22:
dom (Frege dF) =
product (doms dF)
by PARTFUN1:def 4
.=
product (doms F)
by Th32
.=
dom (Frege F)
by PARTFUN1:def 4
;
then
rng ((Frege F) . f) = g .: (rng ((Frege dF) . f))
by A8, A19;
then
y = "/\" (g .: (rng ((Frege dF) . f))),
S
by A20, YELLOW_2:def 6;
then A23:
y =
g . (inf (rng ((Frege dF) . f9)))
by A21, WAYBEL_0:def 30
.=
g . (Inf )
by YELLOW_2:def 6
;
Inf in rng (Infs )
by A19, A22, Th13;
hence
y in g .: (rng (Infs ))
by A23, FUNCT_2:43;
verum
end;
A24:
g .: (rng (Infs )) c= rng (Infs )
proof
let y be
set ;
TARSKI:def 3 ( not y in g .: (rng (Infs )) or y in rng (Infs ) )
assume
y in g .: (rng (Infs ))
;
y in rng (Infs )
then consider x being
set such that
x in the
carrier of
L
and A25:
x in rng (Infs )
and A26:
y = g . x
by FUNCT_2:115;
consider f being
set such that A27:
f in dom (Frege dF)
and A28:
x = //\ ((Frege dF) . f),
L
by A25, Th13;
reconsider f =
f as
Element of
product (doms dF) by A27, PARTFUN1:def 4;
set X =
rng ((Frege dF) . f);
(
g preserves_inf_of rng ((Frege dF) . f) &
ex_inf_of rng ((Frege dF) . f),
L )
by A2, WAYBEL_0:def 32, YELLOW_0:17;
then
inf (g .: (rng ((Frege dF) . f))) = g . (inf (rng ((Frege dF) . f)))
by WAYBEL_0:def 30;
then A29:
y = inf (g .: (rng ((Frege dF) . f)))
by A26, A28, YELLOW_2:def 6;
A30:
dom (Frege dF) =
product (doms dF)
by PARTFUN1:def 4
.=
product (doms F)
by Th32
.=
dom (Frege F)
by PARTFUN1:def 4
;
reconsider f9 =
f as
Element of
product (doms F) by Th32;
rng ((Frege F) . f) = g .: (rng ((Frege dF) . f))
by A8, A27;
then
y = Inf
by A29, YELLOW_2:def 6;
hence
y in rng (Infs )
by A27, A30, Th13;
verum
end;
A31:
d is
monotone
by A5, WAYBEL_1:9;
A32:
for
j being
Element of
J holds
rng (dF . j) is
directed
then
(
rng (Infs ) is
directed & not
rng (Infs ) is
empty )
by Th27;
then A34:
g preserves_sup_of rng (Infs )
by A2, WAYBEL_0:def 37;
reconsider gdF =
(J => g) ** dF as
DoubleIndexedSet of
K,
S ;
A35:
ex_sup_of rng (Infs ),
L
by YELLOW_0:17;
A36:
rng (Sups ) c= g .: (rng (Sups ))
A41:
g .: (rng (Sups )) c= rng (Sups )
F =
(id (J --> the carrier of S)) ** F
by MSUALG_3:4
.=
((J --> g) ** (J --> d)) ** F
by A7, Th30
.=
gdF
by PBOOLE:154
;
then Inf =
inf (rng (Sups ))
by YELLOW_2:def 6
.=
inf (g .: (rng (Sups )))
by A36, A41, XBOOLE_0:def 10
.=
g . (inf (rng (Sups )))
by A6, WAYBEL_0:def 30
.=
g . (Inf )
by YELLOW_2:def 6
.=
g . (Sup )
by A1, A32, Lm8
.=
g . (sup (rng (Infs )))
by YELLOW_2:def 5
.=
sup (g .: (rng (Infs )))
by A34, A35, WAYBEL_0:def 31
.=
sup (rng (Infs ))
by A24, A18, XBOOLE_0:def 10
.=
Sup
by YELLOW_2:def 5
;
hence
Inf = Sup
;
verum
end;
hence
S is continuous LATTICE
by Lm9; verum