let S be LATTICE; 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; 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; ( ( 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)
; f is monotone
thus
f is monotone
verumproof
let X,
Y be
Element of
S;
WAYBEL_1:def 2 ( not X <= Y or f . X <= f . Y )
assume
X <= Y
;
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;
A8:
ex_sup_of f .: (compactbelow X),
T
by YELLOW_0:17;
ex_sup_of f .: (compactbelow Y),
T
by YELLOW_0:17;
hence
f . X <= f . Y
by A2, A6, A7, A8, RELAT_1:123, YELLOW_0:34;
verum
end;