let X, Y be non empty set ; :: thesis: for T being non empty Poset
for S1 being non empty full SubRelStr of (T |^ Y) |^ X
for S2 being non empty full SubRelStr of T |^ [:X,Y:]
for F being Function of S2,S1 st F is currying holds
F is monotone
let T be non empty Poset; :: thesis: for S1 being non empty full SubRelStr of (T |^ Y) |^ X
for S2 being non empty full SubRelStr of T |^ [:X,Y:]
for F being Function of S2,S1 st F is currying holds
F is monotone
let S1 be non empty full SubRelStr of (T |^ Y) |^ X; :: thesis: for S2 being non empty full SubRelStr of T |^ [:X,Y:]
for F being Function of S2,S1 st F is currying holds
F is monotone
let S2 be non empty full SubRelStr of T |^ [:X,Y:]; :: thesis: for F being Function of S2,S1 st F is currying holds
F is monotone
let F be Function of S2,S1; :: thesis: ( F is currying implies F is monotone )
assume that
for x being set st x in dom F holds
( x is Function & proj1 x is Relation )
and
A1:
for f being Function st f in dom F holds
F . f = curry f
; :: according to WAYBEL27:def 2 :: thesis: F is monotone
let f, g be Element of S2; :: according to WAYBEL_1:def 2 :: thesis: ( not f <= g or F . f <= F . g )
reconsider a = f, b = g as Element of (T |^ [:X,Y:]) by YELLOW_0:59;
reconsider Fa = F . f, Fb = F . g as Element of ((T |^ Y) |^ X) by YELLOW_0:59;
assume
f <= g
; :: thesis: F . f <= F . g
then A2:
a <= b
by YELLOW_0:60;
A3:
the carrier of (T |^ Y) = Funcs Y,the carrier of T
by YELLOW_1:28;
then A4:
the carrier of ((T |^ Y) |^ X) = Funcs X,(Funcs Y,the carrier of T)
by YELLOW_1:28;
dom F = the carrier of S2
by FUNCT_2:def 1;
then A5:
( F . f = curry a & F . g = curry b )
by A1;
now let x be
Element of
X;
:: thesis: Fa . x <= Fb . xnow let y be
Element of
Y;
:: thesis: (Fa . x) . y <= (Fb . x) . yreconsider xy =
[x,y] as
Element of
[:X,Y:] ;
(
Fa is
Function of
X,
(Funcs Y,the carrier of T) &
Fb is
Function of
X,
(Funcs Y,the carrier of T) &
Fa . x is
Function of
Y,the
carrier of
T &
Fb . x is
Function of
Y,the
carrier of
T )
by A3, A4, FUNCT_2:121;
then
(
dom Fa = X &
dom Fb = X &
dom (Fa . x) = Y &
dom (Fb . x) = Y )
by FUNCT_2:def 1;
then
(
(Fa . x) . y = a . x,
y &
(Fb . x) . y = b . x,
y )
by A5, FUNCT_5:38;
then
(
(Fa . x) . y = a . xy &
(Fb . x) . y = b . xy )
;
hence
(Fa . x) . y <= (Fb . x) . y
by A2, Th14;
:: thesis: verum end; hence
Fa . x <= Fb . x
by Th14;
:: thesis: verum end;
then
( Fa <= Fb & F . f in the carrier of S1 )
by Th14;
hence
F . f <= F . g
by YELLOW_0:61; :: thesis: verum