let R, S, T be complete LATTICE; :: thesis: for f being directed-sups-preserving Function of [:R,S:],T holds curry f is directed-sups-preserving Function of R,(UPS S,T)
A1:
UPS S,T is full SubRelStr of T |^ the carrier of S
by Def4;
A2:
[:the carrier of R,the carrier of S:] = the carrier of [:R,S:]
by YELLOW_3:def 2;
let f be directed-sups-preserving Function of [:R,S:],T; :: thesis: curry f is directed-sups-preserving Function of R,(UPS S,T)
A3:
dom f = the carrier of [:R,S:]
by FUNCT_2:def 1;
( f in the carrier of (UPS [:R,S:],T) & the carrier of (UPS [:R,S:],T) c= Funcs the carrier of [:R,S:],the carrier of T )
by Def4, Th22;
then
curry f in Funcs the carrier of R,(Funcs the carrier of S,the carrier of T)
by A2, FUNCT_6:19;
then A4:
curry f is Function of the carrier of R,(Funcs the carrier of S,the carrier of T)
by FUNCT_2:121;
then A5:
dom (curry f) = the carrier of R
by FUNCT_2:def 1;
rng (curry f) c= the carrier of (UPS S,T)
then reconsider g = curry f as Function of R,(UPS S,T) by A5, FUNCT_2:4;
g is directed-sups-preserving
proof
let A be
Subset of
R;
:: according to WAYBEL_0:def 37 :: thesis: ( A is empty or not A is directed or g preserves_sup_of A )
assume
( not
A is
empty &
A is
directed )
;
:: thesis: g preserves_sup_of A
then reconsider B =
A as non
empty directed Subset of
R ;
assume
ex_sup_of A,
R
;
:: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of g .: A, UPS S,T & "\/" (g .: A),(UPS S,T) = g . ("\/" A,R) )
thus
ex_sup_of g .: A,
UPS S,
T
by YELLOW_0:17;
:: thesis: "\/" (g .: A),(UPS S,T) = g . ("\/" A,R)
the
carrier of
(UPS S,T) c= the
carrier of
(T |^ the carrier of S)
by A1, YELLOW_0:def 13;
then
g .: B c= the
carrier of
(T |^ the carrier of S)
by XBOOLE_1:1;
then reconsider gA =
g .: A as non
empty Subset of
(T |^ the carrier of S) ;
reconsider gsA =
g . (sup A) as
Element of
(T |^ the carrier of S) by A1, YELLOW_0:59;
A7:
for
s being
Element of
S holds
(the carrier of S --> T) . s is
complete LATTICE
by FUNCOP_1:13;
A8:
T |^ the
carrier of
S = product (the carrier of S --> T)
by YELLOW_1:def 5;
then A9:
dom gsA = the
carrier of
S
by WAYBEL_3:27;
A10:
(
dom (sup gA) = the
carrier of
S &
dom gsA = the
carrier of
S )
by A8, WAYBEL_3:27;
now let x be
set ;
:: thesis: ( x in the carrier of S implies (sup gA) . x = gsA . x )assume
x in the
carrier of
S
;
:: thesis: (sup gA) . x = gsA . xthen reconsider s =
x as
Element of
S ;
reconsider s1 =
{s} as non
empty directed Subset of
S by WAYBEL_0:5;
reconsider As =
[:B,s1:] as non
empty directed Subset of
[:R,S:] ;
A11:
(
f preserves_sup_of As &
ex_sup_of As,
[:R,S:] )
by WAYBEL_0:def 37, YELLOW_0:17;
(the carrier of S --> T) . s = T
by FUNCOP_1:13;
hence (sup gA) . x =
sup (pi gA,s)
by A7, A8, WAYBEL_3:32
.=
sup (f .: As)
by A3, Th9
.=
f . (sup As)
by A11, WAYBEL_0:def 31
.=
f . [(sup (proj1 As)),(sup (proj2 As))]
by YELLOW_3:46
.=
f . [(sup A),(sup (proj2 As))]
by FUNCT_5:11
.=
f . [(sup A),(sup {s})]
by FUNCT_5:11
.=
f . (sup A),
s
by YELLOW_0:39
.=
gsA . x
by A5, A9, FUNCT_5:38
;
:: thesis: verum end;
then
sup gA = gsA
by A10, FUNCT_1:9;
hence
"\/" (g .: A),
(UPS S,T) = g . ("\/" A,R)
by Th27;
:: thesis: verum
end;
hence
curry f is directed-sups-preserving Function of R,(UPS S,T)
; :: thesis: verum