let S, T be up-complete LATTICE; :: thesis: for f being Function of S,T
for N being non empty monotone NetStr of S st f is monotone holds
f * N is monotone
let f be Function of S,T; :: thesis: for N being non empty monotone NetStr of S st f is monotone holds
f * N is monotone
let N be non empty monotone NetStr of S; :: thesis: ( f is monotone implies f * N is monotone )
assume A1:
f is monotone
; :: thesis: f * N is monotone
A2:
netmap N,S is monotone
by WAYBEL_0:def 9;
A3:
netmap (f * N),T = f * (netmap N,S)
by WAYBEL_9:def 8;
set g = netmap (f * N),T;
now let x,
y be
Element of
(f * N);
:: thesis: ( x <= y implies (netmap (f * N),T) . x <= (netmap (f * N),T) . y )assume A4:
x <= y
;
:: thesis: (netmap (f * N),T) . x <= (netmap (f * N),T) . yA5:
RelStr(# the
carrier of
N,the
InternalRel of
N #)
= RelStr(# the
carrier of
(f * N),the
InternalRel of
(f * N) #)
by WAYBEL_9:def 8;
then reconsider x' =
x,
y' =
y as
Element of
N ;
A6:
dom (netmap N,S) = the
carrier of
(f * N)
by A5, FUNCT_2:def 1;
then A7:
(netmap (f * N),T) . x = f . ((netmap N,S) . x)
by A3, FUNCT_1:23;
A8:
(netmap (f * N),T) . y = f . ((netmap N,S) . y)
by A3, A6, FUNCT_1:23;
[x,y] in the
InternalRel of
(f * N)
by A4, ORDERS_2:def 9;
then
x' <= y'
by A5, ORDERS_2:def 9;
then
(netmap N,S) . x' <= (netmap N,S) . y'
by A2, WAYBEL_1:def 2;
hence
(netmap (f * N),T) . x <= (netmap (f * N),T) . y
by A1, A7, A8, WAYBEL_1:def 2;
:: thesis: verum end;
then
netmap (f * N),T is monotone
by WAYBEL_1:def 2;
hence
f * N is monotone
by WAYBEL_0:def 9; :: thesis: verum