let X be RealBanachSpace; for Y being RealNormSpace
for T being Subset of (R_NormSpace_of_BoundedLinearOperators X,Y) st ( for x being Point of X ex K being real number st
( 0 <= K & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators X,Y) st f in T holds
||.(f . x).|| <= K ) ) ) holds
ex L being real number st
( 0 <= L & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators X,Y) st f in T holds
||.f.|| <= L ) )
let Y be RealNormSpace; for T being Subset of (R_NormSpace_of_BoundedLinearOperators X,Y) st ( for x being Point of X ex K being real number st
( 0 <= K & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators X,Y) st f in T holds
||.(f . x).|| <= K ) ) ) holds
ex L being real number st
( 0 <= L & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators X,Y) st f in T holds
||.f.|| <= L ) )
let T be Subset of (R_NormSpace_of_BoundedLinearOperators X,Y); ( ( for x being Point of X ex K being real number st
( 0 <= K & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators X,Y) st f in T holds
||.(f . x).|| <= K ) ) ) implies ex L being real number st
( 0 <= L & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators X,Y) st f in T holds
||.f.|| <= L ) ) )
assume A1:
for x being Point of X ex KTx being real number st
( 0 <= KTx & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators X,Y) st f in T holds
||.(f . x).|| <= KTx ) )
; ex L being real number st
( 0 <= L & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators X,Y) st f in T holds
||.f.|| <= L ) )
per cases
( T <> {} or T = {} )
;
suppose A2:
T <> {}
;
ex L being real number st
( 0 <= L & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators X,Y) st f in T holds
||.f.|| <= L ) )deffunc H1(
Point of
X,
Real)
-> Subset of
X =
Ball $1,$2;
defpred S1[
Point of
X,
set ]
means $2
= { ||.(f . $1).|| where f is bounded LinearOperator of X,Y : f in T } ;
A3:
for
x being
Point of
X ex
y being
Element of
bool REAL st
S1[
x,
y]
ex
Ta being
Function of the
carrier of
X,
(bool REAL ) st
for
x being
Element of
X holds
S1[
x,
Ta . x]
from FUNCT_2:sch 3(A3);
then consider Ta being
Function of
X,
(bool REAL ) such that A4:
for
x being
Point of
X holds
Ta . x = { ||.(f . x).|| where f is bounded LinearOperator of X,Y : f in T }
;
defpred S2[
Element of
NAT ,
set ]
means $2
= { x where x is Point of X : ( Ta . x is bounded_above & sup (Ta . x) <= $1 ) } ;
A5:
for
n being
Element of
NAT ex
y being
Element of
bool the
carrier of
X st
S2[
n,
y]
ex
Xn being
Function of
NAT ,
(bool the carrier of X) st
for
n being
Element of
NAT holds
S2[
n,
Xn . n]
from FUNCT_2:sch 3(A5);
then consider Xn being
Function of
NAT ,
(bool the carrier of X) such that A6:
for
n being
Element of
NAT holds
Xn . n = { x where x is Point of X : ( Ta . x is bounded_above & sup (Ta . x) <= n ) }
;
reconsider Xn =
Xn as
SetSequence of
X ;
A7:
the
carrier of
X c= union (rng Xn)
A14:
for
x being
Point of
X holds not
Ta . x is
empty
A16:
for
n being
Element of
NAT holds
Xn . n is
closed
proof
let n be
Element of
NAT ;
Xn . n is closed
for
s1 being
sequence of
X st
rng s1 c= Xn . n &
s1 is
convergent holds
lim s1 in Xn . n
proof
let s1 be
sequence of
X;
( rng s1 c= Xn . n & s1 is convergent implies lim s1 in Xn . n )
assume that A17:
rng s1 c= Xn . n
and A18:
s1 is
convergent
;
lim s1 in Xn . n
A19:
Ta . (lim s1) = { ||.(f . (lim s1)).|| where f is bounded LinearOperator of X,Y : f in T }
by A4;
A20:
for
y being
real number st
y in Ta . (lim s1) holds
y <= n
proof
let y be
real number ;
( y in Ta . (lim s1) implies y <= n )
assume
y in Ta . (lim s1)
;
y <= n
then consider f being
bounded LinearOperator of
X,
Y such that A21:
y = ||.(f . (lim s1)).||
and A22:
f in T
by A19;
A23:
f is_continuous_in lim s1
by Th4;
A24:
dom f = the
carrier of
X
by FUNCT_2:def 1;
then A25:
rng s1 c= dom f
by A17, XBOOLE_1:1;
then A26:
f /* s1 is
convergent
by A18, A23, NFCONT_1:def 9;
for
k being
Element of
NAT holds
||.(f /* s1).|| . k <= n
proof
let k be
Element of
NAT ;
||.(f /* s1).|| . k <= n
||.(f /* s1).|| . k = ||.((f /* s1) . k).||
by NORMSP_1:def 10;
then A27:
||.(f /* s1).|| . k = ||.(f /. (s1 . k)).||
by A17, A24, FUNCT_2:186, XBOOLE_1:1;
dom s1 = NAT
by FUNCT_2:def 1;
then
s1 . k in rng s1
by FUNCT_1:12;
then
s1 . k in Xn . n
by A17;
then
s1 . k in { x where x is Point of X : ( Ta . x is bounded_above & sup (Ta . x) <= n ) }
by A6;
then consider x being
Point of
X such that A28:
x = s1 . k
and A29:
Ta . x is
bounded_above
and A30:
sup (Ta . x) <= n
;
Ta . x = { ||.(g . x).|| where g is bounded LinearOperator of X,Y : g in T }
by A4;
then
||.(f . (s1 . k)).|| in Ta . (s1 . k)
by A22, A28;
then
||.(f . (s1 . k)).|| <= sup (Ta . (s1 . k))
by A28, A29, SEQ_4:def 4;
hence
||.(f /* s1).|| . k <= n
by A27, A28, A30, XXREAL_0:2;
verum
end;
then A31:
for
i being
Element of
NAT st
0 <= i holds
||.(f /* s1).|| . i <= n
;
f /. (lim s1) = lim (f /* s1)
by A18, A23, A25, NFCONT_1:def 9;
then
lim ||.(f /* s1).|| = ||.(f /. (lim s1)).||
by A26, LOPBAN_1:24;
hence
y <= n
by A21, A26, A31, NORMSP_1:39, RSSPACE2:6;
verum
end;
not
Ta . (lim s1) is
empty
by A14;
then A32:
sup (Ta . (lim s1)) <= n
by A20, SEQ_4:62;
A33:
Xn . n = { x where x is Point of X : ( Ta . x is bounded_above & sup (Ta . x) <= n ) }
by A6;
Ta . (lim s1) is
bounded_above
by A20, SEQ_4:def 1;
hence
lim s1 in Xn . n
by A32, A33;
verum
end;
hence
Xn . n is
closed
by NFCONT_1:def 5;
verum
end; consider f being
set such that A34:
f in T
by A2, XBOOLE_0:def 1;
reconsider f =
f as
bounded LinearOperator of
X,
Y by A34, LOPBAN_1:def 10;
union (rng Xn) is
Subset of
X
by PROB_1:23;
then
union (rng Xn) = the
carrier of
X
by A7, XBOOLE_0:def 10;
then consider n0 being
Element of
NAT ,
r being
Real,
x0 being
Point of
X such that A35:
0 < r
and A36:
H1(
x0,
r)
c= Xn . n0
by A16, Th3;
||.(x0 - x0).|| = ||.(0. X).||
by RLVECT_1:16;
then
x0 in H1(
x0,
r)
by A35;
then
x0 in Xn . n0
by A36;
then
x0 in { x1 where x1 is Point of X : ( Ta . x1 is bounded_above & sup (Ta . x1) <= n0 ) }
by A6;
then consider xx1 being
Point of
X such that A37:
xx1 = x0
and A38:
Ta . xx1 is
bounded_above
and
sup (Ta . xx1) <= n0
;
Ta . xx1 = { ||.(g . xx1).|| where g is bounded LinearOperator of X,Y : g in T }
by A4;
then
||.(f . x0).|| in Ta . x0
by A37, A34;
then
||.(f . x0).|| <= sup (Ta . x0)
by A37, A38, SEQ_4:def 4;
then A39:
0 <= sup (Ta . x0)
by NORMSP_1:8;
A40:
for
x being
Point of
X st
x <> 0. X holds
((r / (2 * ||.x.||)) * x) + x0 in H1(
x0,
r)
set M =
upper_bound (Ta . x0);
take KT =
(2 * ((upper_bound (Ta . x0)) + n0)) / r;
( 0 <= KT & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators X,Y) st f in T holds
||.f.|| <= KT ) )A46:
for
f being
bounded LinearOperator of
X,
Y st
f in T holds
for
x being
Point of
X st
x in H1(
x0,
r) holds
||.(f . x).|| <= n0
proof
let f be
bounded LinearOperator of
X,
Y;
( f in T implies for x being Point of X st x in H1(x0,r) holds
||.(f . x).|| <= n0 )
assume A47:
f in T
;
for x being Point of X st x in H1(x0,r) holds
||.(f . x).|| <= n0
let x be
Point of
X;
( x in H1(x0,r) implies ||.(f . x).|| <= n0 )
assume
x in H1(
x0,
r)
;
||.(f . x).|| <= n0
then
x in Xn . n0
by A36;
then
x in { x1 where x1 is Point of X : ( Ta . x1 is bounded_above & sup (Ta . x1) <= n0 ) }
by A6;
then consider x1 being
Point of
X such that A48:
x1 = x
and A49:
Ta . x1 is
bounded_above
and A50:
sup (Ta . x1) <= n0
;
Ta . x1 = { ||.(g . x1).|| where g is bounded LinearOperator of X,Y : g in T }
by A4;
then
||.(f . x).|| in Ta . x
by A47, A48;
then
||.(f . x).|| <= sup (Ta . x)
by A48, A49, SEQ_4:def 4;
hence
||.(f . x).|| <= n0
by A48, A50, XXREAL_0:2;
verum
end; A51:
now let f be
bounded LinearOperator of
X,
Y;
( f in T implies for k being real number st k in { ||.(f . x1).|| where x1 is Point of X : ||.x1.|| <= 1 } holds
k <= KT )assume A52:
f in T
;
for k being real number st k in { ||.(f . x1).|| where x1 is Point of X : ||.x1.|| <= 1 } holds
k <= KTA53:
for
x being
Point of
X st
x <> 0. X holds
||.(f . x).|| <= KT * ||.x.||
proof
||.(x0 - x0).|| = ||.(0. X).||
by RLVECT_1:16;
then
x0 in H1(
x0,
r)
by A35;
then
x0 in Xn . n0
by A36;
then A54:
x0 in { x1 where x1 is Point of X : ( Ta . x1 is bounded_above & sup (Ta . x1) <= n0 ) }
by A6;
set nr3 =
||.(f . x0).||;
let x be
Point of
X;
( x <> 0. X implies ||.(f . x).|| <= KT * ||.x.|| )
set nrp1 =
r / (2 * ||.x.||);
set nrp2 =
(2 * ||.x.||) / r;
set nr1 =
||.((f . ((r / (2 * ||.x.||)) * x)) + (f . x0)).||;
set nr2 =
||.(f . ((r / (2 * ||.x.||)) * x)).||;
||.(- (f . x0)).|| = ||.(f . x0).||
by NORMSP_1:6;
then A55:
||.(f . ((r / (2 * ||.x.||)) * x)).|| - ||.(f . x0).|| <= ||.((f . ((r / (2 * ||.x.||)) * x)) - (- (f . x0))).||
by NORMSP_1:12;
assume A56:
x <> 0. X
;
||.(f . x).|| <= KT * ||.x.||
then A57:
||.(f . (((r / (2 * ||.x.||)) * x) + x0)).|| <= n0
by A46, A40, A52;
consider x1 being
Point of
X such that A58:
x1 = x0
and A59:
Ta . x1 is
bounded_above
and
sup (Ta . x1) <= n0
by A54;
Ta . x1 = { ||.(g . x1).|| where g is bounded LinearOperator of X,Y : g in T }
by A4;
then
||.(f . x0).|| in Ta . x0
by A52, A58;
then
||.(f . x0).|| <= sup (Ta . x0)
by A58, A59, SEQ_4:def 4;
then A60:
((r / (2 * ||.x.||)) * ||.(f . x).||) - (upper_bound (Ta . x0)) <= ((r / (2 * ||.x.||)) * ||.(f . x).||) - ||.(f . x0).||
by XREAL_1:12;
||.x.|| <> 0
by A56, NORMSP_1:def 2;
then A61:
||.x.|| > 0
by NORMSP_1:8;
||.(f . ((r / (2 * ||.x.||)) * x)).|| = ||.((r / (2 * ||.x.||)) * (f . x)).||
by LOPBAN_1:def 6;
then
||.(f . ((r / (2 * ||.x.||)) * x)).|| = (abs (r / (2 * ||.x.||))) * ||.(f . x).||
by NORMSP_1:def 2;
then
||.(f . ((r / (2 * ||.x.||)) * x)).|| = (r / (2 * ||.x.||)) * ||.(f . x).||
by A35, A61, ABSVALUE:def 1;
then
(
||.((f . ((r / (2 * ||.x.||)) * x)) + (f . x0)).|| = ||.(f . (((r / (2 * ||.x.||)) * x) + x0)).|| &
((r / (2 * ||.x.||)) * ||.(f . x).||) - ||.(f . x0).|| <= ||.((f . ((r / (2 * ||.x.||)) * x)) + (f . x0)).|| )
by A55, LOPBAN_1:def 5, RLVECT_1:30;
then
((r / (2 * ||.x.||)) * ||.(f . x).||) - ||.(f . x0).|| <= n0
by A57, XXREAL_0:2;
then
((r / (2 * ||.x.||)) * ||.(f . x).||) - (upper_bound (Ta . x0)) <= n0
by A60, XXREAL_0:2;
then
(((r / (2 * ||.x.||)) * ||.(f . x).||) + (- (upper_bound (Ta . x0)))) + (upper_bound (Ta . x0)) <= n0 + (upper_bound (Ta . x0))
by XREAL_1:8;
then
((2 * ||.x.||) / r) * ((r / (2 * ||.x.||)) * ||.(f . x).||) <= ((2 * ||.x.||) / r) * (n0 + (upper_bound (Ta . x0)))
by A35, A61, XREAL_1:66;
then A62:
((r / (2 * ||.x.||)) * ((2 * ||.x.||) / r)) * ||.(f . x).|| <= ((2 * ||.x.||) / r) * (n0 + (upper_bound (Ta . x0)))
;
2
* ||.x.|| > 0
by A61, XREAL_1:131;
then
1
* ||.(f . x).|| <= ((2 * ||.x.||) / r) * (n0 + (upper_bound (Ta . x0)))
by A35, A62, XCMPLX_1:113;
hence
||.(f . x).|| <= KT * ||.x.||
;
verum
end; A63:
for
x being
Point of
X holds
||.(f . x).|| <= KT * ||.x.||
thus
for
k being
real number st
k in { ||.(f . x1).|| where x1 is Point of X : ||.x1.|| <= 1 } holds
k <= KT
verum end;
for
f being
Point of
(R_NormSpace_of_BoundedLinearOperators X,Y) st
f in T holds
||.f.|| <= KT
hence
(
0 <= KT & ( for
f being
Point of
(R_NormSpace_of_BoundedLinearOperators X,Y) st
f in T holds
||.f.|| <= KT ) )
by A35, A39;
verum end;