let X be RealBanachSpace; for Y being RealNormSpace
for T being bounded LinearOperator of X,Y
for r being real number
for BX1 being Subset of (LinearTopSpaceNorm X)
for TBX1, BYr being Subset of (LinearTopSpaceNorm Y) st r > 0 & BYr = Ball (0. Y),r & TBX1 = T .: (Ball (0. X),1) & BYr c= Cl TBX1 holds
BYr c= TBX1
let Y be RealNormSpace; for T being bounded LinearOperator of X,Y
for r being real number
for BX1 being Subset of (LinearTopSpaceNorm X)
for TBX1, BYr being Subset of (LinearTopSpaceNorm Y) st r > 0 & BYr = Ball (0. Y),r & TBX1 = T .: (Ball (0. X),1) & BYr c= Cl TBX1 holds
BYr c= TBX1
let T be bounded LinearOperator of X,Y; for r being real number
for BX1 being Subset of (LinearTopSpaceNorm X)
for TBX1, BYr being Subset of (LinearTopSpaceNorm Y) st r > 0 & BYr = Ball (0. Y),r & TBX1 = T .: (Ball (0. X),1) & BYr c= Cl TBX1 holds
BYr c= TBX1
let r be real number ; for BX1 being Subset of (LinearTopSpaceNorm X)
for TBX1, BYr being Subset of (LinearTopSpaceNorm Y) st r > 0 & BYr = Ball (0. Y),r & TBX1 = T .: (Ball (0. X),1) & BYr c= Cl TBX1 holds
BYr c= TBX1
let BX1 be Subset of (LinearTopSpaceNorm X); for TBX1, BYr being Subset of (LinearTopSpaceNorm Y) st r > 0 & BYr = Ball (0. Y),r & TBX1 = T .: (Ball (0. X),1) & BYr c= Cl TBX1 holds
BYr c= TBX1
let TBX1, BYr be Subset of (LinearTopSpaceNorm Y); ( r > 0 & BYr = Ball (0. Y),r & TBX1 = T .: (Ball (0. X),1) & BYr c= Cl TBX1 implies BYr c= TBX1 )
assume that
A1:
r > 0
and
A2:
BYr = Ball (0. Y),r
and
A3:
TBX1 = T .: (Ball (0. X),1)
and
A4:
BYr c= Cl TBX1
; BYr c= TBX1
A5:
for x being Point of X
for y being Point of Y
for TB1, BYsr being Subset of (LinearTopSpaceNorm Y)
for s being real number st s > 0 & TB1 = T .: (Ball x,s) & y = T . x & BYsr = Ball y,(s * r) holds
BYsr c= Cl TB1
proof
reconsider TB01 =
T .: (Ball (0. X),1) as
Subset of
Y ;
let x be
Point of
X;
for y being Point of Y
for TB1, BYsr being Subset of (LinearTopSpaceNorm Y)
for s being real number st s > 0 & TB1 = T .: (Ball x,s) & y = T . x & BYsr = Ball y,(s * r) holds
BYsr c= Cl TB1let y be
Point of
Y;
for TB1, BYsr being Subset of (LinearTopSpaceNorm Y)
for s being real number st s > 0 & TB1 = T .: (Ball x,s) & y = T . x & BYsr = Ball y,(s * r) holds
BYsr c= Cl TB1let TB1,
BYsr be
Subset of
(LinearTopSpaceNorm Y);
for s being real number st s > 0 & TB1 = T .: (Ball x,s) & y = T . x & BYsr = Ball y,(s * r) holds
BYsr c= Cl TB1let s be
real number ;
( s > 0 & TB1 = T .: (Ball x,s) & y = T . x & BYsr = Ball y,(s * r) implies BYsr c= Cl TB1 )
assume that A6:
s > 0
and A7:
TB1 = T .: (Ball x,s)
and A8:
y = T . x
and A9:
BYsr = Ball y,
(s * r)
;
BYsr c= Cl TB1
reconsider s1 =
s as non
zero Real by A6, XREAL_0:def 1;
reconsider y1 =
y as
Point of
(LinearTopSpaceNorm Y) by NORMSP_2:def 4;
A10:
Ball y,
(s * r) = y + (Ball (0. Y),(s * r))
by Th2;
reconsider TB0xs =
T .: (Ball x,s) as
Subset of
Y ;
reconsider TB0s =
T .: (Ball (0. X),s) as
Subset of
Y ;
Ball x,
s = x + (Ball (0. X),s)
by Th2;
then A11:
y + TB0s = TB0xs
by A8, Th6;
s1 * BYr c= s1 * (Cl TBX1)
by A4, CONVEX1:39;
then
s1 * BYr c= Cl (s1 * TBX1)
by RLTOPSP1:53;
then
y1 + (s1 * BYr) c= y1 + (Cl (s1 * TBX1))
by RLTOPSP1:8;
then A12:
y1 + (s1 * BYr) c= Cl (y1 + (s1 * TBX1))
by RLTOPSP1:39;
Ball (0. Y),
(s * r) = s1 * (Ball (0. Y),r)
by A6, Th3;
then
Ball (0. Y),
(s * r) = s1 * BYr
by A2, Th9;
then A13:
y1 + (s1 * BYr) = BYsr
by A9, A10, Th8;
A14:
s1 * (Ball (0. X),1) = Ball (0. X),
(s1 * 1)
by A6, Th3;
s1 * TB01 = s1 * TBX1
by A3, Th9;
hence
BYsr c= Cl TB1
by A7, A12, A13, A11, A14, Th5, Th8;
verum
reconsider x1 =
x as
Point of
(LinearTopSpaceNorm X) by NORMSP_2:def 4;
reconsider TB0 =
T .: (Ball (0. X),s) as
Subset of
(LinearTopSpaceNorm Y) by NORMSP_2:def 4;
end;
A15:
for s0 being real number st s0 > 0 holds
Ball (0. Y),r c= T .: (Ball (0. X),(1 + s0))
proof
let s0 be
real number ;
( s0 > 0 implies Ball (0. Y),r c= T .: (Ball (0. X),(1 + s0)) )
assume A16:
s0 > 0
;
Ball (0. Y),r c= T .: (Ball (0. X),(1 + s0))
now let z be
set ;
( z in Ball (0. Y),r implies z in T .: (Ball (0. X),(1 + s0)) )assume A17:
z in Ball (0. Y),
r
;
z in T .: (Ball (0. X),(1 + s0))then reconsider y =
z as
Point of
Y ;
consider s1 being
real number such that A18:
0 < s1
and A19:
s1 < s0
by A16, XREAL_1:7;
set a =
s1 / (1 + s1);
set e =
(s1 / (1 + s1)) GeoSeq ;
A20:
s1 / (1 + s1) < 1
by A18, XREAL_1:31, XREAL_1:193;
then A21:
abs (s1 / (1 + s1)) < 1
by A18, ABSVALUE:def 1;
then A22:
(s1 / (1 + s1)) GeoSeq is
summable
by SERIES_1:28;
defpred S1[
Element of
NAT ,
Point of
X,
Point of
X,
Point of
X]
means ( $3
in Ball $2,
(((s1 / (1 + s1)) GeoSeq ) . $1) &
||.((T . $3) - y).|| < (((s1 / (1 + s1)) GeoSeq ) . ($1 + 1)) * r implies ( $4
in Ball $3,
(((s1 / (1 + s1)) GeoSeq ) . ($1 + 1)) &
||.((T . $4) - y).|| < (((s1 / (1 + s1)) GeoSeq ) . ($1 + 2)) * r ) );
reconsider B0 =
Ball y,
((((s1 / (1 + s1)) GeoSeq ) . 1) * r) as
Subset of
(LinearTopSpaceNorm Y) by NORMSP_2:def 4;
A23:
0 < s1 / (1 + s1)
by A18, XREAL_1:141;
then
(
((s1 / (1 + s1)) GeoSeq ) . 1
= (s1 / (1 + s1)) |^ 1 &
0 < (s1 / (1 + s1)) |^ 1 )
by NEWTON:102, PREPOWER:def 1;
then
0 < (((s1 / (1 + s1)) GeoSeq ) . 1) * r
by A1, XREAL_1:131;
then
||.(y - y).|| < (((s1 / (1 + s1)) GeoSeq ) . 1) * r
by NORMSP_1:10;
then
(
B0 is
open &
y in B0 )
by NORMSP_2:23;
then
Ball y,
((((s1 / (1 + s1)) GeoSeq ) . 1) * r) meets TBX1
by A2, A4, A17, PRE_TOPC:def 13;
then consider s being
set such that A24:
s in Ball y,
((((s1 / (1 + s1)) GeoSeq ) . 1) * r)
and A25:
s in T .: (Ball (0. X),1)
by A3, XBOOLE_0:3;
consider xn1 being
set such that A26:
xn1 in the
carrier of
X
and A27:
xn1 in Ball (0. X),1
and A28:
s = T . xn1
by A25, FUNCT_2:115;
reconsider xn1 =
xn1 as
Point of
X by A26;
A29:
for
n being
Element of
NAT for
v,
w being
Point of
X ex
z being
Point of
X st
S1[
n,
v,
w,
z]
proof
let n be
Element of
NAT ;
for v, w being Point of X ex z being Point of X st S1[n,v,w,z]let v,
w be
Point of
X;
ex z being Point of X st S1[n,v,w,z]
now reconsider B0 =
Ball y,
((((s1 / (1 + s1)) GeoSeq ) . (n + 2)) * r) as
Subset of
(LinearTopSpaceNorm Y) by NORMSP_2:def 4;
reconsider BYsr =
Ball (T . w),
((((s1 / (1 + s1)) GeoSeq ) . (n + 1)) * r) as
Subset of
(LinearTopSpaceNorm Y) by NORMSP_2:def 4;
reconsider TB1 =
T .: (Ball w,(((s1 / (1 + s1)) GeoSeq ) . (n + 1))) as
Subset of
(LinearTopSpaceNorm Y) by NORMSP_2:def 4;
assume that
w in Ball v,
(((s1 / (1 + s1)) GeoSeq ) . n)
and A30:
||.((T . w) - y).|| < (((s1 / (1 + s1)) GeoSeq ) . (n + 1)) * r
;
ex z being Point of X st
( z in Ball w,(((s1 / (1 + s1)) GeoSeq ) . (n + 1)) & ||.((T . z) - y).|| < (((s1 / (1 + s1)) GeoSeq ) . (n + 2)) * r )
((s1 / (1 + s1)) GeoSeq ) . (n + 1) = (s1 / (1 + s1)) |^ (n + 1)
by PREPOWER:def 1;
then A31:
BYsr c= Cl TB1
by A5, A23, NEWTON:102;
(
((s1 / (1 + s1)) GeoSeq ) . (n + 2) = (s1 / (1 + s1)) |^ (n + 2) &
0 < (s1 / (1 + s1)) |^ (n + 2) )
by A23, NEWTON:102, PREPOWER:def 1;
then
0 < (((s1 / (1 + s1)) GeoSeq ) . (n + 2)) * r
by A1, XREAL_1:131;
then
||.(y - y).|| < (((s1 / (1 + s1)) GeoSeq ) . (n + 2)) * r
by NORMSP_1:10;
then A32:
(
B0 is
open &
y in B0 )
by NORMSP_2:23;
y in BYsr
by A30;
then
Ball y,
((((s1 / (1 + s1)) GeoSeq ) . (n + 2)) * r) meets TB1
by A31, A32, PRE_TOPC:def 13;
then consider s being
set such that A33:
s in Ball y,
((((s1 / (1 + s1)) GeoSeq ) . (n + 2)) * r)
and A34:
s in T .: (Ball w,(((s1 / (1 + s1)) GeoSeq ) . (n + 1)))
by XBOOLE_0:3;
consider z being
set such that A35:
z in the
carrier of
X
and A36:
z in Ball w,
(((s1 / (1 + s1)) GeoSeq ) . (n + 1))
and A37:
s = T . z
by A34, FUNCT_2:115;
reconsider z =
z as
Point of
X by A35;
reconsider sb =
T . z as
Point of
Y ;
ex
ss1 being
Point of
Y st
(
sb = ss1 &
||.(y - ss1).|| < (((s1 / (1 + s1)) GeoSeq ) . (n + 2)) * r )
by A33, A37;
then
||.((T . z) - y).|| < (((s1 / (1 + s1)) GeoSeq ) . (n + 2)) * r
by NORMSP_1:11;
hence
ex
z being
Point of
X st
(
z in Ball w,
(((s1 / (1 + s1)) GeoSeq ) . (n + 1)) &
||.((T . z) - y).|| < (((s1 / (1 + s1)) GeoSeq ) . (n + 2)) * r )
by A36;
verum end;
hence
ex
z being
Point of
X st
S1[
n,
v,
w,
z]
;
verum
end; consider xn being
sequence of
X such that A38:
(
xn . 0 = 0. X &
xn . 1
= xn1 & ( for
n being
Element of
NAT holds
S1[
n,
xn . n,
xn . (n + 1),
xn . (n + 2)] ) )
from LOPBAN_6:sch 1(A29);
reconsider sb =
T . xn1 as
Point of
Y ;
A39:
ex
ss1 being
Point of
Y st
(
sb = ss1 &
||.(y - ss1).|| < (((s1 / (1 + s1)) GeoSeq ) . 1) * r )
by A24, A28;
A40:
for
n being
Element of
NAT holds
(
xn . (n + 1) in Ball (xn . n),
(((s1 / (1 + s1)) GeoSeq ) . n) &
||.((T . (xn . (n + 1))) - y).|| < (((s1 / (1 + s1)) GeoSeq ) . (n + 1)) * r )
A44:
((s1 / (1 + s1)) GeoSeq ) . 0 = 1
by PREPOWER:4;
A45:
for
m,
k being
Element of
NAT holds
||.((xn . (m + k)) - (xn . m)).|| <= (((s1 / (1 + s1)) GeoSeq ) . m) * ((1 - (((s1 / (1 + s1)) GeoSeq ) . k)) / (1 - (((s1 / (1 + s1)) GeoSeq ) . 1)))
A52:
for
k being
Element of
NAT st
0 <= k holds
||.xn.|| . k <= 1
/ (1 - (s1 / (1 + s1)))
A56:
Sum ((s1 / (1 + s1)) GeoSeq ) = 1
/ (1 - (s1 / (1 + s1)))
by A21, SERIES_1:28;
1
/ (1 - (s1 / (1 + s1))) =
1
/ (((1 * (1 + s1)) - s1) / (1 + s1))
by A18, XCMPLX_1:128
.=
1
+ s1
by XCMPLX_1:101
;
then A57:
Sum ((s1 / (1 + s1)) GeoSeq ) < 1
+ s0
by A19, A56, XREAL_1:8;
set xx =
lim xn;
then
xn is
CCauchy
by LOPBAN_3:5;
then A67:
xn is
convergent
by LOPBAN_1:def 16;
then
lim ||.xn.|| = ||.(lim xn).||
by LOPBAN_1:47;
then
||.(lim xn).|| <= Sum ((s1 / (1 + s1)) GeoSeq )
by A56, A67, A52, LOPBAN_1:47, RSSPACE2:6;
then
||.(lim xn).|| < 1
+ s0
by A57, XXREAL_0:2;
then
||.(- (lim xn)).|| < 1
+ s0
by NORMSP_1:6;
then
||.((0. X) - (lim xn)).|| < 1
+ s0
by RLVECT_1:27;
then A68:
lim xn in Ball (0. X),
(1 + s0)
;
rng xn c= the
carrier of
X
;
then A69:
rng xn c= dom T
by FUNCT_2:def 1;
A71:
now let s be
Real;
( 0 < s implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(((T /* xn) . n) - y).|| < s )assume
0 < s
;
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(((T /* xn) . n) - y).|| < sthen A72:
0 < s / r
by A1, XREAL_1:141;
(
(s1 / (1 + s1)) GeoSeq is
convergent &
lim ((s1 / (1 + s1)) GeoSeq ) = 0 )
by A22, SERIES_1:7;
then consider m0 being
Element of
NAT such that A73:
for
n being
Element of
NAT st
m0 <= n holds
abs ((((s1 / (1 + s1)) GeoSeq ) . n) - 0 ) < s / r
by A72, SEQ_2:def 7;
take m =
m0 + 1;
for n being Element of NAT st m <= n holds
||.(((T /* xn) . n) - y).|| < s
(
(s1 / (1 + s1)) |^ 1
< 1 &
0 < (s1 / (1 + s1)) |^ m0 )
by A23, A20, NEWTON:10, NEWTON:102;
then
((s1 / (1 + s1)) |^ m0) * ((s1 / (1 + s1)) |^ 1) <= (s1 / (1 + s1)) |^ m0
by XREAL_1:155;
then
(s1 / (1 + s1)) |^ (m0 + 1) <= (s1 / (1 + s1)) |^ m0
by NEWTON:13;
then
((s1 / (1 + s1)) GeoSeq ) . (m0 + 1) <= (s1 / (1 + s1)) |^ m0
by PREPOWER:def 1;
then A74:
((s1 / (1 + s1)) GeoSeq ) . (m0 + 1) <= ((s1 / (1 + s1)) GeoSeq ) . m0
by PREPOWER:def 1;
abs ((((s1 / (1 + s1)) GeoSeq ) . m0) - 0 ) < s / r
by A73;
then
((s1 / (1 + s1)) GeoSeq ) . m0 < 0 + (s / r)
by RINFSUP1:1;
then
((s1 / (1 + s1)) GeoSeq ) . (m0 + 1) < s / r
by A74, XXREAL_0:2;
then
(((s1 / (1 + s1)) GeoSeq ) . (m0 + 1)) * r < (s / r) * r
by A1, XREAL_1:70;
then A75:
(((s1 / (1 + s1)) GeoSeq ) . (m0 + 1)) * r < s
by A1, XCMPLX_1:88;
now let n be
Element of
NAT ;
( m <= n implies ||.(((T /* xn) . n) - y).|| < s )assume A76:
m <= n
;
||.(((T /* xn) . n) - y).|| < s
1
<= m0 + 1
by NAT_1:11;
then reconsider n0 =
n - 1 as
Element of
NAT by A76, NAT_1:21, XXREAL_0:2;
consider m1 being
Nat such that A77:
n0 + 1
= (m0 + 1) + m1
by A76, NAT_1:10;
A78:
(s1 / (1 + s1)) |^ (n0 + 1) = ((s1 / (1 + s1)) |^ (m0 + 1)) * ((s1 / (1 + s1)) |^ m1)
by A77, NEWTON:13;
A79:
1
|^ m1 = 1
by NEWTON:15;
(
0 < (s1 / (1 + s1)) |^ (m0 + 1) &
(s1 / (1 + s1)) |^ m1 <= 1
|^ m1 )
by A23, A20, NEWTON:102, PREPOWER:17;
then
(s1 / (1 + s1)) |^ (n0 + 1) <= (s1 / (1 + s1)) |^ (m0 + 1)
by A78, A79, XREAL_1:155;
then
((s1 / (1 + s1)) GeoSeq ) . (n0 + 1) <= (s1 / (1 + s1)) |^ (m0 + 1)
by PREPOWER:def 1;
then
((s1 / (1 + s1)) GeoSeq ) . (n0 + 1) <= ((s1 / (1 + s1)) GeoSeq ) . (m0 + 1)
by PREPOWER:def 1;
then
(((s1 / (1 + s1)) GeoSeq ) . (n0 + 1)) * r <= (((s1 / (1 + s1)) GeoSeq ) . (m0 + 1)) * r
by A1, XREAL_1:66;
then
||.((T . (xn . n)) - y).|| <= (((s1 / (1 + s1)) GeoSeq ) . (m0 + 1)) * r
by A40, XXREAL_0:2;
then
||.((T . (xn . n)) - y).|| < s
by A75, XXREAL_0:2;
hence
||.(((T /* xn) . n) - y).|| < s
by A70;
verum end; hence
for
n being
Element of
NAT st
m <= n holds
||.(((T /* xn) . n) - y).|| < s
;
verum end;
T is_continuous_in lim xn
by LOPBAN_5:4;
then
(
T /* xn is
convergent &
T /. (lim xn) = lim (T /* xn) )
by A67, A69, NFCONT_1:def 9;
then
y = T . (lim xn)
by A71, NORMSP_1:def 11;
hence
z in T .: (Ball (0. X),(1 + s0))
by A68, FUNCT_2:43;
verum end;
hence
Ball (0. Y),
r c= T .: (Ball (0. X),(1 + s0))
by TARSKI:def 3;
verum
end;
now reconsider TB01 =
T .: (Ball (0. X),1) as
Subset of
Y ;
let z be
set ;
( z in Ball (0. Y),r implies z in T .: (Ball (0. X),1) )assume A80:
z in Ball (0. Y),
r
;
z in T .: (Ball (0. X),1)then reconsider y =
z as
Point of
Y ;
ex
yy1 being
Point of
Y st
(
y = yy1 &
||.((0. Y) - yy1).|| < r )
by A80;
then
||.(- y).|| < r
by RLVECT_1:27;
then A81:
||.y.|| < r
by NORMSP_1:6;
0 <= ||.y.||
by NORMSP_1:8;
then consider s0 being
real number such that A82:
0 < s0
and A83:
||.y.|| < r / (1 + s0)
and
r / (1 + s0) < r
by A81, Th1;
set y1 =
(1 + s0) * y;
(1 + s0) * ||.y.|| < (r / (1 + s0)) * (1 + s0)
by A82, A83, XREAL_1:70;
then
(1 + s0) * ||.y.|| < r
by A82, XCMPLX_1:88;
then
(abs (1 + s0)) * ||.y.|| < r
by A82, ABSVALUE:def 1;
then
||.((1 + s0) * y).|| < r
by NORMSP_1:def 2;
then
||.(- ((1 + s0) * y)).|| < r
by NORMSP_1:6;
then
||.((0. Y) - ((1 + s0) * y)).|| < r
by RLVECT_1:27;
then A84:
(1 + s0) * y in Ball (0. Y),
r
;
Ball (0. Y),
r c= T .: (Ball (0. X),(1 + s0))
by A15, A82;
then A85:
(1 + s0) * y in T .: (Ball (0. X),(1 + s0))
by A84;
reconsider s1 = 1
+ s0 as non
zero Real by A82;
s1 * (Ball (0. X),1) = Ball (0. X),
(s1 * 1)
by A82, Th3;
then
s1 * y in s1 * TB01
by A85, Th5;
then
(s1 " ) * (s1 * y) in (s1 " ) * (s1 * TB01)
;
then
((s1 " ) * s1) * y in (s1 " ) * (s1 * TB01)
by RLVECT_1:def 10;
then A86:
((s1 " ) * s1) * y in ((s1 " ) * s1) * TB01
by CONVEX1:37;
(s1 " ) * s1 =
(1 / s1) * s1
by XCMPLX_1:217
.=
1
by XCMPLX_1:107
;
then
y in 1
* TB01
by A86, RLVECT_1:def 11;
hence
z in T .: (Ball (0. X),1)
by CONVEX1:32;
verumreconsider TB0s =
T .: (Ball (0. X),s1) as
Subset of
Y ;
end;
hence
BYr c= TBX1
by A2, A3, TARSKI:def 3; verum