let X be non empty TopSpace; :: thesis: for Y being monotone-convergence T_0-TopSpace
for N being net of ContMaps X,(Omega Y) st ( for x being Point of X holds commute N,x,(Omega Y) is eventually-directed ) holds
"\/" (rng the mapping of N),((Omega Y) |^ the carrier of X) is continuous Function of X,Y
let Y be monotone-convergence T_0-TopSpace; :: thesis: for N being net of ContMaps X,(Omega Y) st ( for x being Point of X holds commute N,x,(Omega Y) is eventually-directed ) holds
"\/" (rng the mapping of N),((Omega Y) |^ the carrier of X) is continuous Function of X,Y
let N be net of ContMaps X,(Omega Y); :: thesis: ( ( for x being Point of X holds commute N,x,(Omega Y) is eventually-directed ) implies "\/" (rng the mapping of N),((Omega Y) |^ the carrier of X) is continuous Function of X,Y )
assume A1:
for x being Point of X holds commute N,x,(Omega Y) is eventually-directed
; :: thesis: "\/" (rng the mapping of N),((Omega Y) |^ the carrier of X) is continuous Function of X,Y
set m = the mapping of N;
set L = (Omega Y) |^ the carrier of X;
A2:
TopStruct(# the carrier of Y,the topology of Y #) = TopStruct(# the carrier of (Omega Y),the topology of (Omega Y) #)
by Def2;
reconsider fo = "\/" (rng the mapping of N),((Omega Y) |^ the carrier of X) as Function of X,(Omega Y) by WAYBEL24:19;
reconsider f = fo as Function of X,Y by A2;
A3:
dom the mapping of N = the carrier of N
by FUNCT_2:def 1;
A4:
[#] Y <> {}
;
for V being Subset of Y st V is open holds
f " V is open
proof
let V be
Subset of
Y;
:: thesis: ( V is open implies f " V is open )
assume A5:
V is
open
;
:: thesis: f " V is open
set M =
{ A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st
( g = N . i & A = g " V ) } ;
for
x being
set holds
(
x in f " V iff
x in union { A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st
( g = N . i & A = g " V ) } )
proof
let x be
set ;
:: thesis: ( x in f " V iff x in union { A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st
( g = N . i & A = g " V ) } )
thus
(
x in f " V implies
x in union { A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st
( g = N . i & A = g " V ) } )
:: thesis: ( x in union { A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st
( g = N . i & A = g " V ) } implies x in f " V )proof
assume A6:
x in f " V
;
:: thesis: x in union { A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st
( g = N . i & A = g " V ) }
then A7:
f . x in V
by FUNCT_2:46;
reconsider x =
x as
Point of
X by A6;
set NET =
commute N,
x,
(Omega Y);
A8:
the
mapping of
N in Funcs the
carrier of
N,
(Funcs the carrier of X,the carrier of Y)
by Lm4;
ContMaps X,
(Omega Y) is
SubRelStr of
(Omega Y) |^ the
carrier of
X
by WAYBEL24:def 3;
then A9:
the
carrier of
(ContMaps X,(Omega Y)) c= the
carrier of
((Omega Y) |^ the carrier of X)
by YELLOW_0:def 13;
then A10:
RelStr(# the
carrier of
(commute N,x,(Omega Y)),the
InternalRel of
(commute N,x,(Omega Y)) #)
= RelStr(# the
carrier of
N,the
InternalRel of
N #)
by Def3;
commute N,
x,
(Omega Y) is
eventually-directed
by A1;
then reconsider W =
rng (netmap (commute N,x,(Omega Y)),(Omega Y)) as non
empty directed Subset of
(Omega Y) by WAYBEL_2:18;
f . x =
sup (commute N,x,(Omega Y))
by A1, Th41
.=
Sup
by WAYBEL_2:def 1
.=
sup W
;
then
W meets V
by A5, A7, Def4;
then consider k being
set such that A11:
k in W
and A12:
k in V
by XBOOLE_0:3;
consider i being
set such that A13:
i in dom (netmap (commute N,x,(Omega Y)),(Omega Y))
and A14:
k = (netmap (commute N,x,(Omega Y)),(Omega Y)) . i
by A11, FUNCT_1:def 5;
reconsider i =
i as
Element of
N by A10, A13;
A15:
(netmap (commute N,x,(Omega Y)),(Omega Y)) . i =
((commute the mapping of N) . x) . i
by A9, Def3
.=
(the mapping of N . i) . x
by A8, FUNCT_6:86
;
reconsider g =
N . i as
Function of
X,
(Omega Y) by WAYBEL24:21;
dom g = the
carrier of
X
by FUNCT_2:def 1;
then A16:
x in g " V
by A12, A14, A15, FUNCT_1:def 13;
g " V in { A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st
( g = N . i & A = g " V ) }
;
hence
x in union { A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st
( g = N . i & A = g " V ) }
by A16, TARSKI:def 4;
:: thesis: verum
end;
assume
x in union { A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st
( g = N . i & A = g " V ) }
;
:: thesis: x in f " V
then consider Z being
set such that A17:
x in Z
and A18:
Z in { A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st
( g = N . i & A = g " V ) }
by TARSKI:def 4;
consider A being
Subset of
X such that A19:
Z = A
and A20:
ex
i being
Element of
N ex
g being
Function of
X,
(Omega Y) st
(
g = N . i &
A = g " V )
by A18;
consider i being
Element of
N,
g being
Function of
X,
(Omega Y) such that A21:
g = N . i
and A22:
A = g " V
by A20;
A23:
g . x in V
by A17, A19, A22, FUNCT_1:def 13;
A24:
dom f = the
carrier of
X
by FUNCT_2:def 1;
reconsider x =
x as
Element of
X by A17, A19;
for
x being
Point of
X holds
ex_sup_of commute N,
x,
(Omega Y)
then A25:
ex_sup_of rng the
mapping of
N,
(Omega Y) |^ the
carrier of
X
by Th26;
the
mapping of
N . i in rng the
mapping of
N
by A3, FUNCT_1:def 5;
then
g <= fo
by A21, A25, Th40;
then
ex
a,
b being
Element of
(Omega Y) st
(
a = g . x &
b = fo . x &
a <= b )
by YELLOW_2:def 1;
then consider O being
Subset of
Y such that A26:
O = {(f . x)}
and A27:
g . x in Cl O
by Def2;
V meets O
by A5, A23, A27, PRE_TOPC:def 13;
then consider w being
set such that A28:
w in V /\ O
by XBOOLE_0:4;
A29:
(
w in V &
w in O )
by A28, XBOOLE_0:def 4;
then
w = f . x
by A26, TARSKI:def 1;
hence
x in f " V
by A24, A29, FUNCT_1:def 13;
:: thesis: verum
end;
then A30:
f " V = union { A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st
( g = N . i & A = g " V ) }
by TARSKI:2;
{ A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st
( g = N . i & A = g " V ) } c= bool the
carrier of
X
then reconsider M =
{ A where A is Subset of X : ex i being Element of N ex g being Function of X,(Omega Y) st
( g = N . i & A = g " V ) } as
Subset-Family of
X ;
reconsider M =
M as
Subset-Family of
X ;
M is
open
proof
let P be
Subset of
X;
:: according to TOPS_2:def 1 :: thesis: ( not P in M or P is open )
assume
P in M
;
:: thesis: P is open
then consider A being
Subset of
X such that A31:
P = A
and A32:
ex
i being
Element of
N ex
g being
Function of
X,
(Omega Y) st
(
g = N . i &
A = g " V )
;
consider i being
Element of
N,
g being
Function of
X,
(Omega Y) such that A33:
g = N . i
and A34:
A = g " V
by A32;
A35:
TopStruct(# the
carrier of
X,the
topology of
X #)
= TopStruct(# the
carrier of
X,the
topology of
X #)
;
consider g' being
Function of
X,
(Omega Y) such that A36:
(
g = g' &
g' is
continuous )
by A33, WAYBEL24:def 3;
reconsider g'' =
g' as
continuous Function of
X,
Y by A2, A35, A36, YELLOW12:36;
[#] Y <> {}
;
then
g'' " V is
open
by A5, TOPS_2:55;
hence
P is
open
by A31, A34, A36;
:: thesis: verum
end;
hence
f " V is
open
by A30, TOPS_2:26;
:: thesis: verum
end;
hence
"\/" (rng the mapping of N),((Omega Y) |^ the carrier of X) is continuous Function of X,Y
by A4, TOPS_2:55; :: thesis: verum