let X be non empty TopSpace; for Y being monotone-convergence T_0-TopSpace
for N being net of ContMaps (X,(Omega Y))
for x being Point of X
for f being Function of X,(Omega Y) st ( for a being Point of X holds commute (N,a,(Omega Y)) is eventually-directed ) & f = "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) holds
f . x = sup (commute (N,x,(Omega Y)))
let Y be monotone-convergence T_0-TopSpace; for N being net of ContMaps (X,(Omega Y))
for x being Point of X
for f being Function of X,(Omega Y) st ( for a being Point of X holds commute (N,a,(Omega Y)) is eventually-directed ) & f = "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) holds
f . x = sup (commute (N,x,(Omega Y)))
let N be net of ContMaps (X,(Omega Y)); for x being Point of X
for f being Function of X,(Omega Y) st ( for a being Point of X holds commute (N,a,(Omega Y)) is eventually-directed ) & f = "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) holds
f . x = sup (commute (N,x,(Omega Y)))
let x be Point of X; for f being Function of X,(Omega Y) st ( for a being Point of X holds commute (N,a,(Omega Y)) is eventually-directed ) & f = "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) holds
f . x = sup (commute (N,x,(Omega Y)))
let f be Function of X,(Omega Y); ( ( for a being Point of X holds commute (N,a,(Omega Y)) is eventually-directed ) & f = "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) implies f . x = sup (commute (N,x,(Omega Y))) )
assume that
A1:
for a being Point of X holds commute (N,a,(Omega Y)) is eventually-directed
and
A2:
f = "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X))
; f . x = sup (commute (N,x,(Omega Y)))
set n = the mapping of N;
set m = the mapping of (commute (N,x,(Omega Y)));
set L = (Omega Y) |^ the carrier of X;
A3:
for x being Point of X holds ex_sup_of commute (N,x,(Omega Y))
then A4:
ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X
by Th26;
A5:
dom the mapping of N = the carrier of N
by FUNCT_2:def 1;
then A6:
dom the mapping of (commute (N,x,(Omega Y))) = the carrier of N
by Lm6;
A7:
for a being Element of (Omega Y) st rng the mapping of (commute (N,x,(Omega Y))) is_<=_than a holds
f . x <= a
proof
let a be
Element of
(Omega Y);
( rng the mapping of (commute (N,x,(Omega Y))) is_<=_than a implies f . x <= a )
defpred S1[
set ,
set ]
means ( ( $1
= x implies $2
= a ) & ( $1
<> x implies ex
u being
Element of
X st
( $1
= u & $2
= sup (commute (N,u,(Omega Y))) ) ) );
A8:
Omega Y = ( the carrier of X --> (Omega Y)) . x
;
A9:
for
e being
Element of
X ex
u being
Element of
(Omega Y) st
S1[
e,
u]
consider t being
Function of the
carrier of
X, the
carrier of
(Omega Y) such that A11:
for
u being
Element of
X holds
S1[
u,
t . u]
from FUNCT_2:sch 3(A9);
reconsider t =
t as
Function of
X,
(Omega Y) ;
reconsider tt =
t as
Element of
((Omega Y) |^ the carrier of X) by WAYBEL24:19;
reconsider p =
"\/" (
(rng the mapping of N),
((Omega Y) |^ the carrier of X)),
q =
tt as
Element of
(product ( the carrier of X --> (Omega Y))) by YELLOW_1:def 5;
assume A12:
for
e being
Element of
(Omega Y) st
e in rng the
mapping of
(commute (N,x,(Omega Y))) holds
e <= a
;
LATTICE3:def 9 f . x <= a
tt is_>=_than rng the
mapping of
N
proof
let s be
Element of
((Omega Y) |^ the carrier of X);
LATTICE3:def 9 ( not s in rng the mapping of N or s <= tt )
reconsider ss =
s as
Function of
X,
(Omega Y) by WAYBEL24:19;
reconsider s9 =
s,
t9 =
tt as
Element of
(product ( the carrier of X --> (Omega Y))) by YELLOW_1:def 5;
assume
s in rng the
mapping of
N
;
s <= tt
then consider i being
object such that A13:
i in dom the
mapping of
N
and A14:
s = the
mapping of
N . i
by FUNCT_1:def 3;
reconsider i =
i as
Point of
N by A13;
A15:
for
j being
Element of
X holds
s9 . j <= t9 . j
proof
let j be
Element of
X;
s9 . j <= t9 . j
A17:
ss . j = the
mapping of
(commute (N,j,(Omega Y))) . i
by A14, Th24;
per cases
( j <> x or j = x )
;
suppose
j <> x
;
s9 . j <= t9 . jthen
ex
u being
Element of
X st
(
j = u &
t . j = sup (commute (N,u,(Omega Y))) )
by A11;
then A18:
t9 . j =
Sup
by WAYBEL_2:def 1
.=
sup (rng the mapping of (commute (N,j,(Omega Y))))
;
commute (
N,
j,
(Omega Y)) is
eventually-directed
by A1;
then
ex_sup_of commute (
N,
j,
(Omega Y))
by Th31;
then A19:
ex_sup_of rng the
mapping of
(commute (N,j,(Omega Y))),
Omega Y
;
i in dom the
mapping of
(commute (N,j,(Omega Y)))
by A13, Lm6;
then
ss . j in rng the
mapping of
(commute (N,j,(Omega Y)))
by A17, FUNCT_1:def 3;
hence
s9 . j <= t9 . j
by A18, A19, YELLOW_4:1;
verum end; suppose A20:
j = x
;
s9 . j <= t9 . jA21:
the
mapping of
(commute (N,x,(Omega Y))) . i in rng the
mapping of
(commute (N,x,(Omega Y)))
by A6, FUNCT_1:def 3;
ss . x = the
mapping of
(commute (N,x,(Omega Y))) . i
by A14, Th24;
then
ss . x <= a
by A12, A21;
hence
s9 . j <= t9 . j
by A11, A20;
verum end;
end;
(Omega Y) |^ the
carrier of
X = product ( the carrier of X --> (Omega Y))
by YELLOW_1:def 5;
hence
s <= tt
by A15, WAYBEL_3:28;
verum
end;
then
"\/" (
(rng the mapping of N),
((Omega Y) |^ the carrier of X))
<= tt
by A4, YELLOW_0:30;
then A22:
p <= q
by YELLOW_1:def 5;
tt . x = a
by A11;
hence
f . x <= a
by A2, A8, A22, WAYBEL_3:28;
verum
end;
rng the mapping of (commute (N,x,(Omega Y))) is_<=_than f . x
proof
let w be
Element of
(Omega Y);
LATTICE3:def 9 ( not w in rng the mapping of (commute (N,x,(Omega Y))) or w <= f . x )
assume
w in rng the
mapping of
(commute (N,x,(Omega Y)))
;
w <= f . x
then consider i being
object such that A23:
i in dom the
mapping of
(commute (N,x,(Omega Y)))
and A24:
the
mapping of
(commute (N,x,(Omega Y))) . i = w
by FUNCT_1:def 3;
reconsider i =
i as
Point of
N by A5, A23, Lm6;
reconsider g = the
mapping of
N . i as
Function of
X,
(Omega Y) by Lm5;
g in rng the
mapping of
N
by A5, FUNCT_1:def 3;
then
g <= f
by A2, A3, Th26, Th40;
then
ex
a,
b being
Element of
(Omega Y) st
(
a = g . x &
b = f . x &
a <= b )
;
hence
w <= f . x
by A24, Th24;
verum
end;
hence f . x =
Sup
by A7, YELLOW_0:30
.=
sup (commute (N,x,(Omega Y)))
by WAYBEL_2:def 1
;
verum