let S, T be 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 monotone

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 monotone )

assume A1: for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) ; :: thesis: f is monotone

f is monotone

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 monotone )

assume A1: for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) ; :: thesis: f is monotone

now :: thesis: for a, b being Element of S st a <= b holds

f . a <= f . b

hence
f is monotone
; :: thesis: verumf . a <= f . b

let a, b be Element of S; :: thesis: ( a <= b implies f . a <= f . b )

assume A2: a <= b ; :: thesis: f . a <= f . b

set N = Net-Str (a,b);

A3: f . (lim_inf (Net-Str (a,b))) = f . a by A2, Lm5;

lim_inf (f * (Net-Str (a,b))) = (f . a) "/\" (f . b) by Th8;

then A4: f . a <= (f . a) "/\" (f . b) by A1, A3;

f . a >= (f . a) "/\" (f . b) by YELLOW_0:23;

then f . a = (f . a) "/\" (f . b) by A4, ORDERS_2:2;

hence f . a <= f . b by YELLOW_0:25; :: thesis: verum

end;assume A2: a <= b ; :: thesis: f . a <= f . b

set N = Net-Str (a,b);

A3: f . (lim_inf (Net-Str (a,b))) = f . a by A2, Lm5;

lim_inf (f * (Net-Str (a,b))) = (f . a) "/\" (f . b) by Th8;

then A4: f . a <= (f . a) "/\" (f . b) by A1, A3;

f . a >= (f . a) "/\" (f . b) by YELLOW_0:23;

then f . a = (f . a) "/\" (f . b) by A4, ORDERS_2:2;

hence f . a <= f . b by YELLOW_0:25; :: thesis: verum