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