let L be algebraic LATTICE; :: thesis: for c being closure Function of L,L st c is directed-sups-preserving holds
c .: ([#] (CompactSublatt L)) c= [#] (CompactSublatt (Image c))
let c be closure Function of L,L; :: thesis: ( c is directed-sups-preserving implies c .: ([#] (CompactSublatt L)) c= [#] (CompactSublatt (Image c)) )
assume A1:
c is directed-sups-preserving
; :: thesis: c .: ([#] (CompactSublatt L)) c= [#] (CompactSublatt (Image c))
A2:
( c is idempotent & c is monotone )
by WAYBEL_1:def 13;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in c .: ([#] (CompactSublatt L)) or x in [#] (CompactSublatt (Image c)) )
assume
x in c .: ([#] (CompactSublatt L))
; :: thesis: x in [#] (CompactSublatt (Image c))
then consider y being set such that
A3:
y in dom c
and
A4:
y in [#] (CompactSublatt L)
and
A5:
x = c . y
by FUNCT_1:def 12;
reconsider y' = y as Element of L by A3;
A6:
x in rng c
by A3, A5, FUNCT_1:def 5;
then reconsider x' = x as Element of (Image c) by YELLOW_0:def 15;
reconsider x1 = x' as Element of L by A6;
y' is compact
by A4, Def1;
then A7:
y' << y'
by WAYBEL_3:def 2;
now let D be non
empty directed Subset of
(Image c);
:: thesis: ( x' <= sup D implies ex d being Element of (Image c) st
( d in D & x' <= d ) )
D c= the
carrier of
(Image c)
;
then A8:
D c= rng c
by YELLOW_0:def 15;
then reconsider D' =
D as non
empty Subset of
L by XBOOLE_1:1;
reconsider D' =
D' as non
empty directed Subset of
L by YELLOW_2:7;
assume A9:
x' <= sup D
;
:: thesis: ex d being Element of (Image c) st
( d in D & x' <= d )
id L <= c
by WAYBEL_1:def 14;
then
(id L) . y' <= c . y'
by YELLOW_2:10;
then A10:
y' <= x1
by A5, TMAP_1:91;
A11:
ex_sup_of D',
L
by WAYBEL_0:75;
c preserves_sup_of D'
by A1, WAYBEL_0:def 37;
then A12:
c . (sup D') =
sup (c .: D')
by A11, WAYBEL_0:def 31
.=
sup D'
by A2, A8, YELLOW_2:22
;
c . (sup D') = sup D
by A11, WAYBEL_1:58;
then
x1 <= sup D'
by A9, A12, YELLOW_0:60;
then
y' <= sup D'
by A10, ORDERS_2:26;
then consider d' being
Element of
L such that A13:
(
d' in D' &
y' <= d' )
by A7, WAYBEL_3:def 1;
reconsider d =
d' as
Element of
(Image c) by A13;
take d =
d;
:: thesis: ( d in D & x' <= d )thus
d in D
by A13;
:: thesis: x' <= d
d in the
carrier of
(Image c)
;
then
d in rng c
by YELLOW_0:def 15;
then
d' in { z where z is Element of L : z = c . z }
by A2, YELLOW_2:21;
then consider z' being
Element of
L such that A14:
(
d' = z' &
z' = c . z' )
;
c . y' <= c . d'
by A2, A13, WAYBEL_1:def 2;
hence
x' <= d
by A5, A14, YELLOW_0:61;
:: thesis: verum end;
then
x' << x'
by WAYBEL_3:def 1;
then
x' is compact
by WAYBEL_3:def 2;
then
x in the carrier of (CompactSublatt (Image c))
by Def1;
hence
x in [#] (CompactSublatt (Image c))
; :: thesis: verum