let L be complete LATTICE; for k being kernel Function of L,L holds
( k is directed-sups-preserving iff corestr k is directed-sups-preserving )
let k be kernel Function of L,L; ( k is directed-sups-preserving iff corestr k is directed-sups-preserving )
set ck = corestr k;
[(corestr k),(inclusion k)] is Galois
by WAYBEL_1:42;
then A1:
inclusion k is lower_adjoint
by WAYBEL_1:def 12;
A2:
k = (inclusion k) * (corestr k)
by WAYBEL_1:35;
hereby ( corestr k is directed-sups-preserving implies k is directed-sups-preserving )
assume A3:
k is
directed-sups-preserving
;
corestr k is directed-sups-preserving thus
corestr k is
directed-sups-preserving
verumproof
let D be
Subset of
L;
WAYBEL_0:def 37 ( D is empty or not D is directed or corestr k preserves_sup_of D )
assume
( not
D is
empty &
D is
directed )
;
corestr k preserves_sup_of D
then A4:
k preserves_sup_of D
by A3, WAYBEL_0:def 37;
assume
ex_sup_of D,
L
;
WAYBEL_0:def 31 ( ex_sup_of (corestr k) .: D, Image k & "\/" (((corestr k) .: D),(Image k)) = (corestr k) . ("\/" (D,L)) )
then A5:
sup (k .: D) =
k . (sup D)
by A4, WAYBEL_0:def 31
.=
(inclusion k) . ((corestr k) . (sup D))
by A2, FUNCT_2:21
.=
(corestr k) . (sup D)
by FUNCT_1:35
;
thus
ex_sup_of (corestr k) .: D,
Image k
by YELLOW_0:17;
"\/" (((corestr k) .: D),(Image k)) = (corestr k) . ("\/" (D,L))
A6:
ex_sup_of (inclusion k) .: ((corestr k) .: D),
L
by YELLOW_0:17;
A7:
Image k is
sups-inheriting
by WAYBEL_1:56;
ex_sup_of (corestr k) .: D,
L
by YELLOW_0:17;
then A8:
"\/" (
((corestr k) .: D),
L)
in the
carrier of
(Image k)
by A7, YELLOW_0:def 19;
(corestr k) .: D = (inclusion k) .: ((corestr k) .: D)
by WAYBEL15:14;
hence sup ((corestr k) .: D) =
sup ((inclusion k) .: ((corestr k) .: D))
by A6, A8, YELLOW_0:65
.=
(corestr k) . (sup D)
by A2, A5, RELAT_1:159
;
verum
end;
end;
thus
( corestr k is directed-sups-preserving implies k is directed-sups-preserving )
by A1, A2, WAYBEL15:13; verum