let L be lower-bounded meet-continuous Semilattice; :: thesis: for I being Ideal of L holds DownMap I is approximating
let I be Ideal of L; :: thesis: DownMap I is approximating
for x being Element of L ex ii being Subset of L st
( ii = (DownMap I) . x & x = sup ii )
proof
let x be Element of L; :: thesis: ex ii being Subset of L st
( ii = (DownMap I) . x & x = sup ii )
set ii = (DownMap I) . x;
(DownMap I) . x in the carrier of (InclPoset (Ids L)) ;
then (DownMap I) . x in Ids L by YELLOW_1:1;
then consider ii9 being Ideal of L such that
A1: ii9 = (DownMap I) . x ;
reconsider dI = (downarrow x) /\ I as Subset of L ;
per cases ( x <= sup I or not x <= sup I ) ;
suppose A2: x <= sup I ; :: thesis: ex ii being Subset of L st
( ii = (DownMap I) . x & x = sup ii )
then sup ii9 = sup dI by A1, Def16
.= sup ({x} "/\" I) by Th36
.= x "/\" (sup I) by WAYBEL_2:def 6
.= x by A2, YELLOW_0:25 ;
hence ex ii being Subset of L st
( ii = (DownMap I) . x & x = sup ii ) by A1; :: thesis: verum
end;
suppose not x <= sup I ; :: thesis: ex ii being Subset of L st
( ii = (DownMap I) . x & x = sup ii )
then sup ii9 = sup (downarrow x) by A1, Def16
.= x by WAYBEL_0:34 ;
hence ex ii being Subset of L st
( ii = (DownMap I) . x & x = sup ii ) by A1; :: thesis: verum
end;
end;
end;
hence DownMap I is approximating ; :: thesis: verum