let X be RealBanachSpace; :: thesis: 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 & BX1 = Ball (0. X),1 & BYr = Ball (0. Y),r & TBX1 = T .: (Ball (0. X),1) & BYr c= Cl TBX1 holds
BYr c= TBX1
let Y be RealNormSpace; :: thesis: 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 & BX1 = Ball (0. X),1 & 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; :: thesis: for r being real number
for BX1 being Subset of (LinearTopSpaceNorm X)
for TBX1, BYr being Subset of (LinearTopSpaceNorm Y) st r > 0 & BX1 = Ball (0. X),1 & BYr = Ball (0. Y),r & TBX1 = T .: (Ball (0. X),1) & BYr c= Cl TBX1 holds
BYr c= TBX1
let r be real number ; :: thesis: for BX1 being Subset of (LinearTopSpaceNorm X)
for TBX1, BYr being Subset of (LinearTopSpaceNorm Y) st r > 0 & BX1 = Ball (0. X),1 & 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); :: thesis: for TBX1, BYr being Subset of (LinearTopSpaceNorm Y) st r > 0 & BX1 = Ball (0. X),1 & 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); :: thesis: ( r > 0 & BX1 = Ball (0. X),1 & BYr = Ball (0. Y),r & TBX1 = T .: (Ball (0. X),1) & BYr c= Cl TBX1 implies BYr c= TBX1 )
assume AS0:
( r > 0 & BX1 = Ball (0. X),1 & BYr = Ball (0. Y),r & TBX1 = T .: (Ball (0. X),1) & BYr c= Cl TBX1 )
; :: thesis: BYr c= TBX1
A1:
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
let x be
Point of
X;
:: thesis: 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;
:: thesis: 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);
:: thesis: 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 ;
:: thesis: ( s > 0 & TB1 = T .: (Ball x,s) & y = T . x & BYsr = Ball y,(s * r) implies BYsr c= Cl TB1 )
assume A2:
(
s > 0 &
TB1 = T .: (Ball x,s) &
y = T . x &
BYsr = Ball y,
(s * r) )
;
:: thesis: BYsr c= Cl TB1
reconsider TB0 =
T .: (Ball (0. X),s) as
Subset of
(LinearTopSpaceNorm Y) by NORMSP_2:def 4;
reconsider x1 =
x as
Point of
(LinearTopSpaceNorm X) by NORMSP_2:def 4;
reconsider y1 =
y as
Point of
(LinearTopSpaceNorm Y) by NORMSP_2:def 4;
reconsider s1 =
s as non
zero Real by A2, XREAL_0:def 1;
s1 * BYr c= s1 * (Cl TBX1)
by AS0, 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 P1:
y1 + (s1 * BYr) c= Cl (y1 + (s1 * TBX1))
by RLTOPSP1:39;
Q1:
Ball y,
(s * r) = y + (Ball (0. Y),(s * r))
by Lm01;
Ball (0. Y),
(s * r) = s1 * (Ball (0. Y),r)
by A2, Lm02;
then
Ball (0. Y),
(s * r) = s1 * BYr
by Lm06, AS0;
then P2:
y1 + (s1 * BYr) = BYsr
by A2, Q1, Lm05;
reconsider TB0s =
T .: (Ball (0. X),s) as
Subset of
Y ;
reconsider TB01 =
T .: (Ball (0. X),1) as
Subset of
Y ;
reconsider TB0xs =
T .: (Ball x,s) as
Subset of
Y ;
Ball x,
s = x + (Ball (0. X),s)
by Lm01;
then Q3:
y + TB0s = TB0xs
by A2, Lm03;
Q4:
s1 * TB01 = s1 * TBX1
by AS0, Lm06;
s1 * (Ball (0. X),1) = Ball (0. X),
(s1 * 1)
by A2, Lm02;
hence
BYsr c= Cl TB1
by P1, P2, Q3, A2, Lm05, Q4, Lm032;
:: thesis: verum
end;
B1:
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 ;
:: thesis: ( s0 > 0 implies Ball (0. Y),r c= T .: (Ball (0. X),(1 + s0)) )
assume C1:
s0 > 0
;
:: thesis: Ball (0. Y),r c= T .: (Ball (0. X),(1 + s0))
now let z be
set ;
:: thesis: ( z in Ball (0. Y),r implies z in T .: (Ball (0. X),(1 + s0)) )assume C2:
z in Ball (0. Y),
r
;
:: thesis: z in T .: (Ball (0. X),(1 + s0))then reconsider y =
z as
Point of
Y ;
consider s1 being
real number such that C21:
(
0 < s1 &
s1 < s0 )
by C1, XREAL_1:7;
set a =
s1 / (1 + s1);
set e =
(s1 / (1 + s1)) GeoSeq ;
C23:
0 < s1 / (1 + s1)
by C21, XREAL_1:141;
C24:
s1 / (1 + s1) < 1
by C21, XREAL_1:31, XREAL_1:193;
then
abs (s1 / (1 + s1)) < 1
by C21, ABSVALUE:def 1;
then C3:
(
(s1 / (1 + s1)) GeoSeq is
summable &
Sum ((s1 / (1 + s1)) GeoSeq ) = 1
/ (1 - (s1 / (1 + s1))) )
by SERIES_1:28;
C4:
Sum ((s1 / (1 + s1)) GeoSeq ) < 1
+ s0
C5:
((s1 / (1 + s1)) GeoSeq ) . 0 = 1
by PREPOWER:4;
reconsider B0 =
Ball y,
((((s1 / (1 + s1)) GeoSeq ) . 1) * r) as
Subset of
(LinearTopSpaceNorm Y) by NORMSP_2:def 4;
A13:
B0 is
open
by NORMSP_2:23;
CK1:
((s1 / (1 + s1)) GeoSeq ) . 1
= (s1 / (1 + s1)) |^ 1
by PREPOWER:def 1;
CK2:
0 < (s1 / (1 + s1)) |^ 1
by C23, NEWTON:102;
CK3:
0 < (((s1 / (1 + s1)) GeoSeq ) . 1) * r
by CK1, CK2, AS0, XREAL_1:131;
||.(y - y).|| < (((s1 / (1 + s1)) GeoSeq ) . 1) * r
by CK3, NORMSP_1:10;
then A14:
y in B0
;
Ball y,
((((s1 / (1 + s1)) GeoSeq ) . 1) * r) meets TBX1
by AS0, C2, A13, A14, PRE_TOPC:def 13;
then consider s being
set such that C600:
(
s in Ball y,
((((s1 / (1 + s1)) GeoSeq ) . 1) * r) &
s in T .: (Ball (0. X),1) )
by AS0, XBOOLE_0:3;
consider xn1 being
set such that C601:
(
xn1 in the
carrier of
X &
xn1 in Ball (0. X),1 &
s = T . xn1 )
by C600, FUNCT_2:115;
reconsider xn1 =
xn1 as
Point of
X by C601;
reconsider sb =
T . xn1 as
Point of
Y ;
CS1:
ex
ss1 being
Point of
Y st
(
sb = ss1 &
||.(y - ss1).|| < (((s1 / (1 + s1)) GeoSeq ) . 1) * r )
by C600, C601;
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 ) );
C6:
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 ;
:: thesis: 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;
:: thesis: ex z being Point of X st S1[n,v,w,z]
now assume CAS1:
(
w in Ball v,
(((s1 / (1 + s1)) GeoSeq ) . n) &
||.((T . w) - y).|| < (((s1 / (1 + s1)) GeoSeq ) . (n + 1)) * r )
;
:: thesis: 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 )CX1:
((s1 / (1 + s1)) GeoSeq ) . (n + 1) = (s1 / (1 + s1)) |^ (n + 1)
by PREPOWER:def 1;
reconsider TB1 =
T .: (Ball w,(((s1 / (1 + s1)) GeoSeq ) . (n + 1))) 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;
A12:
BYsr c= Cl TB1
by CX1, C23, A1, NEWTON:102;
reconsider B0 =
Ball y,
((((s1 / (1 + s1)) GeoSeq ) . (n + 2)) * r) as
Subset of
(LinearTopSpaceNorm Y) by NORMSP_2:def 4;
A13:
B0 is
open
by NORMSP_2:23;
CK1:
((s1 / (1 + s1)) GeoSeq ) . (n + 2) = (s1 / (1 + s1)) |^ (n + 2)
by PREPOWER:def 1;
CK2:
0 < (s1 / (1 + s1)) |^ (n + 2)
by C23, NEWTON:102;
0 < (((s1 / (1 + s1)) GeoSeq ) . (n + 2)) * r
by CK1, CK2, AS0, XREAL_1:131;
then
||.(y - y).|| < (((s1 / (1 + s1)) GeoSeq ) . (n + 2)) * r
by NORMSP_1:10;
then A14:
y in B0
;
y in BYsr
by CAS1;
then
Ball y,
((((s1 / (1 + s1)) GeoSeq ) . (n + 2)) * r) meets TB1
by A12, A13, A14, PRE_TOPC:def 13;
then consider s being
set such that C61:
(
s in Ball y,
((((s1 / (1 + s1)) GeoSeq ) . (n + 2)) * r) &
s in T .: (Ball w,(((s1 / (1 + s1)) GeoSeq ) . (n + 1))) )
by XBOOLE_0:3;
consider z being
set such that C62:
(
z in the
carrier of
X &
z in Ball w,
(((s1 / (1 + s1)) GeoSeq ) . (n + 1)) &
s = T . z )
by C61, FUNCT_2:115;
reconsider z =
z as
Point of
X by C62;
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 C61, C62;
then
(
z in Ball w,
(((s1 / (1 + s1)) GeoSeq ) . (n + 1)) &
||.((T . z) - y).|| < (((s1 / (1 + s1)) GeoSeq ) . (n + 2)) * r )
by C62, 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 )
;
:: thesis: verum end;
hence
ex
z being
Point of
X st
S1[
n,
v,
w,
z]
;
:: thesis: verum
end; consider xn being
sequence of
X such that C7:
(
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(C6);
C70:
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 )
C800:
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)))
then
xn is
CCauchy
by LOPBAN_3:5;
then C9:
xn is
convergent
by LOPBAN_1:def 16;
set xx =
lim xn;
C91:
(
||.xn.|| is
convergent &
lim ||.xn.|| = ||.(lim xn).|| )
by C9, LOPBAN_1:47;
for
k being
Element of
NAT st
0 <= k holds
||.xn.|| . k <= 1
/ (1 - (s1 / (1 + s1)))
then
||.(lim xn).|| <= Sum ((s1 / (1 + s1)) GeoSeq )
by C3, C91, RSSPACE2:6;
then
||.(lim xn).|| < 1
+ s0
by C4, XXREAL_0:2;
then
||.(- (lim xn)).|| < 1
+ s0
by NORMSP_1:6;
then
||.((0. X) - (lim xn)).|| < 1
+ s0
by RLVECT_1:27;
then C11:
lim xn in Ball (0. X),
(1 + s0)
;
rng xn c= the
carrier of
X
;
then C1200:
rng xn c= dom T
by FUNCT_2:def 1;
T is_continuous_in lim xn
by LOPBAN_5:4;
then C1220:
(
T /* xn is
convergent &
T /. (lim xn) = lim (T /* xn) )
by C1200, C9, NFCONT_1:def 9;
now let s be
Real;
:: thesis: ( 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 A1:
0 < s
;
:: thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(((T /* xn) . n) - y).|| < sA2:
0 < s / r
by AS0, A1, XREAL_1:141;
KK1:
(
(s1 / (1 + s1)) GeoSeq is
convergent &
lim ((s1 / (1 + s1)) GeoSeq ) = 0 )
by C3, SERIES_1:7;
consider m0 being
Element of
NAT such that KK2:
for
n being
Element of
NAT st
m0 <= n holds
abs ((((s1 / (1 + s1)) GeoSeq ) . n) - 0 ) < s / r
by A2, KK1, SEQ_2:def 7;
abs ((((s1 / (1 + s1)) GeoSeq ) . m0) - 0 ) < s / r
by KK2;
then KK4:
((s1 / (1 + s1)) GeoSeq ) . m0 < 0 + (s / r)
by RINFSUP1:1;
MB6:
(
0 < (s1 / (1 + s1)) |^ 1 &
(s1 / (1 + s1)) |^ 1
< 1 )
by C23, C24, NEWTON:10;
0 < (s1 / (1 + s1)) |^ m0
by C23, NEWTON:102;
then
((s1 / (1 + s1)) |^ m0) * ((s1 / (1 + s1)) |^ 1) <= (s1 / (1 + s1)) |^ m0
by MB6, 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
((s1 / (1 + s1)) GeoSeq ) . (m0 + 1) <= ((s1 / (1 + s1)) GeoSeq ) . m0
by PREPOWER:def 1;
then
((s1 / (1 + s1)) GeoSeq ) . (m0 + 1) < s / r
by KK4, XXREAL_0:2;
then
(((s1 / (1 + s1)) GeoSeq ) . (m0 + 1)) * r < (s / r) * r
by AS0, XREAL_1:70;
then A2:
(((s1 / (1 + s1)) GeoSeq ) . (m0 + 1)) * r < s
by AS0, XCMPLX_1:88;
take m =
m0 + 1;
:: thesis: for n being Element of NAT st m <= n holds
||.(((T /* xn) . n) - y).|| < snow let n be
Element of
NAT ;
:: thesis: ( m <= n implies ||.(((T /* xn) . n) - y).|| < s )assume A3:
m <= n
;
:: thesis: ||.(((T /* xn) . n) - y).|| < s
1
<= m0 + 1
by NAT_1:11;
then reconsider n0 =
n - 1 as
Element of
NAT by A3, NAT_1:21, XXREAL_0:2;
consider m1 being
Nat such that AB1:
n0 + 1
= (m0 + 1) + m1
by A3, NAT_1:10;
AB2:
(s1 / (1 + s1)) |^ (n0 + 1) = ((s1 / (1 + s1)) |^ (m0 + 1)) * ((s1 / (1 + s1)) |^ m1)
by AB1, NEWTON:13;
AB3:
(
0 < (s1 / (1 + s1)) |^ (m0 + 1) &
0 < (s1 / (1 + s1)) |^ m1 )
by C23, NEWTON:102;
AL1:
(s1 / (1 + s1)) |^ m1 <= 1
|^ m1
by C23, C24, PREPOWER:17;
1
|^ m1 = 1
by NEWTON:15;
then
(s1 / (1 + s1)) |^ (n0 + 1) <= (s1 / (1 + s1)) |^ (m0 + 1)
by AB2, AB3, AL1, 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 A5:
(((s1 / (1 + s1)) GeoSeq ) . (n0 + 1)) * r <= (((s1 / (1 + s1)) GeoSeq ) . (m0 + 1)) * r
by AS0, XREAL_1:66;
||.((T . (xn . n)) - y).|| <= (((s1 / (1 + s1)) GeoSeq ) . (m0 + 1)) * r
by A5, C70, XXREAL_0:2;
then
||.((T . (xn . n)) - y).|| < s
by A2, XXREAL_0:2;
hence
||.(((T /* xn) . n) - y).|| < s
by C123;
:: thesis: verum end; hence
for
n being
Element of
NAT st
m <= n holds
||.(((T /* xn) . n) - y).|| < s
;
:: thesis: verum end; then
y = T . (lim xn)
by C1220, NORMSP_1:def 11;
hence
z in T .: (Ball (0. X),(1 + s0))
by C11, FUNCT_2:43;
:: thesis: verum end;
hence
Ball (0. Y),
r c= T .: (Ball (0. X),(1 + s0))
by TARSKI:def 3;
:: thesis: verum
end;
now let z be
set ;
:: thesis: ( z in Ball (0. Y),r implies z in T .: (Ball (0. X),1) )assume R1:
z in Ball (0. Y),
r
;
:: thesis: 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 R1;
then
||.(- y).|| < r
by RLVECT_1:27;
then R2:
||.y.|| < r
by NORMSP_1:6;
RX1:
0 <= ||.y.||
by NORMSP_1:8;
consider s0 being
real number such that RX2:
(
0 < s0 &
||.y.|| < r / (1 + s0) &
r / (1 + s0) < r )
by R2, RX1, Lm00;
(1 + s0) * ||.y.|| < (r / (1 + s0)) * (1 + s0)
by RX2, XREAL_1:70;
then
(1 + s0) * ||.y.|| < r
by RX2, XCMPLX_1:88;
then
(abs (1 + s0)) * ||.y.|| < r
by RX2, ABSVALUE:def 1;
then R3:
||.((1 + s0) * y).|| < r
by NORMSP_1:def 2;
set y1 =
(1 + s0) * y;
||.(- ((1 + s0) * y)).|| < r
by R3, NORMSP_1:6;
then
||.((0. Y) - ((1 + s0) * y)).|| < r
by RLVECT_1:27;
then R4:
(1 + s0) * y in Ball (0. Y),
r
;
Ball (0. Y),
r c= T .: (Ball (0. X),(1 + s0))
by B1, RX2;
then R5:
(1 + s0) * y in T .: (Ball (0. X),(1 + s0))
by R4;
reconsider s1 = 1
+ s0 as non
zero Real by RX2;
reconsider TB0s =
T .: (Ball (0. X),s1) as
Subset of
Y ;
reconsider TB01 =
T .: (Ball (0. X),1) as
Subset of
Y ;
s1 * (Ball (0. X),1) = Ball (0. X),
(s1 * 1)
by RX2, Lm02;
then
s1 * y in s1 * TB01
by R5, Lm032;
then
(s1 " ) * (s1 * y) in (s1 " ) * (s1 * TB01)
;
then
((s1 " ) * s1) * y in (s1 " ) * (s1 * TB01)
by RLVECT_1:def 9;
then LN1:
((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 LN1, RLVECT_1:def 9;
hence
z in T .: (Ball (0. X),1)
by CONVEX1:32;
:: thesis: verum end;
hence
BYr c= TBX1
by AS0, TARSKI:def 3; :: thesis: verum