let X be non empty TopSpace; 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; 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)); ( ( 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
; "\/" ((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;
reconsider fo = "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) as Function of X,(Omega Y) by WAYBEL24:19;
A2:
TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (Omega Y), the topology of (Omega Y) #)
by Def2;
then reconsider f = fo as Function of X,Y ;
A3:
dom the mapping of N = the carrier of N
by FUNCT_2:def 1;
A4:
for V being Subset of Y st V is open holds
f " V is open
proof
let V be
Subset of
Y;
( V is open implies f " V is open )
assume A5:
V is
open
;
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
object 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
object ;
( 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 ) } )
A6:
dom f = the
carrier of
X
by FUNCT_2:def 1;
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 ) } )
( 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
A7:
the
mapping of
N in Funcs ( the
carrier of
N,
(Funcs ( the carrier of X, the carrier of Y)))
by Lm4;
assume A8:
x in f " V
;
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 A9:
f . x in V
by FUNCT_2:38;
reconsider x =
x as
Point of
X by A8;
set NET =
commute (
N,
x,
(Omega Y));
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, A9, Def4;
then consider k being
object such that A10:
k in W
and A11:
k in V
by XBOOLE_0:3;
consider i being
object such that A12:
i in dom (netmap ((commute (N,x,(Omega Y))),(Omega Y)))
and A13:
k = (netmap ((commute (N,x,(Omega Y))),(Omega Y))) . i
by A10, FUNCT_1:def 3;
ContMaps (
X,
(Omega Y)) is
SubRelStr of
(Omega Y) |^ the
carrier of
X
by WAYBEL24:def 3;
then A14:
the
carrier of
(ContMaps (X,(Omega Y))) c= the
carrier of
((Omega Y) |^ the carrier of X)
by YELLOW_0:def 13;
then
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;
then reconsider i =
i as
Element of
N by A12;
reconsider g =
N . i as
Function of
X,
(Omega Y) by WAYBEL24:21;
A15:
dom g = the
carrier of
X
by FUNCT_2:def 1;
A16:
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 ) }
;
(netmap ((commute (N,x,(Omega Y))),(Omega Y))) . i =
((commute the mapping of N) . x) . i
by A14, Def3
.=
( the mapping of N . i) . x
by A7, FUNCT_6:56
;
then
x in g " V
by A11, A13, A15, FUNCT_1:def 7;
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;
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 ) }
;
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 7;
A24:
for
x being
Point of
X holds
ex_sup_of commute (
N,
x,
(Omega Y))
reconsider x =
x as
Element of
X by A17, A19;
the
mapping of
N . i in rng the
mapping of
N
by A3, FUNCT_1:def 3;
then
g <= fo
by A21, A24, Th26, Th40;
then
ex
a,
b being
Element of
(Omega Y) st
(
a = g . x &
b = fo . x &
a <= b )
;
then consider O being
Subset of
Y such that A25:
O = {(f . x)}
and A26:
g . x in Cl O
by Def2;
V meets O
by A5, A23, A26, PRE_TOPC:def 7;
then consider w being
object such that A27:
w in V /\ O
by XBOOLE_0:4;
w in O
by A27, XBOOLE_0:def 4;
then A28:
w = f . x
by A25, TARSKI:def 1;
w in V
by A27, XBOOLE_0:def 4;
hence
x in f " V
by A6, A28, FUNCT_1:def 7;
verum
end;
then A29:
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;
TOPS_2:def 1 ( not P in M or P is open )
assume
P in M
;
P is open
then consider A being
Subset of
X such that A30:
P = A
and A31:
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 A32:
g = N . i
and A33:
A = g " V
by A31;
consider g9 being
Function of
X,
(Omega Y) such that A34:
g = g9
and A35:
g9 is
continuous
by A32, WAYBEL24:def 3;
TopStruct(# the
carrier of
X, the
topology of
X #)
= TopStruct(# the
carrier of
X, the
topology of
X #)
;
then reconsider g99 =
g9 as
continuous Function of
X,
Y by A2, A35, YELLOW12:36;
[#] Y <> {}
;
then
g99 " V is
open
by A5, TOPS_2:43;
hence
P is
open
by A30, A33, A34;
verum
end;
hence
f " V is
open
by A29, TOPS_2:19;
verum
end;
[#] Y <> {}
;
hence
"\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) is continuous Function of X,Y
by A4, TOPS_2:43; verum