let X, Y be non empty TopSpace; for f being continuous Function of (Omega X),(Omega Y) holds f is monotone
let f be continuous Function of (Omega X),(Omega Y); f is monotone
let x, y be Element of (Omega X); WAYBEL_1:def 2 ( not x <= y or f . x <= f . y )
reconsider Z = {(f . y)} as Subset of Y by Lm1;
assume
x <= y
; f . x <= f . y
then consider A being Subset of X such that
A1:
A = {y}
and
A2:
x in Cl A
by Def2;
A3:
for G being Subset of Y st G is open & f . x in G holds
Z meets G
proof
the
carrier of
X = the
carrier of
(Omega X)
by Lm1;
then reconsider g =
f as
Function of
X,
Y by Lm1;
let G be
Subset of
Y;
( G is open & f . x in G implies Z meets G )
assume that A4:
G is
open
and A5:
f . x in G
;
Z meets G
A6:
x in g " G
by A5, FUNCT_2:38;
A7:
TopStruct(# the
carrier of
Y, the
topology of
Y #)
= TopStruct(# the
carrier of
(Omega Y), the
topology of
(Omega Y) #)
by Def2;
A8:
f . y in Z
by TARSKI:def 1;
TopStruct(# the
carrier of
X, the
topology of
X #)
= TopStruct(# the
carrier of
(Omega X), the
topology of
(Omega X) #)
by Def2;
then A9:
g is
continuous
by A7, YELLOW12:36;
[#] Y <> {}
;
then
g " G is
open
by A4, A9, TOPS_2:43;
then
A meets g " G
by A2, A6, PRE_TOPC:def 7;
then consider m being
object such that A10:
m in A /\ (g " G)
by XBOOLE_0:4;
m in A
by A10, XBOOLE_0:def 4;
then A11:
m = y
by A1, TARSKI:def 1;
m in g " G
by A10, XBOOLE_0:def 4;
then
f . y in G
by A11, FUNCT_2:38;
then
Z /\ G <> {} Y
by A8, XBOOLE_0:def 4;
hence
Z meets G
;
verum
end;
the carrier of Y = the carrier of (Omega Y)
by Lm1;
then
f . x in Cl Z
by A3, PRE_TOPC:def 7;
hence
f . x <= f . y
by Def2; verum