let S, T be complete LATTICE; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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 #) & 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 ;
let V be open Subset of X; :: thesis: (LowerAdj g) .: V = (rng (LowerAdj g)) /\ (uparrow ((LowerAdj g) .: V))
reconsider A = uparrow ((LowerAdj g) .: V) as Subset of Y by A1;
d .: V = A /\ (rng d)
proof
(
d .: V c= A &
d .: V c= rng d )
by RELAT_1:144, WAYBEL_0:16;
hence
d .: V c= A /\ (rng d)
by XBOOLE_1:19;
:: according to XBOOLE_0:def 10 :: thesis: A /\ (rng d) c= d .: V
let t be
set ;
:: according to TARSKI:def 3 :: thesis: ( not t in A /\ (rng d) or t in d .: V )
assume
t in A /\ (rng d)
;
:: thesis: t in d .: V
then A2:
(
t in A &
t in rng d )
by XBOOLE_0:def 4;
then reconsider t =
t as
Element of
S ;
consider x being
Element of
S such that A3:
(
x <= t &
x in (LowerAdj g) .: V )
by A2, WAYBEL_0:def 16;
consider u being
set such that A4:
(
u in the
carrier of
T &
u in V &
x = (LowerAdj g) . u )
by A3, FUNCT_2:115;
dom d = the
carrier of
T
by FUNCT_2:def 1;
then consider v being
set such that A5:
(
v in the
carrier of
T &
t = d . v )
by A2, FUNCT_1:def 5;
reconsider u =
u,
v =
v as
Element of
T by A4, A5;
A6:
(LowerAdj g) . (u "\/" v) =
x "\/" t
by A4, A5, WAYBEL_6:2
.=
t
by A3, YELLOW_0:24
;
reconsider V' =
V as
Subset of
T by A1;
V is
upper
by WAYBEL11:def 4;
then
(
V' is
upper &
u <= u "\/" v )
by A1, WAYBEL_0:25, YELLOW_0:22;
then
u "\/" v in V'
by A4, WAYBEL_0:def 20;
hence
t in d .: V
by A6, FUNCT_2:43;
:: thesis: verum
end;
hence
(LowerAdj g) .: V = (rng (LowerAdj g)) /\ (uparrow ((LowerAdj g) .: V))
; :: thesis: verum