let S be complete LATTICE; :: thesis: for T being continuous complete LATTICE
for g being infs-preserving Function of S,T st LowerAdj g is waybelow-preserving holds
g is directed-sups-preserving
let T be continuous complete LATTICE; :: thesis: for g being infs-preserving Function of S,T st LowerAdj g is waybelow-preserving holds
g is directed-sups-preserving
let g be infs-preserving Function of S,T; :: thesis: ( LowerAdj g is waybelow-preserving implies g is directed-sups-preserving )
assume A1: for t, t9 being Element of T st t << t9 holds
(LowerAdj g) . t << (LowerAdj g) . t9 ; :: according to WAYBEL34:def 8 :: thesis: g is directed-sups-preserving
let D be Subset of S; :: according to WAYBEL_0:def 37 :: thesis: ( D is empty or not D is directed or g preserves_sup_of D )
assume A2: ( not D is empty & D is directed ) ; :: thesis: g preserves_sup_of D
assume ex_sup_of D,S ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of g .: D,T & "\/" ((g .: D),T) = g . ("\/" (D,S)) )
thus ex_sup_of g .: D,T by YELLOW_0:17; :: thesis: "\/" ((g .: D),T) = g . ("\/" (D,S))
A3: sup (g .: D) <= g . (sup D) by WAYBEL17:15;
A4: g . (sup D) = sup (waybelow (g . (sup D))) by WAYBEL_3:def 5;
waybelow (g . (sup D)) is_<=_than sup (g .: D)
proof
let t be Element of T; :: according to LATTICE3:def 9 :: thesis: ( not t in waybelow (g . (sup D)) or t <= sup (g .: D) )
assume t in waybelow (g . (sup D)) ; :: thesis: t <= sup (g .: D)
then t << g . (sup D) by WAYBEL_3:7;
then A5: (LowerAdj g) . t << (LowerAdj g) . (g . (sup D)) by A1;
A6: [g,(LowerAdj g)] is Galois by Def1;
then A7: (LowerAdj g) * g <= id S by WAYBEL_1:18;
(id S) . (sup D) = sup D by FUNCT_1:18;
then ((LowerAdj g) * g) . (sup D) <= sup D by A7, YELLOW_2:9;
then (LowerAdj g) . (g . (sup D)) <= sup D by FUNCT_2:15;
then consider x being Element of S such that
A8: x in D and
A9: (LowerAdj g) . t <= x by A2, A5;
A10: g . x in g .: D by A8, FUNCT_2:35;
A11: t <= g . x by A6, A9, WAYBEL_1:8;
g . x <= sup (g .: D) by A10, YELLOW_2:22;
hence t <= sup (g .: D) by A11, ORDERS_2:3; :: thesis: verum
end;
then g . (sup D) <= sup (g .: D) by A4, YELLOW_0:32;
hence "\/" ((g .: D),T) = g . ("\/" (D,S)) by A3, ORDERS_2:2; :: thesis: verum