let S, T be complete LATTICE; for g being infs-preserving Function of S,T
for X being Scott TopAugmentation of T
for Y being Scott TopAugmentation of S
for V being open Subset of X holds (LowerAdj g) .: V = (rng (LowerAdj g)) /\ (uparrow ((LowerAdj g) .: V))
let g be infs-preserving Function of S,T; for X being Scott TopAugmentation of T
for Y being Scott TopAugmentation of S
for V being open Subset of X holds (LowerAdj g) .: V = (rng (LowerAdj g)) /\ (uparrow ((LowerAdj g) .: V))
let X be Scott TopAugmentation of T; for Y being Scott TopAugmentation of S
for V being open Subset of X holds (LowerAdj g) .: V = (rng (LowerAdj g)) /\ (uparrow ((LowerAdj g) .: V))
let Y be Scott TopAugmentation of S; for V being open Subset of X holds (LowerAdj g) .: V = (rng (LowerAdj g)) /\ (uparrow ((LowerAdj g) .: V))
A1:
RelStr(# the carrier of X, the InternalRel of X #) = RelStr(# the carrier of T, the InternalRel of T #)
by YELLOW_9:def 4;
A2:
RelStr(# the carrier of Y, the InternalRel of Y #) = RelStr(# the carrier of S, the InternalRel of S #)
by YELLOW_9:def 4;
then reconsider d = LowerAdj g as Function of X,Y by A1;
let V be open Subset of X; (LowerAdj g) .: V = (rng (LowerAdj g)) /\ (uparrow ((LowerAdj g) .: V))
reconsider A = uparrow ((LowerAdj g) .: V) as Subset of Y by A2;
d .: V = A /\ (rng d)
proof
A3:
d .: V c= A
by WAYBEL_0:16;
d .: V c= rng d
by RELAT_1:111;
hence
d .: V c= A /\ (rng d)
by A3, XBOOLE_1:19;
XBOOLE_0:def 10 A /\ (rng d) c= d .: V
let t be
object ;
TARSKI:def 3 ( not t in A /\ (rng d) or t in d .: V )
assume A4:
t in A /\ (rng d)
;
t in d .: V
then A5:
t in A
by XBOOLE_0:def 4;
A6:
t in rng d
by A4, XBOOLE_0:def 4;
reconsider t =
t as
Element of
S by A5;
consider x being
Element of
S such that A7:
x <= t
and A8:
x in (LowerAdj g) .: V
by A5, WAYBEL_0:def 16;
consider u being
object such that A9:
u in the
carrier of
T
and A10:
u in V
and A11:
x = (LowerAdj g) . u
by A8, FUNCT_2:64;
dom d = the
carrier of
T
by FUNCT_2:def 1;
then consider v being
object such that A12:
v in the
carrier of
T
and A13:
t = d . v
by A6, FUNCT_1:def 3;
reconsider u =
u,
v =
v as
Element of
T by A9, A12;
A14:
(LowerAdj g) . (u "\/" v) =
x "\/" t
by A11, A13, WAYBEL_6:2
.=
t
by A7, YELLOW_0:24
;
reconsider V9 =
V as
Subset of
T by A1;
V is
upper
by WAYBEL11:def 4;
then A15:
V9 is
upper
by A1, WAYBEL_0:25;
u <= u "\/" v
by YELLOW_0:22;
then
u "\/" v in V9
by A10, A15;
hence
t in d .: V
by A14, FUNCT_2:35;
verum
end;
hence
(LowerAdj g) .: V = (rng (LowerAdj g)) /\ (uparrow ((LowerAdj g) .: V))
; verum