let X be non empty TopSpace; :: thesis: 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; :: thesis: 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); :: thesis: 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; :: thesis: 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); :: thesis: ( ( 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)
; :: thesis: 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:
dom the mapping of N = the carrier of N
by FUNCT_2:def 1;
then A4:
dom the mapping of (commute N,x,(Omega Y)) = the carrier of N
by Lm6;
for x being Point of X holds ex_sup_of commute N,x,(Omega Y)
then A5:
ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X
by Th26;
A6:
rng the mapping of (commute N,x,(Omega Y)) is_<=_than f . x
proof
let w be
Element of
(Omega Y);
:: according to LATTICE3:def 9 :: thesis: ( 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))
;
:: thesis: w <= f . x
then consider i being
set such that A7:
i in dom the
mapping of
(commute N,x,(Omega Y))
and A8:
the
mapping of
(commute N,x,(Omega Y)) . i = w
by FUNCT_1:def 5;
reconsider i =
i as
Point of
N by A3, A7, Lm6;
reconsider g = the
mapping of
N . i as
Function of
X,
(Omega Y) by Lm5;
g in rng the
mapping of
N
by A3, FUNCT_1:def 5;
then
g <= f
by A2, A5, Th40;
then
ex
a,
b being
Element of
(Omega Y) st
(
a = g . x &
b = f . x &
a <= b )
by YELLOW_2:def 1;
hence
w <= f . x
by A8, Th24;
:: thesis: verum
end;
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);
:: thesis: ( rng the mapping of (commute N,x,(Omega Y)) is_<=_than a implies f . x <= a )
assume A9:
for
e being
Element of
(Omega Y) st
e in rng the
mapping of
(commute N,x,(Omega Y)) holds
e <= a
;
:: according to LATTICE3:def 9 :: thesis: 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)) ) ) );
A10:
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 A12:
for
u being
Element of
X holds
S1[
u,
t . u]
from FUNCT_2:sch 3(A10);
reconsider t =
t as
Function of
X,
(Omega Y) ;
reconsider tt =
t as
Element of
((Omega Y) |^ the carrier of X) by WAYBEL24:19;
tt is_>=_than rng the
mapping of
N
proof
let s be
Element of
((Omega Y) |^ the carrier of X);
:: according to LATTICE3:def 9 :: thesis: ( not s in rng the mapping of N or s <= tt )
assume
s in rng the
mapping of
N
;
:: thesis: s <= tt
then consider i being
set such that A13:
i in dom the
mapping of
N
and A14:
s = the
mapping of
N . i
by FUNCT_1:def 5;
reconsider i =
i as
Point of
N by A13;
reconsider ss =
s as
Function of
X,
(Omega Y) by WAYBEL24:19;
A15:
(Omega Y) |^ the
carrier of
X = product (the carrier of X --> (Omega Y))
by YELLOW_1:def 5;
reconsider s' =
s,
t' =
tt as
Element of
(product (the carrier of X --> (Omega Y))) by YELLOW_1:def 5;
for
j being
Element of
X holds
s' . j <= t' . j
proof
let j be
Element of
X;
:: thesis: s' . j <= t' . j
A16:
ss . j = the
mapping of
(commute N,j,(Omega Y)) . i
by A14, Th24;
A17:
Omega Y = (the carrier of X --> (Omega Y)) . j
by FUNCOP_1:13;
per cases
( j <> x or j = x )
;
suppose
j <> x
;
:: thesis: s' . j <= t' . jthen
ex
u being
Element of
X st
(
j = u &
t . j = sup (commute N,u,(Omega Y)) )
by A12;
then A18:
t' . 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
by WAYBEL_9:def 3;
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 A16, FUNCT_1:def 5;
hence
s' . j <= t' . j
by A17, A18, A19, YELLOW_4:1;
:: thesis: verum end; suppose A20:
j = x
;
:: thesis: s' . j <= t' . jA21:
ss . x = the
mapping of
(commute N,x,(Omega Y)) . i
by A14, Th24;
the
mapping of
(commute N,x,(Omega Y)) . i in rng the
mapping of
(commute N,x,(Omega Y))
by A4, FUNCT_1:def 5;
then
ss . x <= a
by A9, A21;
hence
s' . j <= t' . j
by A12, A17, A20;
:: thesis: verum end;
end;
hence
s <= tt
by A15, WAYBEL_3:28;
:: thesis: verum
end;
then A22:
"\/" (rng the mapping of N),
((Omega Y) |^ the carrier of X) <= tt
by A5, YELLOW_0:30;
A23:
tt . x = a
by A12;
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;
A24:
Omega Y = (the carrier of X --> (Omega Y)) . x
by FUNCOP_1:13;
p <= q
by A22, YELLOW_1:def 5;
hence
f . x <= a
by A2, A23, A24, WAYBEL_3:28;
:: thesis: verum
end;
hence f . x =
Sup
by A6, YELLOW_0:30
.=
sup (commute N,x,(Omega Y))
by WAYBEL_2:def 1
;
:: thesis: verum