let L be complete LATTICE; :: thesis: ( 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
; :: thesis: 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; :: thesis: ( 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
; :: thesis: S is continuous LATTICE
reconsider S' = S as complete LATTICE by A2, A3, Th29;
for J being non empty set
for K being V9() ManySortedSet of
for F being DoubleIndexedSet of K,S' 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,S' 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,S' st ( for j being Element of J holds rng (F . j) is directed ) holds
Inf = Sup let F be
DoubleIndexedSet of
K,
S';
:: thesis: ( ( 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
;
:: thesis: 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;
for
t being
Element of
S holds
d . t is_minimum_of g " {t}
by A3, A5, WAYBEL_1:23;
then A6:
g * d = id S
by WAYBEL_1:24;
A7:
d is
monotone
by A5, WAYBEL_1:9;
reconsider dF =
(J => d) ** F as
DoubleIndexedSet of
K,
L by Th31;
A8:
for
j being
Element of
J holds
rng (dF . j) is
directed
reconsider gdF =
(J => g) ** dF as
DoubleIndexedSet of
K,
S ;
A10:
F =
(id (J --> the carrier of S)) ** F
by MSUALG_3:4
.=
((J --> g) ** (J --> d)) ** F
by A6, Th30
.=
gdF
by PBOOLE:154
;
A11:
rng (Sups ) c= g .: (rng (Sups ))
A16:
g .: (rng (Sups )) c= rng (Sups )
A22:
ex_inf_of rng (Sups ),
L
by YELLOW_0:17;
A23:
g preserves_inf_of rng (Sups )
by A2, WAYBEL_0:def 32;
(
rng (Infs ) is
directed & not
rng (Infs ) is
empty )
by A8, Th27;
then A24:
g preserves_sup_of rng (Infs )
by A2, WAYBEL_0:def 37;
A25:
ex_sup_of rng (Infs ),
L
by YELLOW_0:17;
A26:
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 ;
:: thesis: ( f in dom (Frege dF) implies rng ((Frege F) . f) = g .: (rng ((Frege dF) . f)) )
assume A27:
f in dom (Frege dF)
;
:: thesis: rng ((Frege F) . f) = g .: (rng ((Frege dF) . f))
then reconsider f =
f as
Element of
product (doms dF) by PARTFUN1:def 4;
A28:
dom (Frege dF) =
product (doms dF)
by PARTFUN1:def 4
.=
product (doms F)
by Th32
.=
dom (Frege F)
by PARTFUN1:def 4
;
A29:
dom ((Frege dF) . f) =
dom dF
by A27, Th8
.=
J
by PARTFUN1:def 4
;
A30:
dom ((Frege F) . f) =
dom F
by A27, A28, Th8
.=
J
by PARTFUN1:def 4
;
dom g = the
carrier of
L
by FUNCT_2:def 1;
then
rng ((Frege dF) . f) c= dom g
;
then A31:
dom (g * ((Frege dF) . f)) = dom ((Frege dF) . f)
by RELAT_1:46;
now let i be
set ;
:: thesis: ( i in J implies (g * ((Frege dF) . f)) . i = ((Frege F) . f) . i )assume A32:
i in J
;
:: thesis: (g * ((Frege dF) . f)) . i = ((Frege F) . f) . ithen reconsider j =
i as
Element of
J ;
A33:
j in dom dF
by A32, PARTFUN1:def 4;
then
f . j in dom (dF . j)
by A27, Th9;
then
f . j in dom (((J => d) . j) * (F . j))
by MSUALG_3:2;
then A34:
f . j in dom (d * (F . j))
by FUNCOP_1:13;
A35:
j in dom F
by A32, PARTFUN1:def 4;
(g * ((Frege dF) . f)) . j =
g . (((Frege dF) . f) . j)
by A29, FUNCT_1:23
.=
g . ((dF . j) . (f . j))
by A27, A33, 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 A34, FUNCT_1:23
.=
((id the carrier of S) * (F . j)) . (f . j)
by A6, RELAT_1:55
.=
(F . j) . (f . j)
by FUNCT_2:23
.=
((Frege F) . f) . j
by A27, A28, A35, Th9
;
hence
(g * ((Frege dF) . f)) . i = ((Frege F) . f) . i
;
:: thesis: verum end;
then rng ((Frege F) . f) =
rng (g * ((Frege dF) . f))
by A29, A30, A31, FUNCT_1:9
.=
g .: (rng ((Frege dF) . f))
by RELAT_1:160
;
hence
rng ((Frege F) . f) = g .: (rng ((Frege dF) . f))
;
:: thesis: verum
end;
A36:
g .: (rng (Infs )) c= rng (Infs )
proof
let y be
set ;
:: according to TARSKI:def 3 :: thesis: ( not y in g .: (rng (Infs )) or y in rng (Infs ) )
assume
y in g .: (rng (Infs ))
;
:: thesis: y in rng (Infs )
then consider x being
set such that
x in the
carrier of
L
and A37:
x in rng (Infs )
and A38:
y = g . x
by FUNCT_2:115;
consider f being
set such that A39:
f in dom (Frege dF)
and A40:
x = //\ ((Frege dF) . f),
L
by A37, Th13;
reconsider f =
f as
Element of
product (doms dF) by A39, PARTFUN1:def 4;
reconsider f' =
f as
Element of
product (doms F) by Th32;
set X =
rng ((Frege dF) . f);
A41:
g preserves_inf_of rng ((Frege dF) . f)
by A2, WAYBEL_0:def 32;
ex_inf_of rng ((Frege dF) . f),
L
by YELLOW_0:17;
then
inf (g .: (rng ((Frege dF) . f))) = g . (inf (rng ((Frege dF) . f)))
by A41, WAYBEL_0:def 30;
then A42:
y = inf (g .: (rng ((Frege dF) . f)))
by A38, A40, YELLOW_2:def 6;
A43:
dom (Frege dF) =
product (doms dF)
by PARTFUN1:def 4
.=
product (doms F)
by Th32
.=
dom (Frege F)
by PARTFUN1:def 4
;
rng ((Frege F) . f) = g .: (rng ((Frege dF) . f))
by A26, A39;
then
y = Inf
by A42, YELLOW_2:def 6;
hence
y in rng (Infs )
by A39, A43, Th13;
:: thesis: verum
end;
A44:
rng (Infs ) c= g .: (rng (Infs ))
proof
let y be
set ;
:: according to TARSKI:def 3 :: thesis: ( not y in rng (Infs ) or y in g .: (rng (Infs )) )
assume
y in rng (Infs )
;
:: thesis: y in g .: (rng (Infs ))
then consider f being
set such that A45:
f in dom (Frege F)
and A46:
y = //\ ((Frege F) . f),
S
by Th13;
reconsider f =
f as
Element of
product (doms F) by A45, PARTFUN1:def 4;
reconsider f' =
f as
Element of
product (doms dF) by Th32;
A47:
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 A26, A45;
then A48:
y = "/\" (g .: (rng ((Frege dF) . f))),
S
by A46, YELLOW_2:def 6;
set X =
rng ((Frege dF) . f');
A49:
g preserves_inf_of rng ((Frege dF) . f')
by A2, WAYBEL_0:def 32;
ex_inf_of rng ((Frege dF) . f'),
L
by YELLOW_0:17;
then A50:
y =
g . (inf (rng ((Frege dF) . f')))
by A48, A49, WAYBEL_0:def 30
.=
g . (Inf )
by YELLOW_2:def 6
;
Inf in rng (Infs )
by A45, A47, Th13;
hence
y in g .: (rng (Infs ))
by A50, FUNCT_2:43;
:: thesis: verum
end;
Inf =
inf (rng (Sups ))
by A10, YELLOW_2:def 6
.=
inf (g .: (rng (Sups )))
by A11, A16, XBOOLE_0:def 10
.=
g . (inf (rng (Sups )))
by A22, A23, WAYBEL_0:def 30
.=
g . (Inf )
by YELLOW_2:def 6
.=
g . (Sup )
by A1, A8, Lm8
.=
g . (sup (rng (Infs )))
by YELLOW_2:def 5
.=
sup (g .: (rng (Infs )))
by A24, A25, WAYBEL_0:def 31
.=
sup (rng (Infs ))
by A36, A44, XBOOLE_0:def 10
.=
Sup
by YELLOW_2:def 5
;
hence
Inf = Sup
;
:: thesis: verum
end;
hence
S is continuous LATTICE
by Lm9; :: thesis: verum