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