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