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 & upper_bound (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 & upper_bound (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 5;
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_0:def 4;
then A27:
||.(f /* s1).|| . k = ||.(f /. (s1 . k)).||
by A17, A24, FUNCT_2:109, XBOOLE_1:1;
dom s1 = NAT
by FUNCT_2:def 1;
then
s1 . k in rng s1
by FUNCT_1:3;
then
s1 . k in Xn . n
by A17;
then
s1 . k in { x where x is Point of X : ( Ta . x is bounded_above & upper_bound (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:
upper_bound (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)).|| <= upper_bound (Ta . (s1 . k))
by A28, A29, SEQ_4:def 1;
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 5;
then
lim ||.(f /* s1).|| = ||.(f /. (lim s1)).||
by A26, LOPBAN_1:20;
hence
y <= n
by A21, A26, A31, NORMSP_1:23, RSSPACE2:5;
verum
end;
then
for
y being
ext-real number st
y in Ta . (lim s1) holds
y <= n
;
then A32:
n is
UpperBound of
Ta . (lim s1)
by XXREAL_2:def 1;
not
Ta . (lim s1) is
empty
by A14;
then A33:
upper_bound (Ta . (lim s1)) <= n
by A20, SEQ_4:45;
A34:
Xn . n = { x where x is Point of X : ( Ta . x is bounded_above & upper_bound (Ta . x) <= n ) }
by A6;
Ta . (lim s1) is
bounded_above
by A32, XXREAL_2:def 10;
hence
lim s1 in Xn . n
by A33, A34;
verum
end;
hence
Xn . n is
closed
by NFCONT_1:def 3;
verum
end; consider f being
set such that A35:
f in T
by A2, XBOOLE_0:def 1;
reconsider f =
f as
bounded LinearOperator of
X,
Y by A35, LOPBAN_1:def 9;
union (rng Xn) is
Subset of
X
by PROB_1:11;
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 A36:
0 < r
and A37:
H1(
x0,
r)
c= Xn . n0
by A16, Th3;
||.(x0 - x0).|| = ||.(0. X).||
by RLVECT_1:5;
then
x0 in H1(
x0,
r)
by A36;
then
x0 in Xn . n0
by A37;
then
x0 in { x1 where x1 is Point of X : ( Ta . x1 is bounded_above & upper_bound (Ta . x1) <= n0 ) }
by A6;
then consider xx1 being
Point of
X such that A38:
xx1 = x0
and A39:
Ta . xx1 is
bounded_above
and
upper_bound (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 A38, A35;
then
||.(f . x0).|| <= upper_bound (Ta . x0)
by A38, A39, SEQ_4:def 1;
then A40:
0 <= upper_bound (Ta . x0)
;
A41:
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 ) )A47:
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 A48:
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 A37;
then
x in { x1 where x1 is Point of X : ( Ta . x1 is bounded_above & upper_bound (Ta . x1) <= n0 ) }
by A6;
then consider x1 being
Point of
X such that A49:
x1 = x
and A50:
Ta . x1 is
bounded_above
and A51:
upper_bound (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 A48, A49;
then
||.(f . x).|| <= upper_bound (Ta . x)
by A49, A50, SEQ_4:def 1;
hence
||.(f . x).|| <= n0
by A49, A51, XXREAL_0:2;
verum
end; A52:
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 A53:
f in T
;
for k being real number st k in { ||.(f . x1).|| where x1 is Point of X : ||.x1.|| <= 1 } holds
k <= KTA54:
for
x being
Point of
X st
x <> 0. X holds
||.(f . x).|| <= KT * ||.x.||
proof
||.(x0 - x0).|| = ||.(0. X).||
by RLVECT_1:5;
then
x0 in H1(
x0,
r)
by A36;
then
x0 in Xn . n0
by A37;
then A55:
x0 in { x1 where x1 is Point of X : ( Ta . x1 is bounded_above & upper_bound (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:2;
then A56:
||.(f . ((r / (2 * ||.x.||)) * x)).|| - ||.(f . x0).|| <= ||.((f . ((r / (2 * ||.x.||)) * x)) - (- (f . x0))).||
by NORMSP_1:8;
assume A57:
x <> 0. X
;
||.(f . x).|| <= KT * ||.x.||
then A58:
||.(f . (((r / (2 * ||.x.||)) * x) + x0)).|| <= n0
by A47, A41, A53;
consider x1 being
Point of
X such that A59:
x1 = x0
and A60:
Ta . x1 is
bounded_above
and
upper_bound (Ta . x1) <= n0
by A55;
Ta . x1 = { ||.(g . x1).|| where g is bounded LinearOperator of X,Y : g in T }
by A4;
then
||.(f . x0).|| in Ta . x0
by A53, A59;
then
||.(f . x0).|| <= upper_bound (Ta . x0)
by A59, A60, SEQ_4:def 1;
then A61:
((r / (2 * ||.x.||)) * ||.(f . x).||) - (upper_bound (Ta . x0)) <= ((r / (2 * ||.x.||)) * ||.(f . x).||) - ||.(f . x0).||
by XREAL_1:10;
||.x.|| <> 0
by A57, NORMSP_0:def 5;
then A62:
||.x.|| > 0
;
||.(f . ((r / (2 * ||.x.||)) * x)).|| = ||.((r / (2 * ||.x.||)) * (f . x)).||
by LOPBAN_1:def 5;
then
||.(f . ((r / (2 * ||.x.||)) * x)).|| = (abs (r / (2 * ||.x.||))) * ||.(f . x).||
by NORMSP_1:def 1;
then
||.(f . ((r / (2 * ||.x.||)) * x)).|| = (r / (2 * ||.x.||)) * ||.(f . x).||
by A36, 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 A56, GRCAT_1:def 8, RLVECT_1:17;
then
((r / (2 * ||.x.||)) * ||.(f . x).||) - ||.(f . x0).|| <= n0
by A58, XXREAL_0:2;
then
((r / (2 * ||.x.||)) * ||.(f . x).||) - (upper_bound (Ta . x0)) <= n0
by A61, 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:6;
then
((2 * ||.x.||) / r) * ((r / (2 * ||.x.||)) * ||.(f . x).||) <= ((2 * ||.x.||) / r) * (n0 + (upper_bound (Ta . x0)))
by A36, XREAL_1:64;
then A63:
((r / (2 * ||.x.||)) * ((2 * ||.x.||) / r)) * ||.(f . x).|| <= ((2 * ||.x.||) / r) * (n0 + (upper_bound (Ta . x0)))
;
2
* ||.x.|| > 0
by A62, XREAL_1:129;
then
1
* ||.(f . x).|| <= ((2 * ||.x.||) / r) * (n0 + (upper_bound (Ta . x0)))
by A36, A63, XCMPLX_1:112;
hence
||.(f . x).|| <= KT * ||.x.||
;
verum
end; A64:
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 A36, A40;
verum end;