let S be LATTICE; :: thesis: for T being lower-bounded up-complete LATTICE
for f being Function of S,T st ( for x being Element of S holds f . x = "\/" { (f . w) where w is Element of S : w << x } ,T ) holds
f is monotone
let T be lower-bounded up-complete LATTICE; :: thesis: for f being Function of S,T st ( for x being Element of S holds f . x = "\/" { (f . w) where w is Element of S : w << x } ,T ) holds
f is monotone
let f be Function of S,T; :: thesis: ( ( for x being Element of S holds f . x = "\/" { (f . w) where w is Element of S : w << x } ,T ) implies f is monotone )
assume A1:
for x being Element of S holds f . x = "\/" { (f . w) where w is Element of S : w << x } ,T
; :: thesis: f is monotone
let X, Y be Element of S; :: according to WAYBEL_1:def 2 :: thesis: ( not X <= Y or f . X <= f . Y )
deffunc H1( Element of S) -> Element of S = $1;
defpred S1[ Element of S] means $1 << X;
defpred S2[ Element of S] means $1 << Y;
assume
X <= Y
; :: thesis: f . X <= f . Y
then A2:
waybelow X c= waybelow Y
by WAYBEL_3:12;
A3:
f . X = "\/" { (f . w) where w is Element of S : w << X } ,T
by A1;
A4:
the carrier of S c= dom f
by FUNCT_2:def 1;
A5:
f .: { H1(w) where w is Element of S : S1[w] } = { (f . H1(w)) where w is Element of S : S1[w] }
from WAYBEL17:sch 2(A4);
f .: { H1(w) where w is Element of S : S2[w] } = { (f . H1(w)) where w is Element of S : S2[w] }
from WAYBEL17:sch 2(A4);
then A6:
f . Y = "\/" (f .: (waybelow Y)),T
by A1;
( ex_sup_of f .: (waybelow X),T & ex_sup_of f .: (waybelow Y),T )
by YELLOW_0:17;
hence
f . X <= f . Y
by A2, A3, A5, A6, RELAT_1:156, YELLOW_0:34; :: thesis: verum