let X, Y be non empty set ; 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; 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; 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:]; for F being Function of S2,S1 st F is currying holds
F is monotone
let F be Function of S2,S1; ( 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
; WAYBEL27:def 2 F is monotone
let f, g be Element of S2; WAYBEL_1:def 2 ( not f <= g or F . f <= F . g )
reconsider a = f, b = g as Element of (T |^ [:X,Y:]) by YELLOW_0:58;
A2:
dom F = the carrier of S2
by FUNCT_2:def 1;
then A3:
F . g = curry b
by A1;
reconsider Fa = F . f, Fb = F . g as Element of ((T |^ Y) |^ X) by YELLOW_0:58;
assume
f <= g
; F . f <= F . g
then A4:
a <= b
by YELLOW_0:59;
A5:
the carrier of (T |^ Y) = Funcs (Y, the carrier of T)
by YELLOW_1:28;
then A6:
the carrier of ((T |^ Y) |^ X) = Funcs (X,(Funcs (Y, the carrier of T)))
by YELLOW_1:28;
A7:
F . f = curry a
by A2, A1;
now for x being Element of X holds Fa . x <= Fb . xlet x be
Element of
X;
Fa . x <= Fb . xnow for y being Element of Y holds (Fa . x) . y <= (Fb . x) . ylet y be
Element of
Y;
(Fa . x) . y <= (Fb . x) . yreconsider xy =
[x,y] as
Element of
[:X,Y:] ;
Fa . x is
Function of
Y, the
carrier of
T
by A5, FUNCT_2:66;
then A8:
dom (Fa . x) = Y
by FUNCT_2:def 1;
Fa is
Function of
X,
(Funcs (Y, the carrier of T))
by A6, FUNCT_2:66;
then
dom Fa = X
by FUNCT_2:def 1;
then
(Fa . x) . y = a . (
x,
y)
by A8, A7, FUNCT_5:31;
then A9:
(Fa . x) . y = a . xy
;
Fb . x is
Function of
Y, the
carrier of
T
by A5, FUNCT_2:66;
then A10:
dom (Fb . x) = Y
by FUNCT_2:def 1;
Fb is
Function of
X,
(Funcs (Y, the carrier of T))
by A6, FUNCT_2:66;
then
dom Fb = X
by FUNCT_2:def 1;
then
(Fb . x) . y = b . (
x,
y)
by A10, A3, FUNCT_5:31;
hence
(Fa . x) . y <= (Fb . x) . y
by A9, A4, Th14;
verum end; hence
Fa . x <= Fb . x
by Th14;
verum end;
then
Fa <= Fb
by Th14;
hence
F . f <= F . g
by YELLOW_0:60; verum