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 Z being Scott TopAugmentation of Image (LowerAdj g)
for d being Function of X,Y
for d' being Function of X,Z st d = LowerAdj g & d' = d & d is relatively_open holds
d' is open
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 Z being Scott TopAugmentation of Image (LowerAdj g)
for d being Function of X,Y
for d' being Function of X,Z st d = LowerAdj g & d' = d & d is relatively_open holds
d' is open
let X be Scott TopAugmentation of T; :: thesis: for Y being Scott TopAugmentation of S
for Z being Scott TopAugmentation of Image (LowerAdj g)
for d being Function of X,Y
for d' being Function of X,Z st d = LowerAdj g & d' = d & d is relatively_open holds
d' is open
let Y be Scott TopAugmentation of S; :: thesis: for Z being Scott TopAugmentation of Image (LowerAdj g)
for d being Function of X,Y
for d' being Function of X,Z st d = LowerAdj g & d' = d & d is relatively_open holds
d' is open
let Z be Scott TopAugmentation of Image (LowerAdj g); :: thesis: for d being Function of X,Y
for d' being Function of X,Z st d = LowerAdj g & d' = d & d is relatively_open holds
d' is open
let d be Function of X,Y; :: thesis: for d' being Function of X,Z st d = LowerAdj g & d' = d & d is relatively_open holds
d' is open
let d' be Function of X,Z; :: thesis: ( d = LowerAdj g & d' = d & d is relatively_open implies d' is open )
assume that
A1:
( d = LowerAdj g & d' = d )
and
A2:
for V being open Subset of X holds d .: V is open Subset of (Y | (rng d))
; :: according to WAYBEL34:def 9 :: thesis: d' is open
let V be Subset of X; :: according to T_0TOPSP:def 2 :: thesis: ( not V is open or d' .: V is open )
assume
V is open
; :: thesis: d' .: V is open
then reconsider A = d .: V as open Subset of (Y | (rng d)) by A2;
A3:
Image (LowerAdj g) = subrelstr (rng (LowerAdj g))
by YELLOW_2:def 2;
then A4:
the carrier of (Image (LowerAdj g)) = rng d
by A1, YELLOW_0:def 15;
A5:
( the carrier of (Y | (rng d)) = [#] (Y | (rng d)) & [#] (Y | (rng d)) = rng d )
by PRE_TOPC:def 10;
A6:
( RelStr(# the carrier of Z,the InternalRel of Z #) = Image (LowerAdj g) & 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 B = A as Subset of Z by A1, A3, A5, YELLOW_0:def 15;
A in the topology of (Y | (rng d))
by PRE_TOPC:def 5;
then consider C being Subset of Y such that
A7:
( C in the topology of Y & A = C /\ ([#] (Y | (rng d))) )
by PRE_TOPC:def 9;
C is open
by A7, PRE_TOPC:def 5;
then A8:
( C is upper & C is inaccessible_by_directed_joins )
by WAYBEL11:def 4;
A9:
B is upper
proof
let x,
y be
Element of
Z;
:: according to WAYBEL_0:def 20 :: thesis: ( not x in B or not x <= y or y in B )
reconsider x' =
x,
y' =
y as
Element of
(Image (LowerAdj g)) by A6;
reconsider a =
x',
b =
y' as
Element of
S by YELLOW_0:59;
reconsider a' =
a,
b' =
b as
Element of
Y by A6;
assume
(
x in B &
x <= y )
;
:: thesis: y in B
then
(
x' in C &
x' <= y' )
by A6, A7, XBOOLE_0:def 4, YELLOW_0:1;
then
(
a in C &
a <= b )
by YELLOW_0:60;
then
(
a' in C &
a' <= b' )
by A6, YELLOW_0:1;
then
(
b' in C &
y' in rng d )
by A4, A8, WAYBEL_0:def 20;
hence
y in B
by A5, A7, XBOOLE_0:def 4;
:: thesis: verum
end;
B is inaccessible_by_directed_joins
proof
let D be non
empty directed Subset of
Z;
:: according to WAYBEL11:def 1 :: thesis: ( not "\/" D,Z in B or not D misses B )
assume A10:
sup D in B
;
:: thesis: not D misses B
reconsider D' =
D as non
empty Subset of
(Image (LowerAdj g)) by A6;
reconsider E =
D' as non
empty Subset of
S by A4, A6, XBOOLE_1:1;
reconsider E' =
E as non
empty Subset of
Y by A6;
A11:
(
ex_sup_of D,
Z &
ex_sup_of D,
Y )
by YELLOW_0:17;
D' is
directed
by A6, WAYBEL_0:3;
then
E is
directed
by YELLOW_2:7;
then A12:
E' is
directed
by A6, WAYBEL_0:3;
A13:
ex_sup_of D',
S
by YELLOW_0:17;
Image (LowerAdj g) is
sups-inheriting
by YELLOW_2:34;
then
"\/" D',
S in the
carrier of
(Image (LowerAdj g))
by A13, YELLOW_0:def 19;
then sup E =
sup D'
by YELLOW_0:69
.=
sup D
by A6, A11, YELLOW_0:26
;
then
sup E' = sup D
by A6, A11, YELLOW_0:26;
then
sup E' in C
by A7, A10, XBOOLE_0:def 4;
then
C meets E
by A8, A12, WAYBEL11:def 1;
hence
D meets B
by A4, A5, A7, XBOOLE_1:77;
:: thesis: verum
end;
hence
d' .: V is open
by A1, A9, WAYBEL11:def 4; :: thesis: verum