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

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)

hence f preserves_sup_of D ; :: thesis: verum

end;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

f preserves_sup_of D
by A3, A4, ORDERS_2:2, YELLOW_0:17;
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:65

.= f .: D by RELAT_1:115 ;

hence f . (sup D) <= sup (f .: D) by A5, A6, WAYBEL11:22; :: thesis: verum

end;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:65

.= f .: D by RELAT_1:115 ;

hence f . (sup D) <= sup (f .: D) by A5, A6, WAYBEL11:22; :: thesis: verum

hence f preserves_sup_of D ; :: thesis: verum