let L be lower-bounded algebraic LATTICE; for c being closure Function of L,L st c is directed-sups-preserving holds
c .: ([#] (CompactSublatt L)) = [#] (CompactSublatt (Image c))
let c be closure Function of L,L; ( c is directed-sups-preserving implies c .: ([#] (CompactSublatt L)) = [#] (CompactSublatt (Image c)) )
assume A1:
c is directed-sups-preserving
; c .: ([#] (CompactSublatt L)) = [#] (CompactSublatt (Image c))
now for a9 being object st a9 in [#] (CompactSublatt (Image c)) holds
a9 in c .: ([#] (CompactSublatt L))
c is
idempotent
by WAYBEL_1:def 13;
then A2:
rng c = { x where x is Element of L : x = c . x }
by YELLOW_2:19;
c is
idempotent
by WAYBEL_1:def 13;
then reconsider Imc =
Image c as
complete LATTICE by A1, YELLOW_2:35;
let a9 be
object ;
( a9 in [#] (CompactSublatt (Image c)) implies a9 in c .: ([#] (CompactSublatt L)) )assume A3:
a9 in [#] (CompactSublatt (Image c))
;
a9 in c .: ([#] (CompactSublatt L))A4:
the
carrier of
(CompactSublatt Imc) c= the
carrier of
Imc
by YELLOW_0:def 13;
then reconsider a =
a9 as
Element of
Imc by A3;
a is
compact
by A3, Def1;
then A5:
a << a
by WAYBEL_3:def 2;
a9 in the
carrier of
Imc
by A3, A4;
then
a in rng c
by YELLOW_0:def 15;
then consider a1 being
Element of
L such that A6:
a = a1
and A7:
a1 = c . a1
by A2;
compactbelow a1 is non
empty directed Subset of
L
by Def4;
then A8:
(
c preserves_sup_of compactbelow a1 &
ex_sup_of compactbelow a1,
L )
by A1, WAYBEL_0:75, WAYBEL_0:def 37;
A9:
c is
monotone
by A1, YELLOW_2:16;
then A15:
c .: (compactbelow a1) c= (downarrow a1) /\ (c .: ([#] (CompactSublatt L)))
;
a = sup (compactbelow a1)
by A6, Def3;
then A16:
a = sup (c .: (compactbelow a1))
by A6, A7, A8, WAYBEL_0:def 31;
c .: (compactbelow a1) c= rng c
by RELAT_1:111;
then A17:
c .: (compactbelow a1) c= the
carrier of
Imc
by YELLOW_0:def 15;
A18:
(downarrow a) /\ (c .: ([#] (CompactSublatt L))) is non
empty directed Subset of
Imc
proof
(c .: ([#] (CompactSublatt L))) /\ (downarrow a) is
Subset of
Imc
;
then reconsider D =
(downarrow a) /\ (c .: ([#] (CompactSublatt L))) as
Subset of
Imc ;
A19:
Bottom Imc <= a
by YELLOW_0:44;
A20:
now for x, y being Element of Imc st x in D & y in D holds
ex z being Element of Imc st
( z in D & x <= z & y <= z )let x,
y be
Element of
Imc;
( x in D & y in D implies ex z being Element of Imc st
( z in D & x <= z & y <= z ) )assume that A21:
x in D
and A22:
y in D
;
ex z being Element of Imc st
( z in D & x <= z & y <= z )
x in c .: ([#] (CompactSublatt L))
by A21, XBOOLE_0:def 4;
then consider d being
object such that A23:
d in dom c
and A24:
d in [#] (CompactSublatt L)
and A25:
x = c . d
by FUNCT_1:def 6;
y in c .: ([#] (CompactSublatt L))
by A22, XBOOLE_0:def 4;
then consider e being
object such that A26:
e in dom c
and A27:
e in [#] (CompactSublatt L)
and A28:
y = c . e
by FUNCT_1:def 6;
reconsider e =
e as
Element of
L by A26;
y in downarrow a
by A22, XBOOLE_0:def 4;
then
y <= a
by WAYBEL_0:17;
then A29:
c . e <= a1
by A6, A28, YELLOW_0:59;
reconsider d =
d as
Element of
L by A23;
A30:
d <= d "\/" e
by YELLOW_0:22;
x in downarrow a
by A21, XBOOLE_0:def 4;
then
x <= a
by WAYBEL_0:17;
then
c . d <= a1
by A6, A25, YELLOW_0:59;
then A31:
(c . d) "\/" (c . e) <= a1
by A29, YELLOW_0:22;
d "\/" e in the
carrier of
L
;
then
d "\/" e in dom c
by FUNCT_2:def 1;
then
c . (d "\/" e) in rng c
by FUNCT_1:def 3;
then reconsider z =
c . (d "\/" e) as
Element of
Imc by YELLOW_0:def 15;
take z =
z;
( z in D & x <= z & y <= z )A32:
id L <= c
by WAYBEL_1:def 14;
then
(id L) . e <= c . e
by YELLOW_2:9;
then A33:
e <= c . e
by FUNCT_1:18;
(id L) . d <= c . d
by A32, YELLOW_2:9;
then
d <= c . d
by FUNCT_1:18;
then
d "\/" e <= (c . d) "\/" (c . e)
by A33, YELLOW_3:3;
then
d "\/" e <= a1
by A31, ORDERS_2:3;
then
c . (d "\/" e) <= a1
by A7, A9, WAYBEL_1:def 2;
then
z <= a
by A6, YELLOW_0:60;
then A34:
z in downarrow a
by WAYBEL_0:17;
A35:
e <= d "\/" e
by YELLOW_0:22;
then A36:
c . e <= c . (d "\/" e)
by A9, WAYBEL_1:def 2;
e is
compact
by A27, Def1;
then
e << e
by WAYBEL_3:def 2;
then A37:
e << d "\/" e
by A35, WAYBEL_3:2;
d is
compact
by A24, Def1;
then
d << d
by WAYBEL_3:def 2;
then
d << d "\/" e
by A30, WAYBEL_3:2;
then
d "\/" e << d "\/" e
by A37, WAYBEL_3:3;
then
d "\/" e is
compact
by WAYBEL_3:def 2;
then A38:
d "\/" e in [#] (CompactSublatt L)
by Def1;
d "\/" e in the
carrier of
L
;
then
d "\/" e in dom c
by FUNCT_2:def 1;
then
z in c .: ([#] (CompactSublatt L))
by A38, FUNCT_1:def 6;
hence
z in D
by A34, XBOOLE_0:def 4;
( x <= z & y <= z )
c . d <= c . (d "\/" e)
by A9, A30, WAYBEL_1:def 2;
hence
(
x <= z &
y <= z )
by A25, A28, A36, YELLOW_0:60;
verum end;
Bottom L is
compact
by WAYBEL_3:15;
then
(
dom c = the
carrier of
L &
Bottom L in [#] (CompactSublatt L) )
by Def1, FUNCT_2:def 1;
then A39:
c . (Bottom L) in c .: ([#] (CompactSublatt L))
by FUNCT_1:def 6;
A40:
(
ex_sup_of {} ,
L &
{} c= the
carrier of
L )
by YELLOW_0:42;
A41:
{} c= the
carrier of
Imc
;
c . (Bottom L) =
c . ("\/" ({},L))
by YELLOW_0:def 11
.=
"\/" (
{},
Imc)
by A40, A41, WAYBEL_1:55
.=
Bottom Imc
by YELLOW_0:def 11
;
then
c . (Bottom L) in downarrow a
by A19, WAYBEL_0:17;
hence
(downarrow a) /\ (c .: ([#] (CompactSublatt L))) is non
empty directed Subset of
Imc
by A39, A20, WAYBEL_0:def 1, XBOOLE_0:def 4;
verum
end; A42:
c .: ([#] (CompactSublatt L)) c= rng c
by RELAT_1:111;
then A45:
(downarrow a1) /\ (c .: ([#] (CompactSublatt L))) c= (downarrow a) /\ (c .: ([#] (CompactSublatt L)))
;
ex_sup_of c .: (compactbelow a1),
L
by A8, WAYBEL_0:def 31;
then A46:
a = "\/" (
(c .: (compactbelow a1)),
Imc)
by A6, A7, A17, A16, WAYBEL_1:55;
(
ex_sup_of c .: (compactbelow a1),
Imc &
ex_sup_of (downarrow a) /\ (c .: ([#] (CompactSublatt L))),
Imc )
by YELLOW_0:17;
then
a <= "\/" (
((downarrow a) /\ (c .: ([#] (CompactSublatt L)))),
Imc)
by A46, A15, A45, XBOOLE_1:1, YELLOW_0:34;
then consider k being
Element of
Imc such that A47:
k in (downarrow a) /\ (c .: ([#] (CompactSublatt L)))
and A48:
a <= k
by A5, A18, WAYBEL_3:def 1;
k in downarrow a
by A47, XBOOLE_0:def 4;
then A49:
k <= a
by WAYBEL_0:17;
k in c .: ([#] (CompactSublatt L))
by A47, XBOOLE_0:def 4;
hence
a9 in c .: ([#] (CompactSublatt L))
by A48, A49, ORDERS_2:2;
verum end;
then A50:
[#] (CompactSublatt (Image c)) c= c .: ([#] (CompactSublatt L))
;
c .: ([#] (CompactSublatt L)) c= [#] (CompactSublatt (Image c))
by A1, Th23;
hence
c .: ([#] (CompactSublatt L)) = [#] (CompactSublatt (Image c))
by A50, XBOOLE_0:def 10; verum