let S, T be complete LATTICE; for g being infs-preserving Function of S,T st g is V7() holds
for X being Scott TopAugmentation of T
for Y being Scott TopAugmentation of S
for d being Function of X,Y st d = LowerAdj g holds
( g is directed-sups-preserving iff d is open )
let g be infs-preserving Function of S,T; ( g is V7() implies for X being Scott TopAugmentation of T
for Y being Scott TopAugmentation of S
for d being Function of X,Y st d = LowerAdj g holds
( g is directed-sups-preserving iff d is open ) )
assume A1:
g is V7()
; for X being Scott TopAugmentation of T
for Y being Scott TopAugmentation of S
for d being Function of X,Y st d = LowerAdj g holds
( g is directed-sups-preserving iff d is open )
let X be Scott TopAugmentation of T; for Y being Scott TopAugmentation of S
for d being Function of X,Y st d = LowerAdj g holds
( g is directed-sups-preserving iff d is open )
let Y be Scott TopAugmentation of S; for d being Function of X,Y st d = LowerAdj g holds
( g is directed-sups-preserving iff d is open )
[g,(LowerAdj g)] is Galois
by Def1;
then
LowerAdj g is onto
by A1, WAYBEL_1:27;
then A2:
rng (LowerAdj g) = the carrier of S
by FUNCT_2:def 3;
A3:
RelStr(# the carrier of Y, the InternalRel of Y #) = RelStr(# the carrier of S, the InternalRel of S #)
by YELLOW_9:def 4;
A4:
RelStr(# the carrier of X, the InternalRel of X #) = RelStr(# the carrier of T, the InternalRel of T #)
by YELLOW_9:def 4;
A5:
[#] Y = the carrier of Y
;
let d be Function of X,Y; ( d = LowerAdj g implies ( g is directed-sups-preserving iff d is open ) )
assume A6:
d = LowerAdj g
; ( g is directed-sups-preserving iff d is open )
A7:
Y | (rng d) = TopStruct(# the carrier of Y, the topology of Y #)
by A2, A3, A5, A6, TSEP_1:93;
thus
( g is directed-sups-preserving implies d is open )
( d is open implies g is directed-sups-preserving )
assume A9:
for V being Subset of X st V is open holds
d .: V is open
; T_0TOPSP:def 2 g is directed-sups-preserving
now for X9 being Scott TopAugmentation of T
for Y9 being Scott TopAugmentation of S
for V9 being open Subset of X9 holds uparrow ((LowerAdj g) .: V9) is open Subset of Y9let X9 be
Scott TopAugmentation of
T;
for Y9 being Scott TopAugmentation of S
for V9 being open Subset of X9 holds uparrow ((LowerAdj g) .: V9) is open Subset of Y9let Y9 be
Scott TopAugmentation of
S;
for V9 being open Subset of X9 holds uparrow ((LowerAdj g) .: V9) is open Subset of Y9let V9 be
open Subset of
X9;
uparrow ((LowerAdj g) .: V9) is open Subset of Y9A10:
RelStr(# the
carrier of
X9, the
InternalRel of
X9 #)
= RelStr(# the
carrier of
T, the
InternalRel of
T #)
by YELLOW_9:def 4;
A11:
RelStr(# the
carrier of
Y9, the
InternalRel of
Y9 #)
= RelStr(# the
carrier of
S, the
InternalRel of
S #)
by YELLOW_9:def 4;
reconsider V =
V9 as
Subset of
X by A4, A10;
reconsider V =
V as
open Subset of
X by A4, A10, YELLOW_9:50;
reconsider d9 =
d as
Function of
X9,
Y9 by A3, A4, A10, A11;
d .: V is
open
by A9;
then A12:
d9 .: V9 is
open Subset of
Y9
by A3, A11, YELLOW_9:50;
then
d9 .: V9 is
upper
by WAYBEL11:def 4;
then A13:
uparrow (d9 .: V9) c= d9 .: V9
by WAYBEL_0:24;
d9 .: V9 c= uparrow (d9 .: V9)
by WAYBEL_0:16;
then
uparrow (d9 .: V9) = d9 .: V9
by A13;
hence
uparrow ((LowerAdj g) .: V9) is
open Subset of
Y9
by A6, A11, A12, WAYBEL_0:13;
verum end;
hence
g is directed-sups-preserving
by Th21; verum