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 2;
A4:
the carrier of T = the carrier of L
by A2, YELLOW_6:def 24;
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 [:T,T:] holds Tsup is_continuous_at x
proof
reconsider Lc =
L as
complete continuous Scott TopLattice by A1;
let ab be
Point of
[:T,T:];
Tsup is_continuous_at ab
reconsider Tsab =
Tsup . ab as
Point of
T ;
consider a,
b being
Point of
T such that A6:
ab = [a,b]
by A3, DOMAIN_1:1;
reconsider a9 =
a,
b9 =
b as
Element of
L by A2, YELLOW_6:def 24;
set D1 =
waybelow a9;
set D2 =
waybelow b9;
set D =
(waybelow a9) "\/" (waybelow b9);
reconsider Tsab9 =
Tsab as
Element of
L by A2, YELLOW_6:def 24;
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
by CONNSP_2:def 1;
reconsider basab =
{ (wayabove q) where q is Element of L : q << Tsab9 } as
Basis of
Tsab9 by A1, WAYBEL11:44;
basab is
Basis of
Tsab
by A2, A5, Th21;
then consider V being
Subset of
T such that A8:
V in basab
and A9:
V c= Int G
by A7, YELLOW_8:def 1;
consider u being
Element of
L such that A10:
V = wayabove u
and A11:
u << Tsab9
by A8;
A12:
(waybelow a9) "\/" (waybelow b9) = { (x "\/" y) where x, y is Element of L : ( x in waybelow a9 & y in waybelow b9 ) }
by YELLOW_4:def 3;
Lc = L
;
then A13:
(
a9 = sup (waybelow a9) &
b9 = sup (waybelow b9) )
by WAYBEL_3:def 5;
Tsab9 =
Tsup . (
a,
b)
by A6
.=
a9 "\/" b9
by WAYBEL_2:def 5
.=
sup ((waybelow a9) "\/" (waybelow b9))
by A13, WAYBEL_2:4
;
then consider xy being
Element of
L such that A14:
xy in (waybelow a9) "\/" (waybelow b9)
and A15:
u << xy
by A1, A11, WAYBEL_4:53;
consider x,
y being
Element of
L such that A16:
xy = x "\/" y
and A17:
x in waybelow a9
and A18:
y in waybelow b9
by A14, A12;
reconsider H =
[:(wayabove x),(wayabove y):] as
Subset of
[:T,T:] by A4, A3, YELLOW_3:def 2;
y << b9
by A18, WAYBEL_3:7;
then A19:
b9 in wayabove y
;
Int G c= G
by TOPS_1:16;
then A20:
V c= G
by A9;
reconsider wx =
wayabove x,
wy =
wayabove y as
Subset of
T by A2, YELLOW_6:def 24;
wayabove y is
open
by A1, WAYBEL11:36;
then
wayabove y in the
topology of
L
by PRE_TOPC:def 2;
then A21:
wy is
open
by A2, A5, PRE_TOPC:def 2;
wayabove x is
open
by A1, WAYBEL11:36;
then
wayabove x in the
topology of
L
by PRE_TOPC:def 2;
then
wx is
open
by A2, A5, PRE_TOPC:def 2;
then
H is
open
by A21, BORSUK_1:6;
then A22:
H = Int H
by TOPS_1:23;
x << a9
by A17, WAYBEL_3:7;
then
a9 in wayabove x
;
then
[a9,b9] in H
by A19, ZFMISC_1:87;
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;
hence
Tsup .: H c= G
by A20;
verum
end;
hence
Tsup is continuous
by TMAP_1:44; verum