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