let S, T be 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
f is directed-sups-preserving
let f be Function of S,T; :: thesis: ( ( for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) ) implies f is directed-sups-preserving )
assume A1: for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) ; :: thesis: f is directed-sups-preserving
thus f is directed-sups-preserving :: thesis: verum

proof

let D be Subset of S; :: according to WAYBEL_0:def 37 :: thesis: ( D is empty or not D is directed or f preserves_sup_of D )
assume ( not D is empty & D is directed ) ; :: thesis: f preserves_sup_of D
then reconsider D = D as non empty directed Subset of S ;
A2: f is monotone by A1, Th11;
then A3: sup (f .: D) <= f . (sup D) by Th15;
A4: f . (sup D) <= sup (f .: D)

proof

sup D = lim_inf (Net-Str D) by Th10;
then A5: 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;
A6: 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:94
.= f .: D by RELAT_1:148 ;
hence f . (sup D) <= sup (f .: D) by A5, A6, WAYBEL11:22; :: thesis: verum

end;

f preserves_sup_of D

proof

assume ex_sup_of D,S ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of f .: D,T & "\/" (f .: D),T = f . ("\/" D,S) )
thus ( ex_sup_of f .: D,T & "\/" (f .: D),T = f . ("\/" D,S) ) by A3, A4, ORDERS_2:25, YELLOW_0:17; :: thesis: verum

end;

hence f preserves_sup_of D ; :: thesis: verum

end;