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)

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

hence
sup (f .: D) = f . (sup D)
by A3, ORDERS_2:2; :: thesis: verum
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;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