let L be lower-bounded algebraic LATTICE; :: thesis: 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; :: thesis: ( c is directed-sups-preserving implies c .: ([#] (CompactSublatt L)) = [#] (CompactSublatt (Image c)) )
assume A1:
c is directed-sups-preserving
; :: thesis: c .: ([#] (CompactSublatt L)) = [#] (CompactSublatt (Image c))
then A2:
c .: ([#] (CompactSublatt L)) c= [#] (CompactSublatt (Image c))
by Th25;
now let a' be
set ;
:: thesis: ( a' in [#] (CompactSublatt (Image c)) implies a' in c .: ([#] (CompactSublatt L)) )
c is
idempotent
by WAYBEL_1:def 13;
then reconsider Imc =
Image c as
complete LATTICE by A1, YELLOW_2:37;
assume A3:
a' in [#] (CompactSublatt (Image c))
;
:: thesis: a' in c .: ([#] (CompactSublatt L))then A4:
a' in the
carrier of
(CompactSublatt (Image c))
;
A5:
the
carrier of
(CompactSublatt Imc) c= the
carrier of
Imc
by YELLOW_0:def 13;
then A6:
a' in the
carrier of
Imc
by A4;
reconsider a =
a' as
Element of
Imc by A4, A5;
A7:
a in rng c
by A6, YELLOW_0:def 15;
c is
idempotent
by WAYBEL_1:def 13;
then
rng c = { x where x is Element of L : x = c . x }
by YELLOW_2:21;
then consider a1 being
Element of
L such that A8:
(
a = a1 &
a1 = c . a1 )
by A7;
a is
compact
by A3, Def1;
then A9:
a << a
by WAYBEL_3:def 2;
A10:
c is
monotone
by A1, YELLOW_2:18;
A11:
c .: ([#] (CompactSublatt L)) c= rng c
by RELAT_1:144;
A12:
(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 ;
A13:
dom c = the
carrier of
L
by FUNCT_2:def 1;
Bottom L is
compact
by WAYBEL_3:15;
then
Bottom L in the
carrier of
(CompactSublatt L)
by Def1;
then
Bottom L in [#] (CompactSublatt L)
;
then A14:
c . (Bottom L) in c .: ([#] (CompactSublatt L))
by A13, FUNCT_1:def 12;
A15:
Bottom Imc <= a
by YELLOW_0:44;
A16:
ex_sup_of {} ,
L
by YELLOW_0:42;
A17:
{} c= the
carrier of
L
by XBOOLE_1:2;
A18:
{} c= the
carrier of
Imc
by XBOOLE_1:2;
c . (Bottom L) =
c . ("\/" {} ,L)
by YELLOW_0:def 11
.=
"\/" {} ,
Imc
by A16, A17, A18, WAYBEL_1:58
.=
Bottom Imc
by YELLOW_0:def 11
;
then A19:
c . (Bottom L) in downarrow a
by A15, WAYBEL_0:17;
now let x,
y be
Element of
Imc;
:: thesis: ( x in D & y in D implies ex z being Element of Imc st
( z in D & x <= z & y <= z ) )assume
(
x in D &
y in D )
;
:: thesis: ex z being Element of Imc st
( z in D & x <= z & y <= z )then A20:
(
x in downarrow a &
x in c .: ([#] (CompactSublatt L)) &
y in downarrow a &
y in c .: ([#] (CompactSublatt L)) )
by XBOOLE_0:def 4;
then consider d being
set such that A21:
d in dom c
and A22:
d in [#] (CompactSublatt L)
and A23:
x = c . d
by FUNCT_1:def 12;
reconsider d =
d as
Element of
L by A21;
consider e being
set such that A24:
e in dom c
and A25:
e in [#] (CompactSublatt L)
and A26:
y = c . e
by A20, FUNCT_1:def 12;
reconsider e =
e as
Element of
L by A24;
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 5;
then reconsider z =
c . (d "\/" e) as
Element of
Imc by YELLOW_0:def 15;
take z =
z;
:: thesis: ( z in D & x <= z & y <= z )
id L <= c
by WAYBEL_1:def 14;
then
(
(id L) . d <= c . d &
(id L) . e <= c . e )
by YELLOW_2:10;
then
(
d <= c . d &
e <= c . e )
by TMAP_1:91;
then A27:
d "\/" e <= (c . d) "\/" (c . e)
by YELLOW_3:3;
(
x <= a &
y <= a )
by A20, WAYBEL_0:17;
then
(
c . d <= a1 &
c . e <= a1 )
by A8, A23, A26, YELLOW_0:60;
then
(c . d) "\/" (c . e) <= a1
by YELLOW_0:22;
then
d "\/" e <= a1
by A27, ORDERS_2:26;
then
c . (d "\/" e) <= a1
by A8, A10, WAYBEL_1:def 2;
then
z <= a
by A8, YELLOW_0:61;
then A28:
z in downarrow a
by WAYBEL_0:17;
d "\/" e in the
carrier of
L
;
then A29:
d "\/" e in dom c
by FUNCT_2:def 1;
A30:
(
d <= d "\/" e &
e <= d "\/" e )
by YELLOW_0:22;
(
d is
compact &
e is
compact )
by A22, A25, Def1;
then
(
d << d &
e << e )
by WAYBEL_3:def 2;
then
(
d << d "\/" e &
e << d "\/" e )
by A30, WAYBEL_3:2;
then
d "\/" e << d "\/" e
by WAYBEL_3:3;
then
d "\/" e is
compact
by WAYBEL_3:def 2;
then
d "\/" e in the
carrier of
(CompactSublatt L)
by Def1;
then
d "\/" e in [#] (CompactSublatt L)
;
then
z in c .: ([#] (CompactSublatt L))
by A29, FUNCT_1:def 12;
hence
z in D
by A28, XBOOLE_0:def 4;
:: thesis: ( x <= z & y <= z )
(
c . d <= c . (d "\/" e) &
c . e <= c . (d "\/" e) )
by A10, A30, WAYBEL_1:def 2;
hence
(
x <= z &
y <= z )
by A23, A26, YELLOW_0:61;
:: thesis: verum end;
hence
(downarrow a) /\ (c .: ([#] (CompactSublatt L))) is non
empty directed Subset of
Imc
by A14, A19, WAYBEL_0:def 1, XBOOLE_0:def 4;
:: thesis: verum
end; A31:
compactbelow a1 is non
empty directed Subset of
L
by Def4;
then A32:
c preserves_sup_of compactbelow a1
by A1, WAYBEL_0:def 37;
A33:
ex_sup_of compactbelow a1,
L
by A31, WAYBEL_0:75;
then A34:
ex_sup_of c .: (compactbelow a1),
L
by A32, WAYBEL_0:def 31;
c .: (compactbelow a1) c= rng c
by RELAT_1:144;
then A35:
c .: (compactbelow a1) c= the
carrier of
Imc
by YELLOW_0:def 15;
a = sup (compactbelow a1)
by A8, Def3;
then
a = sup (c .: (compactbelow a1))
by A8, A32, A33, WAYBEL_0:def 31;
then A36:
a = "\/" (c .: (compactbelow a1)),
Imc
by A8, A34, A35, WAYBEL_1:58;
A37:
ex_sup_of c .: (compactbelow a1),
Imc
by YELLOW_0:17;
A38:
ex_sup_of (downarrow a) /\ (c .: ([#] (CompactSublatt L))),
Imc
by YELLOW_0:17;
then A45:
c .: (compactbelow a1) c= (downarrow a1) /\ (c .: ([#] (CompactSublatt L)))
by TARSKI:def 3;
then
(downarrow a1) /\ (c .: ([#] (CompactSublatt L))) c= (downarrow a) /\ (c .: ([#] (CompactSublatt L)))
by TARSKI:def 3;
then
a <= "\/" ((downarrow a) /\ (c .: ([#] (CompactSublatt L)))),
Imc
by A36, A37, A38, A45, XBOOLE_1:1, YELLOW_0:34;
then consider k being
Element of
Imc such that A48:
(
k in (downarrow a) /\ (c .: ([#] (CompactSublatt L))) &
a <= k )
by A9, A12, WAYBEL_3:def 1;
A49:
(
k in downarrow a &
k in c .: ([#] (CompactSublatt L)) )
by A48, XBOOLE_0:def 4;
then
k <= a
by WAYBEL_0:17;
hence
a' in c .: ([#] (CompactSublatt L))
by A48, A49, ORDERS_2:25;
:: thesis: verum end;
then
[#] (CompactSublatt (Image c)) c= c .: ([#] (CompactSublatt L))
by TARSKI:def 3;
hence
c .: ([#] (CompactSublatt L)) = [#] (CompactSublatt (Image c))
by A2, XBOOLE_0:def 10; :: thesis: verum