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
now :: thesis: for a, b being Element of S st a <= b holds
f . 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;
hence f is monotone ; :: thesis: verum