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:66;
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 for A being Subset of L st A is open holds
sF " A is open let A be
Subset of
L;
( A is open implies sF " A is open )assume A2:
A is
open
;
sF " A is open now for x being set holds
( ( 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 ) )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 7;
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
;
then A7:
(
pi (
aF,
y) is
directed & not
pi (
aF,
y) is
empty )
by A5, YELLOW16:35;
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:33;
then
pi (
aF,
y)
meets A
by A2, A4, A7, WAYBEL11:def 1;
then consider a being
object 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:43;
( 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
object ;
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 7;
reconsider b =
b as
Element of
X by A14;
A16:
( the carrier of X => L) . b = L
;
then
(
pi (
aF,
b) is
directed & not
pi (
aF,
b) is
empty )
by A5, YELLOW16:35;
then A17:
ex_sup_of pi (
aF,
b),
L
by WAYBEL_0:75;
sF . b = sup (pi (aF,b))
by A8, A5, A16, YELLOW16:33;
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;
then
sF . b in A
by A2, A15, WAYBEL_0:def 20;
hence
b in sF " A
by A13, FUNCT_1:def 7;
verum
end;
dom f = the
carrier of
X
by FUNCT_2:def 1;
hence
x in Q
by A10, A12, FUNCT_1:def 7;
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:25;
verum end;
[#] L <> {}
;
hence
"\/" (F,(L |^ the carrier of X)) is continuous Function of X,L
by A1, TOPS_2:43; verum