let S, T be up-complete LATTICE; :: thesis: for f being Function of S,T st ( for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) ) holds
for D being non empty directed Subset of S holds sup (f .: D) = f . (sup D)
let f be Function of S,T; :: thesis: ( ( for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) ) implies for D being non empty directed Subset of S holds sup (f .: D) = f . (sup D) )
assume A1: for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) ; :: thesis: for D being non empty directed Subset of S holds sup (f .: D) = f . (sup D)
let D be non empty directed Subset of S; :: thesis: sup (f .: D) = f . (sup D)
A2: f is monotone by A1, Th11;
then A3: sup (f .: D) <= f . (sup D) by Th16;
f . (sup D) <= sup (f .: D)
proof
sup D = lim_inf (Net-Str D) by Th10;
then A4: f . (sup D) <= lim_inf (f * (Net-Str D)) by A1;
reconsider fN = f * (Net-Str D) as reflexive monotone net of T by A2;
A5: sup fN = Sup by WAYBEL_2:def 1
.= Sup by WAYBEL_9:def 8
.= sup (rng (f * ((id the carrier of S) | D))) by YELLOW_2:def 5 ;
rng (f * ((id the carrier of S) | D)) = rng (f * (id D)) by FUNCT_3:1
.= rng (f | D) by RELAT_1:65
.= f .: D by RELAT_1:115 ;
hence f . (sup D) <= sup (f .: D) by A4, A5, Lm6; :: thesis: verum
end;
hence sup (f .: D) = f . (sup D) by A3, ORDERS_2:2; :: thesis: verum