let X be non empty TopSpace; for Y being T_0-TopSpace
for N being net of ContMaps (X,(Omega Y)) st ( for x being Point of X holds ex_sup_of commute (N,x,(Omega Y)) ) holds
ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X
let Y be T_0-TopSpace; for N being net of ContMaps (X,(Omega Y)) st ( for x being Point of X holds ex_sup_of commute (N,x,(Omega Y)) ) holds
ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X
let N be net of ContMaps (X,(Omega Y)); ( ( for x being Point of X holds ex_sup_of commute (N,x,(Omega Y)) ) implies ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X )
assume A1:
for x being Point of X holds ex_sup_of commute (N,x,(Omega Y))
; ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X
deffunc H1( Element of X) -> Element of the carrier of (Omega Y) = sup (commute (N,$1,(Omega Y)));
set n = the mapping of N;
set L = (Omega Y) |^ the carrier of X;
consider f being Function of the carrier of X, the carrier of (Omega Y) such that
A2:
for u being Element of X holds f . u = H1(u)
from FUNCT_2:sch 4();
reconsider a = f as Element of ((Omega Y) |^ the carrier of X) by WAYBEL24:19;
ex a being Element of ((Omega Y) |^ the carrier of X) st
( rng the mapping of N is_<=_than a & ( for b being Element of ((Omega Y) |^ the carrier of X) st rng the mapping of N is_<=_than b holds
a <= b ) )
proof
take
a
;
( rng the mapping of N is_<=_than a & ( for b being Element of ((Omega Y) |^ the carrier of X) st rng the mapping of N is_<=_than b holds
a <= b ) )
A3:
dom the
mapping of
N = the
carrier of
N
by FUNCT_2:def 1;
A4:
(Omega Y) |^ the
carrier of
X = product ( the carrier of X --> (Omega Y))
by YELLOW_1:def 5;
thus
rng the
mapping of
N is_<=_than a
for b being Element of ((Omega Y) |^ the carrier of X) st rng the mapping of N is_<=_than b holds
a <= bproof
let k be
Element of
((Omega Y) |^ the carrier of X);
LATTICE3:def 9 ( not k in rng the mapping of N or k <= a )
reconsider k9 =
k,
a9 =
a as
Element of
(product ( the carrier of X --> (Omega Y))) by YELLOW_1:def 5;
assume
k in rng the
mapping of
N
;
k <= a
then consider i being
object such that A5:
i in dom the
mapping of
N
and A6:
k = the
mapping of
N . i
by FUNCT_1:def 3;
reconsider i =
i as
Point of
N by A5;
for
u being
Element of
X holds
k9 . u <= a9 . u
proof
let u be
Element of
X;
k9 . u <= a9 . u
ex_sup_of commute (
N,
u,
(Omega Y))
by A1;
then A8:
ex_sup_of rng the
mapping of
(commute (N,u,(Omega Y))),
Omega Y
;
A9:
k9 . u = the
mapping of
(commute (N,u,(Omega Y))) . i
by A6, Th24;
dom the
mapping of
(commute (N,u,(Omega Y))) = the
carrier of
N
by A3, Lm6;
then A10:
k9 . u in rng the
mapping of
(commute (N,u,(Omega Y)))
by A9, FUNCT_1:def 3;
a9 . u =
sup (commute (N,u,(Omega Y)))
by A2
.=
Sup
by WAYBEL_2:def 1
.=
sup (rng the mapping of (commute (N,u,(Omega Y))))
;
hence
k9 . u <= a9 . u
by A8, A10, YELLOW_4:1;
verum
end;
hence
k <= a
by A4, WAYBEL_3:28;
verum
end;
let b be
Element of
((Omega Y) |^ the carrier of X);
( rng the mapping of N is_<=_than b implies a <= b )
assume A11:
for
k being
Element of
((Omega Y) |^ the carrier of X) st
k in rng the
mapping of
N holds
k <= b
;
LATTICE3:def 9 a <= b
reconsider a9 =
a,
b9 =
b as
Element of
(product ( the carrier of X --> (Omega Y))) by YELLOW_1:def 5;
for
u being
Element of
X holds
a9 . u <= b9 . u
proof
let u be
Element of
X;
a9 . u <= b9 . u
ex_sup_of commute (
N,
u,
(Omega Y))
by A1;
then A12:
ex_sup_of rng the
mapping of
(commute (N,u,(Omega Y))),
Omega Y
;
A13:
Omega Y = ( the carrier of X --> (Omega Y)) . u
;
A14:
rng the
mapping of
(commute (N,u,(Omega Y))) is_<=_than b . u
proof
let s be
Element of
(Omega Y);
LATTICE3:def 9 ( not s in rng the mapping of (commute (N,u,(Omega Y))) or s <= b . u )
assume
s in rng the
mapping of
(commute (N,u,(Omega Y)))
;
s <= b . u
then consider i being
object such that A15:
i in dom the
mapping of
(commute (N,u,(Omega Y)))
and A16:
the
mapping of
(commute (N,u,(Omega Y))) . i = s
by FUNCT_1:def 3;
reconsider i =
i as
Point of
N by A3, A15, Lm6;
the
mapping of
N . i is
Function of
X,
(Omega Y)
by WAYBEL24:21;
then reconsider k = the
mapping of
N . i as
Element of
((Omega Y) |^ the carrier of X) by WAYBEL24:19;
reconsider k9 =
k as
Element of
(product ( the carrier of X --> (Omega Y))) by YELLOW_1:def 5;
the
mapping of
N . i in rng the
mapping of
N
by A3, FUNCT_1:def 3;
then
k <= b
by A11;
then A17:
k9 <= b9
by YELLOW_1:def 5;
s = ( the mapping of N . i) . u
by A16, Th24;
hence
s <= b . u
by A13, A17, WAYBEL_3:28;
verum
end;
a9 . u =
sup (commute (N,u,(Omega Y)))
by A2
.=
Sup
by WAYBEL_2:def 1
.=
sup (rng the mapping of (commute (N,u,(Omega Y))))
;
hence
a9 . u <= b9 . u
by A12, A14, YELLOW_0:30;
verum
end;
hence
a <= b
by A4, WAYBEL_3:28;
verum
end;
hence
ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X
by YELLOW_0:15; verum