let L be complete continuous LATTICE; for p being projection Function of L,L st p is infs-preserving holds
( Image p is continuous LATTICE & Image p is infs-inheriting )
let p be projection Function of L,L; ( p is infs-preserving implies ( Image p is continuous LATTICE & Image p is infs-inheriting ) )
assume A1:
p is infs-preserving
; ( Image p is continuous LATTICE & Image p is infs-inheriting )
reconsider Lc = { c where c is Element of L : c <= p . c } as non empty Subset of L by WAYBEL_1:43;
reconsider pc = p | Lc as Function of (subrelstr Lc),(subrelstr Lc) by WAYBEL_1:45;
A2:
subrelstr Lc is infs-inheriting
by A1, WAYBEL_1:51;
then A3:
subrelstr Lc is complete
by YELLOW_2:30;
A4:
pc is infs-preserving
proof
let X be
Subset of
(subrelstr Lc);
WAYBEL_0:def 32 pc preserves_inf_of X
assume
ex_inf_of X,
subrelstr Lc
;
WAYBEL_0:def 30 ( ex_inf_of pc .: X, subrelstr Lc & "/\" ((pc .: X),(subrelstr Lc)) = pc . ("/\" (X,(subrelstr Lc))) )
thus
ex_inf_of pc .: X,
subrelstr Lc
by A3, YELLOW_0:17;
"/\" ((pc .: X),(subrelstr Lc)) = pc . ("/\" (X,(subrelstr Lc)))
the
carrier of
(subrelstr Lc) = Lc
by YELLOW_0:def 15;
then reconsider X9 =
X as
Subset of
L by XBOOLE_1:1;
A5:
(
ex_inf_of X9,
L &
p preserves_inf_of X9 )
by A1, YELLOW_0:17;
X c= the
carrier of
(subrelstr Lc)
;
then
X c= Lc
by YELLOW_0:def 15;
then A6:
pc .: X = p .: X
by RELAT_1:129;
A7:
ex_inf_of X,
L
by YELLOW_0:17;
then
"/\" (
X9,
L)
in the
carrier of
(subrelstr Lc)
by A2;
then A8:
(
dom pc = the
carrier of
(subrelstr Lc) &
inf X9 = inf X )
by A7, FUNCT_2:def 1, YELLOW_0:63;
(
ex_inf_of p .: X,
L &
"/\" (
(pc .: X),
L)
in the
carrier of
(subrelstr Lc) )
by A2, YELLOW_0:17;
hence inf (pc .: X) =
inf (p .: X)
by A6, YELLOW_0:63
.=
p . (inf X9)
by A5
.=
pc . (inf X)
by A8, FUNCT_1:47
;
verum
end;
reconsider cpc = corestr pc as Function of (subrelstr Lc),(Image pc) ;
A9: the carrier of (subrelstr (rng p)) =
rng p
by YELLOW_0:def 15
.=
rng pc
by WAYBEL_1:44
.=
the carrier of (subrelstr (rng pc))
by YELLOW_0:def 15
;
subrelstr (rng pc) is full SubRelStr of L
by WAYBEL15:1;
then A10:
Image p = Image pc
by A9, YELLOW_0:57;
pc is closure
by WAYBEL_1:47;
then A11:
cpc is sups-preserving
by WAYBEL_1:55;
subrelstr Lc is sups-inheriting SubRelStr of L
by WAYBEL_1:49;
then
subrelstr Lc is continuous LATTICE
by A2, WAYBEL_5:28;
hence
Image p is continuous LATTICE
by A3, A10, A4, A11, Th19, WAYBEL_5:33; Image p is infs-inheriting
thus
Image p is infs-inheriting
by A1, A2, WAYBEL_1:51; verum