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