let S, T be complete Lawson TopLattice; for f being meet-preserving Function of S,T holds
( f is continuous iff ( f is directed-sups-preserving & ( for X being non empty Subset of S holds f preserves_inf_of X ) ) )
A1:
[#] T <> {}
;
set Ss = the Scott TopAugmentation of S;
set Ts = the Scott TopAugmentation of T;
set Sl = the correct lower TopAugmentation of S;
set Tl = the correct lower TopAugmentation of T;
A2:
S is TopAugmentation of S
by YELLOW_9:44;
A3:
T is TopAugmentation of T
by YELLOW_9:44;
A4:
S is Refinement of the Scott TopAugmentation of S, the correct lower TopAugmentation of S
by A2, WAYBEL19:29;
A5:
T is Refinement of the Scott TopAugmentation of T, the correct lower TopAugmentation of T
by A3, WAYBEL19:29;
A6:
T is TopAugmentation of the Scott TopAugmentation of T
by YELLOW_9:45;
A7:
S is TopAugmentation of the Scott TopAugmentation of S
by YELLOW_9:45;
A8:
RelStr(# the carrier of the Scott TopAugmentation of S, the InternalRel of the Scott TopAugmentation of S #) = RelStr(# the carrier of S, the InternalRel of S #)
by YELLOW_9:def 4;
A9:
RelStr(# the carrier of the correct lower TopAugmentation of S, the InternalRel of the correct lower TopAugmentation of S #) = RelStr(# the carrier of S, the InternalRel of S #)
by YELLOW_9:def 4;
A10:
RelStr(# the carrier of the Scott TopAugmentation of T, the InternalRel of the Scott TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #)
by YELLOW_9:def 4;
A11:
RelStr(# the carrier of the correct lower TopAugmentation of T, the InternalRel of the correct lower TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #)
by YELLOW_9:def 4;
let f be meet-preserving Function of S,T; ( f is continuous iff ( f is directed-sups-preserving & ( for X being non empty Subset of S holds f preserves_inf_of X ) ) )
reconsider g = f as Function of the correct lower TopAugmentation of S, the correct lower TopAugmentation of T by A9, A11;
reconsider h = f as Function of the Scott TopAugmentation of S, the Scott TopAugmentation of T by A8, A10;
A12:
[#] the Scott TopAugmentation of T <> {}
;
hereby ( f is directed-sups-preserving & ( for X being non empty Subset of S holds f preserves_inf_of X ) implies f is continuous )
assume A13:
f is
continuous
;
( f is directed-sups-preserving & ( for X being non empty Subset of S holds f preserves_inf_of X ) )now for P being Subset of the Scott TopAugmentation of T st P is open holds
h " P is open let P be
Subset of the
Scott TopAugmentation of
T;
( P is open implies h " P is open )reconsider A =
P as
Subset of the
Scott TopAugmentation of
T ;
reconsider C =
A as
Subset of
T by A10;
assume A14:
P is
open
;
h " P is open then
C is
open
by A6, WAYBEL19:37;
then A15:
f " C is
open
by A1, A13, TOPS_2:43;
A is
upper
by A14, WAYBEL11:def 4;
then
h " A is
upper
by A8, A10, WAYBEL17:2, WAYBEL_9:1;
then
f " C is
upper
by A8, WAYBEL_0:25;
hence
h " P is
open
by A7, A15, WAYBEL19:41;
verum end; then
h is
continuous
by A12, TOPS_2:43;
hence
f is
directed-sups-preserving
by A8, A10, Th6;
for X being non empty Subset of S holds f preserves_inf_of X
for
X being non
empty filtered Subset of
S holds
f preserves_inf_of X
proof
let F be non
empty filtered Subset of
S;
f preserves_inf_of F
assume
ex_inf_of F,
S
;
WAYBEL_0:def 30 ( ex_inf_of f .: F,T & "/\" ((f .: F),T) = f . ("/\" (F,S)) )
thus
ex_inf_of f .: F,
T
by YELLOW_0:17;
"/\" ((f .: F),T) = f . ("/\" (F,S))
{(inf F)} = Lim (F opp+id)
by WAYBEL19:43;
then
Im (
f,
(inf F))
c= Lim (f * (F opp+id))
by A13, Th24;
then
{(f . (inf F))} c= Lim (f * (F opp+id))
by SETWISEO:8;
then A16:
f . (inf F) in Lim (f * (F opp+id))
by ZFMISC_1:31;
reconsider G =
f .: F as non
empty filtered Subset of
T by WAYBEL20:24;
A17:
rng the
mapping of
(f * (F opp+id)) =
rng (f * the mapping of (F opp+id))
by WAYBEL_9:def 8
.=
rng (f * (id F))
by WAYBEL19:27
.=
rng (f | F)
by RELAT_1:65
.=
G
by RELAT_1:115
;
Lim (f * (F opp+id)) =
{(inf (f * (F opp+id)))}
by Th44
.=
{(Inf )}
by WAYBEL_9:def 2
.=
{(inf G)}
by A17, YELLOW_2:def 6
;
hence
"/\" (
(f .: F),
T)
= f . ("/\" (F,S))
by A16, TARSKI:def 1;
verum
end; hence
for
X being non
empty Subset of
S holds
f preserves_inf_of X
by Th4;
verum
end;
assume
f is directed-sups-preserving
; ( ex X being non empty Subset of S st not f preserves_inf_of X or f is continuous )
then A18:
h is directed-sups-preserving
by A8, A10, Th6;
assume
for X being non empty Subset of S holds f preserves_inf_of X
; f is continuous
then
for X being non empty Subset of the correct lower TopAugmentation of S holds g preserves_inf_of X
by A9, A11, WAYBEL_0:65;
then
g is continuous
by WAYBEL19:8;
hence
f is continuous
by A4, A5, A18, WAYBEL19:24; verum