let L be complete Scott TopLattice; ( L is continuous implies sup_op L is jointly_Scott-continuous )
assume A1:
L is continuous
; sup_op L is jointly_Scott-continuous
set Tsup = sup_op L;
let T be non empty TopSpace; WAYBEL14:def 1 ( TopStruct(# the carrier of T,the topology of T #) = ConvergenceSpace (Scott-Convergence L) implies ex ft being Function of [:T,T:],T st
( ft = sup_op L & ft is continuous ) )
assume A2:
TopStruct(# the carrier of T,the topology of T #) = ConvergenceSpace (Scott-Convergence L)
; ex ft being Function of [:T,T:],T st
( ft = sup_op L & ft is continuous )
A3:
the carrier of [:T,T:] = [:the carrier of T,the carrier of T:]
by BORSUK_1:def 5;
A4:
the carrier of T = the carrier of L
by A2, YELLOW_6:def 27;
then
the carrier of [:T,T:] = the carrier of [:L,L:]
by A3, YELLOW_3:def 2;
then reconsider Tsup = sup_op L as Function of [:T,T:],T by A4;
take
Tsup
; ( Tsup = sup_op L & Tsup is continuous )
thus
Tsup = sup_op L
; Tsup is continuous
A5:
TopStruct(# the carrier of L,the topology of L #) = ConvergenceSpace (Scott-Convergence L)
by WAYBEL11:32;
for x being Point of holds Tsup is_continuous_at x
proof
reconsider Lc =
L as
complete continuous Scott TopLattice by A1;
let ab be
Point of ;
Tsup is_continuous_at ab
reconsider Tsab =
Tsup . ab as
Point of ;
consider a,
b being
Point of
such that A6:
ab = [a,b]
by A3, DOMAIN_1:9;
reconsider a' =
a,
b' =
b as
Element of
by A2, YELLOW_6:def 27;
set D1 =
waybelow a';
set D2 =
waybelow b';
set D =
(waybelow a') "\/" (waybelow b');
reconsider Tsab' =
Tsab as
Element of
by A2, YELLOW_6:def 27;
let G be
a_neighborhood of
Tsup . ab;
TMAP_1:def 2 ex b1 being a_neighborhood of ab st Tsup .: b1 c= G
A7:
(
Tsab in Int G &
Int G is
open )
by CONNSP_2:def 1, TOPS_1:51;
reconsider basab =
{ (wayabove q) where q is Element of : q << Tsab' } as
Basis of
Tsab' by A1, WAYBEL11:44;
basab is
Basis of
Tsab
by A2, A5, Th21;
then consider V being
Subset of
such that A8:
V in basab
and A9:
V c= Int G
by A7, YELLOW_8:def 2;
consider u being
Element of
such that A10:
V = wayabove u
and A11:
u << Tsab'
by A8;
A12:
(waybelow a') "\/" (waybelow b') = { (x "\/" y) where x, y is Element of : ( x in waybelow a' & y in waybelow b' ) }
by YELLOW_4:def 3;
Lc = L
;
then A13:
(
a' = sup (waybelow a') &
b' = sup (waybelow b') )
by WAYBEL_3:def 5;
Tsab' =
Tsup . a,
b
by A6
.=
a' "\/" b'
by WAYBEL_2:def 5
.=
sup ((waybelow a') "\/" (waybelow b'))
by A13, WAYBEL_2:4
;
then consider xy being
Element of
such that A14:
xy in (waybelow a') "\/" (waybelow b')
and A15:
u << xy
by A1, A11, WAYBEL_4:54;
consider x,
y being
Element of
such that A16:
xy = x "\/" y
and A17:
x in waybelow a'
and A18:
y in waybelow b'
by A14, A12;
reconsider H =
[:(wayabove x),(wayabove y):] as
Subset of
by A4, A3, YELLOW_3:def 2;
y << b'
by A18, WAYBEL_3:7;
then A19:
b' in wayabove y
;
Int G c= G
by TOPS_1:44;
then A20:
V c= G
by A9, XBOOLE_1:1;
reconsider wx =
wayabove x,
wy =
wayabove y as
Subset of
by A2, YELLOW_6:def 27;
wayabove y is
open
by A1, WAYBEL11:36;
then
wayabove y in the
topology of
L
by PRE_TOPC:def 5;
then A21:
wy is
open
by A2, A5, PRE_TOPC:def 5;
wayabove x is
open
by A1, WAYBEL11:36;
then
wayabove x in the
topology of
L
by PRE_TOPC:def 5;
then
wx is
open
by A2, A5, PRE_TOPC:def 5;
then
H is
open
by A21, BORSUK_1:46;
then A22:
H = Int H
by TOPS_1:55;
x << a'
by A17, WAYBEL_3:7;
then
a' in wayabove x
;
then
[a',b'] in H
by A19, ZFMISC_1:106;
then reconsider H =
H as
a_neighborhood of
ab by A6, A22, CONNSP_2:def 1;
take
H
;
Tsup .: H c= G
A23:
(
Tsup .: H = (wayabove x) "\/" (wayabove y) &
(wayabove x) "\/" (wayabove y) c= uparrow (x "\/" y) )
by Th12, WAYBEL_2:35;
uparrow (x "\/" y) c= wayabove u
by A15, A16, Th7;
then
Tsup .: H c= V
by A10, A23, XBOOLE_1:1;
hence
Tsup .: H c= G
by A20, XBOOLE_1:1;
verum
end;
hence
Tsup is continuous
by TMAP_1:49; verum