let S be LATTICE; :: thesis: for T being 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 & w is compact ) } ,T ) holds
f is monotone
let T be 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 & w is compact ) } ,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 & w is compact ) } ,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 & w is compact ) } ,T
; :: thesis: f is monotone
thus
f is monotone
:: thesis: verumproof
let X,
Y be
Element of
S;
:: according to WAYBEL_1:def 2 :: thesis: ( not X <= Y or f . X <= f . Y )
assume
X <= Y
;
:: thesis: f . X <= f . Y
then A2:
compactbelow X c= compactbelow Y
by WAYBEL13:1;
A3:
f . X = "\/" { (f . w) where w is Element of S : ( w <= X & w is compact ) } ,
T
by A1;
A4:
f . Y = "\/" { (f . w) where w is Element of S : ( w <= Y & w is compact ) } ,
T
by A1;
A5:
the
carrier of
S c= dom f
by FUNCT_2:def 1;
defpred S1[
Element of
S]
means ( $1
<= X & $1 is
compact );
defpred S2[
Element of
S]
means ( $1
<= Y & $1 is
compact );
deffunc H1(
Element of
S)
-> Element of
S = $1;
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(A5);
then A6:
f . X = "\/" (f .: (compactbelow X)),
T
by A3, WAYBEL_8:def 2;
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(A5);
then A7:
f . Y = "\/" (f .: (compactbelow Y)),
T
by A4, WAYBEL_8:def 2;
(
ex_sup_of f .: (compactbelow X),
T &
ex_sup_of f .: (compactbelow Y),
T )
by YELLOW_0:17;
hence
f . X <= f . Y
by A2, A6, A7, RELAT_1:156, YELLOW_0:34;
:: thesis: verum
end;