let X be non empty monotone-convergence TopSpace; :: thesis: for Y being T_0-TopSpace
for f being continuous Function of (Omega X),(Omega Y) holds f is directed-sups-preserving
let Y be T_0-TopSpace; :: thesis: for f being continuous Function of (Omega X),(Omega Y) holds f is directed-sups-preserving
let f be continuous Function of (Omega X),(Omega Y); :: thesis: f is directed-sups-preserving
let D be non empty directed Subset of (Omega X); :: according to YELLOW14:def 1 :: thesis: f preserves_sup_of D
assume A1:
ex_sup_of D, Omega X
; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of f .: D, Omega Y & "\/" (f .: D),(Omega Y) = f . ("\/" D,(Omega X)) )
A2:
TopStruct(# the carrier of X,the topology of X #) = TopStruct(# the carrier of (Omega X),the topology of (Omega X) #)
by Def2;
A3:
TopStruct(# the carrier of Y,the topology of Y #) = TopStruct(# the carrier of (Omega Y),the topology of (Omega Y) #)
by Def2;
ex a being Element of (Omega Y) st
( f .: D is_<=_than a & ( for b being Element of (Omega Y) st f .: D is_<=_than b holds
a <= b ) )
proof
take a =
f . (sup D);
:: thesis: ( f .: D is_<=_than a & ( for b being Element of (Omega Y) st f .: D is_<=_than b holds
a <= b ) )
D is_<=_than sup D
by A1, YELLOW_0:def 9;
hence
f .: D is_<=_than a
by YELLOW_2:16;
:: thesis: for b being Element of (Omega Y) st f .: D is_<=_than b holds
a <= b
let b be
Element of
(Omega Y);
:: thesis: ( f .: D is_<=_than b implies a <= b )
assume A4:
for
c being
Element of
(Omega Y) st
c in f .: D holds
c <= b
;
:: according to LATTICE3:def 9 :: thesis: a <= b
reconsider Z =
{b} as
Subset of
Y by Lm1;
for
G being
Subset of
Y st
G is
open &
a in G holds
Z meets G
proof
let G be
Subset of
Y;
:: thesis: ( G is open & a in G implies Z meets G )
assume that A5:
G is
open
and A6:
a in G
;
:: thesis: Z meets G
A7:
b in {b}
by TARSKI:def 1;
reconsider H =
G as
open Subset of
(Omega Y) by A3, A5, TOPS_3:76;
[#] (Omega Y) <> {}
;
then
f " H is
open
by TOPS_2:55;
then A8:
f " H is
open Subset of
X
by A2, TOPS_3:76;
sup D in f " H
by A6, FUNCT_2:46;
then
D meets f " H
by A8, Def4;
then consider c being
set such that A9:
c in D
and A10:
c in f " H
by XBOOLE_0:3;
reconsider c =
c as
Point of
(Omega X) by A9;
A11:
f . c <= b
by A4, A9, FUNCT_2:43;
f . c in H
by A10, FUNCT_2:46;
then
b in G
by A11, WAYBEL_0:def 20;
hence
Z meets G
by A7, XBOOLE_0:3;
:: thesis: verum
end;
then
a in Cl Z
by A3, PRE_TOPC:def 13;
hence
a <= b
by Def2;
:: thesis: verum
end;
hence A12:
ex_sup_of f .: D, Omega Y
by YELLOW_0:15; :: thesis: "\/" (f .: D),(Omega Y) = f . ("\/" D,(Omega X))
assume A13:
sup (f .: D) <> f . (sup D)
; :: thesis: contradiction
set V = (downarrow (sup (f .: D))) ` ;
[#] (Omega Y) <> {}
;
then A14:
f " ((downarrow (sup (f .: D))) ` ) is open
by TOPS_2:55;
reconsider fV = f " ((downarrow (sup (f .: D))) ` ) as Subset of X by A2;
reconsider fV = fV as open Subset of X by A2, A14, TOPS_3:76;
sup (f .: D) <= sup (f .: D)
;
then A15:
sup (f .: D) in downarrow (sup (f .: D))
by WAYBEL_0:17;
sup (f .: D) <= f . (sup D)
by A1, A12, WAYBEL17:15;
then
not f . (sup D) <= sup (f .: D)
by A13, ORDERS_2:25;
then
not f . (sup D) in downarrow (sup (f .: D))
by WAYBEL_0:17;
then
f . (sup D) in (downarrow (sup (f .: D))) `
by XBOOLE_0:def 5;
then
sup D in fV
by FUNCT_2:46;
then
D meets fV
by Def4;
then consider d being set such that
A16:
d in D
and
A17:
d in fV
by XBOOLE_0:3;
reconsider d = d as Element of (Omega X) by A16;
A18:
f . d in (downarrow (sup (f .: D))) `
by A17, FUNCT_2:46;
f . d <= sup (f .: D)
by A12, A16, FUNCT_2:43, YELLOW_4:1;
then
sup (f .: D) in (downarrow (sup (f .: D))) `
by A18, WAYBEL_0:def 20;
hence
contradiction
by A15, XBOOLE_0:def 5; :: thesis: verum