let X be non empty TopSpace; for L being non empty up-complete Scott TopPoset
for F being non empty directed Subset of (ContMaps X,L) holds "\/" F,(L |^ the carrier of X) is continuous Function of X,L
let L be non empty up-complete Scott TopPoset; for F being non empty directed Subset of (ContMaps X,L) holds "\/" F,(L |^ the carrier of X) is continuous Function of X,L
let F be non empty directed Subset of (ContMaps X,L); "\/" F,(L |^ the carrier of X) is continuous Function of X,L
set sF = "\/" F,(L |^ the carrier of X);
Funcs the carrier of X,the carrier of L = the carrier of (L |^ the carrier of X)
by YELLOW_1:28;
then reconsider sF = "\/" F,(L |^ the carrier of X) as Function of X,L by FUNCT_2:121;
ContMaps X,L is full SubRelStr of L |^ the carrier of X
by WAYBEL24:def 3;
then reconsider aF = F as non empty directed Subset of (L |^ the carrier of X) by YELLOW_2:7;
A1:
now let A be
Subset of
L;
( A is open implies sF " A is open )assume A2:
A is
open
;
sF " A is open now let x be
set ;
( ( x in sF " A implies ex Q being Element of bool the carrier of X st
( Q is open & Q c= sF " A & x in Q ) ) & ( ex Q being Subset of X st
( Q is open & Q c= sF " A & x in Q ) implies x in sF " A ) )hereby ( ex Q being Subset of X st
( Q is open & Q c= sF " A & x in Q ) implies x in sF " A )
assume A3:
x in sF " A
;
ex Q being Element of bool the carrier of X st
( Q is open & Q c= sF " A & x in Q )then A4:
sF . x in A
by FUNCT_1:def 13;
reconsider y =
x as
Element of
X by A3;
A5:
the
carrier of
X -POS_prod (the carrier of X => L) = L |^ the
carrier of
X
by YELLOW_1:def 5;
A6:
(the carrier of X => L) . y = L
by FUNCOP_1:13;
then A7:
(
pi aF,
y is
directed & not
pi aF,
y is
empty )
by A5, YELLOW16:37;
A8:
ex_sup_of aF,
L |^ the
carrier of
X
by WAYBEL_0:75;
then
(sup aF) . y = sup (pi aF,y)
by A6, A5, YELLOW16:35;
then
pi aF,
y meets A
by A2, A4, A7, WAYBEL11:def 1;
then consider a being
set such that A9:
a in pi aF,
y
and A10:
a in A
by XBOOLE_0:3;
consider f being
Function such that A11:
f in aF
and A12:
a = f . y
by A9, CARD_3:def 6;
reconsider f =
f as
continuous Function of
X,
L by A11, WAYBEL24:21;
take Q =
f " A;
( Q is open & Q c= sF " A & x in Q )
[#] L <> {}
;
hence
Q is
open
by A2, TOPS_2:55;
( Q c= sF " A & x in Q )A13:
dom sF = the
carrier of
X
by FUNCT_2:def 1;
thus
Q c= sF " A
x in Qproof
let b be
set ;
TARSKI:def 3 ( not b in Q or b in sF " A )
assume A14:
b in Q
;
b in sF " A
then A15:
f . b in A
by FUNCT_1:def 13;
reconsider b =
b as
Element of
X by A14;
A16:
(the carrier of X => L) . b = L
by FUNCOP_1:13;
then
(
pi aF,
b is
directed & not
pi aF,
b is
empty )
by A5, YELLOW16:37;
then A17:
ex_sup_of pi aF,
b,
L
by WAYBEL_0:75;
sF . b = sup (pi aF,b)
by A8, A5, A16, YELLOW16:35;
then A18:
sF . b is_>=_than pi aF,
b
by A17, YELLOW_0:30;
f . b in pi aF,
b
by A11, CARD_3:def 6;
then
f . b <= sF . b
by A18, LATTICE3:def 9;
then
sF . b in A
by A2, A15, WAYBEL_0:def 20;
hence
b in sF " A
by A13, FUNCT_1:def 13;
verum
end;
dom f = the
carrier of
X
by FUNCT_2:def 1;
hence
x in Q
by A10, A12, FUNCT_1:def 13;
verum
end; thus
( ex
Q being
Subset of
X st
(
Q is
open &
Q c= sF " A &
x in Q ) implies
x in sF " A )
;
verum end; hence
sF " A is
open
by TOPS_1:57;
verum end;
[#] L <> {}
;
hence
"\/" F,(L |^ the carrier of X) is continuous Function of X,L
by A1, TOPS_2:55; verum