:: LOPBAN_5 semantic presentation
begin
theorem Th1: :: LOPBAN_5:1
for seq being Real_Sequence
for r being Real st seq is bounded & 0 <= r holds
lim_inf (r (#) seq) = r * (lim_inf seq)
proof
let seq be Real_Sequence; ::_thesis: for r being Real st seq is bounded & 0 <= r holds
lim_inf (r (#) seq) = r * (lim_inf seq)
let r be Real; ::_thesis: ( seq is bounded & 0 <= r implies lim_inf (r (#) seq) = r * (lim_inf seq) )
assume that
A1: seq is bounded and
A2: 0 <= r ; ::_thesis: lim_inf (r (#) seq) = r * (lim_inf seq)
inferior_realsequence seq in Funcs (NAT,REAL) by FUNCT_2:8;
then A3: ex f being Function st
( inferior_realsequence seq = f & dom f = NAT & rng f c= REAL ) by FUNCT_2:def_2;
(inferior_realsequence seq) . 0 in rng (inferior_realsequence seq) by FUNCT_2:4;
then reconsider X1 = rng (inferior_realsequence seq) as non empty Subset of REAL by A3;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(inferior_realsequence_(r_(#)_seq))_._n_=_(r_(#)_(inferior_realsequence_seq))_._n
let n be Element of NAT ; ::_thesis: (inferior_realsequence (r (#) seq)) . n = (r (#) (inferior_realsequence seq)) . n
consider r1 being real number such that
A4: 0 < r1 and
A5: for k being Element of NAT holds abs (seq . k) < r1 by A1, SEQ_2:3;
seq ^\ n in Funcs (NAT,REAL) by FUNCT_2:8;
then ex f being Function st
( seq ^\ n = f & dom f = NAT & rng f c= REAL ) by FUNCT_2:def_2;
then reconsider Y1 = rng (seq ^\ n) as non empty Subset of REAL by FUNCT_2:4;
now__::_thesis:_for_k_being_Element_of_NAT_holds_abs_((seq_^\_n)_._k)_<_r1
let k be Element of NAT ; ::_thesis: abs ((seq ^\ n) . k) < r1
abs ((seq ^\ n) . k) = abs (seq . (n + k)) by NAT_1:def_3;
hence abs ((seq ^\ n) . k) < r1 by A5; ::_thesis: verum
end;
then seq ^\ n is bounded by A4, SEQ_2:3;
then A6: Y1 is bounded_below by RINFSUP1:6;
(inferior_realsequence (r (#) seq)) . n = lower_bound ((r (#) seq) ^\ n) by RINFSUP1:36
.= lower_bound (r (#) (seq ^\ n)) by SEQM_3:21
.= lower_bound (r ** Y1) by INTEGRA2:17
.= r * (lower_bound (seq ^\ n)) by A2, A6, INTEGRA2:15
.= r * ((inferior_realsequence seq) . n) by RINFSUP1:36 ;
hence (inferior_realsequence (r (#) seq)) . n = (r (#) (inferior_realsequence seq)) . n by SEQ_1:9; ::_thesis: verum
end;
then inferior_realsequence (r (#) seq) = r (#) (inferior_realsequence seq) by FUNCT_2:63;
then A7: rng (inferior_realsequence (r (#) seq)) = r ** X1 by INTEGRA2:17;
inferior_realsequence seq is bounded by A1, RINFSUP1:56;
then X1 is bounded_above by RINFSUP1:5;
hence lim_inf (r (#) seq) = r * (lim_inf seq) by A2, A7, INTEGRA2:13; ::_thesis: verum
end;
theorem :: LOPBAN_5:2
for seq being Real_Sequence
for r being Real st seq is bounded & 0 <= r holds
lim_sup (r (#) seq) = r * (lim_sup seq)
proof
let seq be Real_Sequence; ::_thesis: for r being Real st seq is bounded & 0 <= r holds
lim_sup (r (#) seq) = r * (lim_sup seq)
let r be Real; ::_thesis: ( seq is bounded & 0 <= r implies lim_sup (r (#) seq) = r * (lim_sup seq) )
assume that
A1: seq is bounded and
A2: 0 <= r ; ::_thesis: lim_sup (r (#) seq) = r * (lim_sup seq)
superior_realsequence seq in Funcs (NAT,REAL) by FUNCT_2:8;
then A3: ex f being Function st
( superior_realsequence seq = f & dom f = NAT & rng f c= REAL ) by FUNCT_2:def_2;
(superior_realsequence seq) . 0 in rng (superior_realsequence seq) by FUNCT_2:4;
then reconsider X1 = rng (superior_realsequence seq) as non empty Subset of REAL by A3;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(superior_realsequence_(r_(#)_seq))_._n_=_(r_(#)_(superior_realsequence_seq))_._n
let n be Element of NAT ; ::_thesis: (superior_realsequence (r (#) seq)) . n = (r (#) (superior_realsequence seq)) . n
consider r1 being real number such that
A4: 0 < r1 and
A5: for k being Element of NAT holds abs (seq . k) < r1 by A1, SEQ_2:3;
seq ^\ n in Funcs (NAT,REAL) by FUNCT_2:8;
then ex f being Function st
( seq ^\ n = f & dom f = NAT & rng f c= REAL ) by FUNCT_2:def_2;
then reconsider Y1 = rng (seq ^\ n) as non empty Subset of REAL by FUNCT_2:4;
now__::_thesis:_for_k_being_Element_of_NAT_holds_abs_((seq_^\_n)_._k)_<_r1
let k be Element of NAT ; ::_thesis: abs ((seq ^\ n) . k) < r1
abs ((seq ^\ n) . k) = abs (seq . (n + k)) by NAT_1:def_3;
hence abs ((seq ^\ n) . k) < r1 by A5; ::_thesis: verum
end;
then seq ^\ n is bounded by A4, SEQ_2:3;
then A6: Y1 is bounded_above by RINFSUP1:5;
(superior_realsequence (r (#) seq)) . n = upper_bound ((r (#) seq) ^\ n) by RINFSUP1:37
.= upper_bound (r (#) (seq ^\ n)) by SEQM_3:21
.= upper_bound (r ** Y1) by INTEGRA2:17
.= r * (upper_bound (seq ^\ n)) by A2, A6, INTEGRA2:13
.= r * ((superior_realsequence seq) . n) by RINFSUP1:37 ;
hence (superior_realsequence (r (#) seq)) . n = (r (#) (superior_realsequence seq)) . n by SEQ_1:9; ::_thesis: verum
end;
then superior_realsequence (r (#) seq) = r (#) (superior_realsequence seq) by FUNCT_2:63;
then A7: rng (superior_realsequence (r (#) seq)) = r ** X1 by INTEGRA2:17;
superior_realsequence seq is bounded by A1, RINFSUP1:56;
then X1 is bounded_below by RINFSUP1:6;
hence lim_sup (r (#) seq) = r * (lim_sup seq) by A2, A7, INTEGRA2:15; ::_thesis: verum
end;
registration
let X be RealBanachSpace;
cluster MetricSpaceNorm X -> complete ;
coherence
MetricSpaceNorm X is complete
proof
now__::_thesis:_for_S1_being_sequence_of_(MetricSpaceNorm_X)_st_S1_is_Cauchy_holds_
S1_is_convergent
let S1 be sequence of (MetricSpaceNorm X); ::_thesis: ( S1 is Cauchy implies S1 is convergent )
reconsider S2 = S1 as sequence of X ;
assume A1: S1 is Cauchy ; ::_thesis: S1 is convergent
S2 is Cauchy_sequence_by_Norm
proof
let r be Real; :: according to RSSPACE3:def_5 ::_thesis: ( r <= 0 or ex b1 being Element of NAT st
for b2, b3 being Element of NAT holds
( not b1 <= b2 or not b1 <= b3 or not r <= dist ((S2 . b2),(S2 . b3)) ) )
assume r > 0 ; ::_thesis: ex b1 being Element of NAT st
for b2, b3 being Element of NAT holds
( not b1 <= b2 or not b1 <= b3 or not r <= dist ((S2 . b2),(S2 . b3)) )
then consider p being Element of NAT such that
A2: for n, m being Element of NAT st p <= n & p <= m holds
dist ((S1 . n),(S1 . m)) < r by A1, TBSP_1:def_4;
now__::_thesis:_for_n,_m_being_Element_of_NAT_st_p_<=_n_&_p_<=_m_holds_
dist_((S2_._n),(S2_._m))_<_r
let n, m be Element of NAT ; ::_thesis: ( p <= n & p <= m implies dist ((S2 . n),(S2 . m)) < r )
assume ( p <= n & p <= m ) ; ::_thesis: dist ((S2 . n),(S2 . m)) < r
then dist ((S1 . n),(S1 . m)) < r by A2;
hence dist ((S2 . n),(S2 . m)) < r by NORMSP_2:def_1; ::_thesis: verum
end;
hence ex b1 being Element of NAT st
for b2, b3 being Element of NAT holds
( not b1 <= b2 or not b1 <= b3 or not r <= dist ((S2 . b2),(S2 . b3)) ) ; ::_thesis: verum
end;
then S2 is convergent by LOPBAN_1:def_15;
hence S1 is convergent by NORMSP_2:5; ::_thesis: verum
end;
hence MetricSpaceNorm X is complete by TBSP_1:def_5; ::_thesis: verum
end;
end;
definition
let X be RealNormSpace;
let x0 be Point of X;
let r be real number ;
func Ball (x0,r) -> Subset of X equals :: LOPBAN_5:def 1
{ x where x is Point of X : ||.(x0 - x).|| < r } ;
coherence
{ x where x is Point of X : ||.(x0 - x).|| < r } is Subset of X
proof
defpred S1[ Point of X] means ||.(x0 - $1).|| < r;
{ y where y is Point of X : S1[y] } c= the carrier of X from FRAENKEL:sch_10();
hence { x where x is Point of X : ||.(x0 - x).|| < r } is Subset of X ; ::_thesis: verum
end;
end;
:: deftheorem defines Ball LOPBAN_5:def_1_:_
for X being RealNormSpace
for x0 being Point of X
for r being real number holds Ball (x0,r) = { x where x is Point of X : ||.(x0 - x).|| < r } ;
theorem Th3: :: LOPBAN_5:3
for X being RealBanachSpace
for Y being SetSequence of X st union (rng Y) = the carrier of X & ( for n being Element of NAT holds Y . n is closed ) holds
ex n0 being Element of NAT ex r being Real ex x0 being Point of X st
( 0 < r & Ball (x0,r) c= Y . n0 )
proof
let X be RealBanachSpace; ::_thesis: for Y being SetSequence of X st union (rng Y) = the carrier of X & ( for n being Element of NAT holds Y . n is closed ) holds
ex n0 being Element of NAT ex r being Real ex x0 being Point of X st
( 0 < r & Ball (x0,r) c= Y . n0 )
let Y be SetSequence of X; ::_thesis: ( union (rng Y) = the carrier of X & ( for n being Element of NAT holds Y . n is closed ) implies ex n0 being Element of NAT ex r being Real ex x0 being Point of X st
( 0 < r & Ball (x0,r) c= Y . n0 ) )
assume that
A1: union (rng Y) = the carrier of X and
A2: for n being Element of NAT holds Y . n is closed ; ::_thesis: ex n0 being Element of NAT ex r being Real ex x0 being Point of X st
( 0 < r & Ball (x0,r) c= Y . n0 )
now__::_thesis:_for_n_being_Element_of_NAT_holds_(Y_._n)_`_in_Family_open_set_(MetricSpaceNorm_X)
let n be Element of NAT ; ::_thesis: (Y . n) ` in Family_open_set (MetricSpaceNorm X)
reconsider Yn = Y . n as Subset of (TopSpaceNorm X) ;
Y . n is closed by A2;
then Yn is closed by NORMSP_2:15;
then Yn ` is open by TOPS_1:3;
hence (Y . n) ` in Family_open_set (MetricSpaceNorm X) by PRE_TOPC:def_2; ::_thesis: verum
end;
then consider n0 being Element of NAT , r being Real, xx0 being Point of (MetricSpaceNorm X) such that
A3: ( 0 < r & Ball (xx0,r) c= Y . n0 ) by A1, NORMSP_2:1;
consider x0 being Point of X such that
x0 = xx0 and
A4: Ball (xx0,r) = { x where x is Point of X : ||.(x0 - x).|| < r } by NORMSP_2:2;
Ball (x0,r) = { x where x is Point of X : ||.(x0 - x).|| < r } ;
hence ex n0 being Element of NAT ex r being Real ex x0 being Point of X st
( 0 < r & Ball (x0,r) c= Y . n0 ) by A3, A4; ::_thesis: verum
end;
theorem Th4: :: LOPBAN_5:4
for X, Y being RealNormSpace
for f being Lipschitzian LinearOperator of X,Y holds
( f is_Lipschitzian_on the carrier of X & f is_continuous_on the carrier of X & ( for x being Point of X holds f is_continuous_in x ) )
proof
let X, Y be RealNormSpace; ::_thesis: for f being Lipschitzian LinearOperator of X,Y holds
( f is_Lipschitzian_on the carrier of X & f is_continuous_on the carrier of X & ( for x being Point of X holds f is_continuous_in x ) )
let f be Lipschitzian LinearOperator of X,Y; ::_thesis: ( f is_Lipschitzian_on the carrier of X & f is_continuous_on the carrier of X & ( for x being Point of X holds f is_continuous_in x ) )
consider K being Real such that
A1: 0 <= K and
A2: for x being VECTOR of X holds ||.(f . x).|| <= K * ||.x.|| by LOPBAN_1:def_8;
A3: now__::_thesis:_for_x,_y_being_Point_of_X_st_x_in_the_carrier_of_X_&_y_in_the_carrier_of_X_holds_
||.((f_/._x)_-_(f_/._y)).||_<=_(K_+_1)_*_||.(x_-_y).||
let x, y be Point of X; ::_thesis: ( x in the carrier of X & y in the carrier of X implies ||.((f /. x) - (f /. y)).|| <= (K + 1) * ||.(x - y).|| )
assume that
x in the carrier of X and
y in the carrier of X ; ::_thesis: ||.((f /. x) - (f /. y)).|| <= (K + 1) * ||.(x - y).||
(f /. x) - (f /. y) = (f . x) + ((- 1) * (f . y)) by RLVECT_1:16;
then (f /. x) - (f /. y) = (f . x) + (f . ((- 1) * y)) by LOPBAN_1:def_5;
then (f /. x) - (f /. y) = f . (x + ((- 1) * y)) by VECTSP_1:def_20;
then A4: (f /. x) - (f /. y) = f . (x + (- y)) by RLVECT_1:16;
||.((f /. x) - (f /. y)).|| <= (K * ||.(x - y).||) + ||.(x - y).|| by A2, A4, XREAL_1:38;
hence ||.((f /. x) - (f /. y)).|| <= (K + 1) * ||.(x - y).|| ; ::_thesis: verum
end;
dom f = the carrier of X by FUNCT_2:def_1;
hence f is_Lipschitzian_on the carrier of X by A1, A3, NFCONT_1:def_9; ::_thesis: ( f is_continuous_on the carrier of X & ( for x being Point of X holds f is_continuous_in x ) )
hence A5: f is_continuous_on the carrier of X by NFCONT_1:45; ::_thesis: for x being Point of X holds f is_continuous_in x
hereby ::_thesis: verum
let x be Point of X; ::_thesis: f is_continuous_in x
f | the carrier of X = f by RELSET_1:19;
hence f is_continuous_in x by A5, NFCONT_1:def_7; ::_thesis: verum
end;
end;
theorem Th5: :: LOPBAN_5:5
for X being 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 ) )
proof
let X be RealBanachSpace; ::_thesis: 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; ::_thesis: 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)); ::_thesis: ( ( 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 ) ) ; ::_thesis: 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 ) )
percases ( T <> {} or T = {} ) ;
supposeA2: T <> {} ; ::_thesis: 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 Lipschitzian 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]
proof
let x be Point of X; ::_thesis: ex y being Element of bool REAL st S1[x,y]
take y = { ||.(f . x).|| where f is Lipschitzian LinearOperator of X,Y : f in T } ; ::_thesis: ( y is Element of bool REAL & S1[x,y] )
now__::_thesis:_for_z_being_set_st_z_in_y_holds_
z_in_REAL
let z be set ; ::_thesis: ( z in y implies z in REAL )
assume z in y ; ::_thesis: z in REAL
then ex f being Lipschitzian LinearOperator of X,Y st
( z = ||.(f . x).|| & f in T ) ;
hence z in REAL ; ::_thesis: verum
end;
hence ( y is Element of bool REAL & S1[x,y] ) by TARSKI:def_3; ::_thesis: verum
end;
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 Lipschitzian 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]
proof
let n be Element of NAT ; ::_thesis: ex y being Element of bool the carrier of X st S2[n,y]
take y = { x where x is Point of X : ( Ta . x is bounded_above & upper_bound (Ta . x) <= n ) } ; ::_thesis: ( y is Element of bool the carrier of X & S2[n,y] )
now__::_thesis:_for_z_being_set_st_z_in_y_holds_
z_in_the_carrier_of_X
let z be set ; ::_thesis: ( z in y implies z in the carrier of X )
assume z in y ; ::_thesis: z in the carrier of X
then ex x being Point of X st
( z = x & Ta . x is bounded_above & upper_bound (Ta . x) <= n ) ;
hence z in the carrier of X ; ::_thesis: verum
end;
hence ( y is Element of bool the carrier of X & S2[n,y] ) by TARSKI:def_3; ::_thesis: verum
end;
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)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of X or x in union (rng Xn) )
assume x in the carrier of X ; ::_thesis: x in union (rng Xn)
then reconsider x1 = x as Point of X ;
consider KTx1 being real number such that
0 <= KTx1 and
A8: for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.(f . x1).|| <= KTx1 by A1;
A9: Ta . x1 = { ||.(f . x1).|| where f is Lipschitzian LinearOperator of X,Y : f in T } by A4;
A10: for p being real number st p in Ta . x1 holds
p <= KTx1
proof
let p be real number ; ::_thesis: ( p in Ta . x1 implies p <= KTx1 )
assume p in Ta . x1 ; ::_thesis: p <= KTx1
then ex f being Lipschitzian LinearOperator of X,Y st
( p = ||.(f . x1).|| & f in T ) by A9;
hence p <= KTx1 by A8; ::_thesis: verum
end;
KTx1 is UpperBound of Ta . x1
proof
let p be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not p in Ta . x1 or p <= KTx1 )
assume p in Ta . x1 ; ::_thesis: p <= KTx1
then ex f being Lipschitzian LinearOperator of X,Y st
( p = ||.(f . x1).|| & f in T ) by A9;
hence p <= KTx1 by A8; ::_thesis: verum
end;
then A11: Ta . x1 is bounded_above by XXREAL_2:def_10;
consider n being Element of NAT such that
A12: KTx1 < n by SEQ_4:3;
consider f being set such that
A13: f in T by A2, XBOOLE_0:def_1;
reconsider f = f as Lipschitzian LinearOperator of X,Y by A13, LOPBAN_1:def_9;
||.(f . x1).|| in Ta . x by A9, A13;
then upper_bound (Ta . x1) <= KTx1 by A10, SEQ_4:45;
then upper_bound (Ta . x1) <= n by A12, XXREAL_0:2;
then x1 in { z1 where z1 is Point of X : ( Ta . z1 is bounded_above & upper_bound (Ta . z1) <= n ) } by A11;
then x1 in Xn . n by A6;
then x1 in Union Xn by PROB_1:12;
hence x in union (rng Xn) ; ::_thesis: verum
end;
A14: for x being Point of X holds not Ta . x is empty
proof
let x be Point of X; ::_thesis: not Ta . x is empty
consider f0 being set such that
A15: f0 in T by A2, XBOOLE_0:def_1;
reconsider f0 = f0 as Lipschitzian LinearOperator of X,Y by A15, LOPBAN_1:def_9;
Ta . x = { ||.(f . x).|| where f is Lipschitzian LinearOperator of X,Y : f in T } by A4;
then ||.(f0 . x).|| in Ta . x by A15;
hence not Ta . x is empty ; ::_thesis: verum
end;
A16: for n being Element of NAT holds Xn . n is closed
proof
let n be Element of NAT ; ::_thesis: 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; ::_thesis: ( 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 ; ::_thesis: lim s1 in Xn . n
A19: Ta . (lim s1) = { ||.(f . (lim s1)).|| where f is Lipschitzian 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 ; ::_thesis: ( y in Ta . (lim s1) implies y <= n )
assume y in Ta . (lim s1) ; ::_thesis: y <= n
then consider f being Lipschitzian 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 ; ::_thesis: ||.(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 Lipschitzian 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; ::_thesis: 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; ::_thesis: 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; ::_thesis: verum
end;
hence Xn . n is closed by NFCONT_1:def_3; ::_thesis: verum
end;
consider f being set such that
A35: f in T by A2, XBOOLE_0:def_1;
reconsider f = f as Lipschitzian 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 Lipschitzian 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)
proof
let x be Point of X; ::_thesis: ( x <> 0. X implies ((r / (2 * ||.x.||)) * x) + x0 in H1(x0,r) )
reconsider x1 = (||.x.|| ") * x as Point of X ;
A42: ||.((r / 2) * x1).|| = (abs (r / 2)) * ||.x1.|| by NORMSP_1:def_1;
assume x <> 0. X ; ::_thesis: ((r / (2 * ||.x.||)) * x) + x0 in H1(x0,r)
then A43: ||.x.|| <> 0 by NORMSP_0:def_5;
||.((((r / (2 * ||.x.||)) * x) + x0) - x0).|| = ||.(((r / (2 * ||.x.||)) * x) + (x0 + (- x0))).|| by RLVECT_1:def_3;
then ||.((((r / (2 * ||.x.||)) * x) + x0) - x0).|| = ||.(((r / (2 * ||.x.||)) * x) + (0. X)).|| by RLVECT_1:5;
then ||.((((r / (2 * ||.x.||)) * x) + x0) - x0).|| = ||.((r / (2 * ||.x.||)) * x).|| by RLVECT_1:def_4;
then ||.((((r / (2 * ||.x.||)) * x) + x0) - x0).|| = ||.(((r / 2) / ||.x.||) * x).|| by XCMPLX_1:78;
then A44: ||.((((r / (2 * ||.x.||)) * x) + x0) - x0).|| = ||.((r / 2) * x1).|| by RLVECT_1:def_7;
A45: abs (||.x.|| ") = ||.x.|| " by ABSVALUE:def_1;
||.x1.|| = (abs (||.x.|| ")) * ||.x.|| by NORMSP_1:def_1;
then ||.x1.|| = 1 by A43, A45, XCMPLX_0:def_7;
then ||.((r / 2) * x1).|| = r / 2 by A36, A42, ABSVALUE:def_1;
then A46: ||.(x0 - (((r / (2 * ||.x.||)) * x) + x0)).|| = r / 2 by A44, NORMSP_1:7;
r / 2 < r by A36, XREAL_1:216;
hence ((r / (2 * ||.x.||)) * x) + x0 in H1(x0,r) by A46; ::_thesis: verum
end;
set M = upper_bound (Ta . x0);
take KT = (2 * ((upper_bound (Ta . x0)) + n0)) / r; ::_thesis: ( 0 <= KT & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.f.|| <= KT ) )
A47: for f being Lipschitzian 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 Lipschitzian LinearOperator of X,Y; ::_thesis: ( 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 ; ::_thesis: for x being Point of X st x in H1(x0,r) holds
||.(f . x).|| <= n0
let x be Point of X; ::_thesis: ( x in H1(x0,r) implies ||.(f . x).|| <= n0 )
assume x in H1(x0,r) ; ::_thesis: ||.(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 Lipschitzian 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; ::_thesis: verum
end;
A52: now__::_thesis:_for_f_being_Lipschitzian_LinearOperator_of_X,Y_st_f_in_T_holds_
for_k_being_real_number_st_k_in__{__||.(f_._x1).||_where_x1_is_Point_of_X_:_||.x1.||_<=_1__}__holds_
k_<=_KT
let f be Lipschitzian LinearOperator of X,Y; ::_thesis: ( 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 ; ::_thesis: for k being real number st k in { ||.(f . x1).|| where x1 is Point of X : ||.x1.|| <= 1 } holds
k <= KT
A54: 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; ::_thesis: ( 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 ; ::_thesis: ||.(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 Lipschitzian 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, VECTSP_1:def_20, 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.|| ; ::_thesis: verum
end;
A64: for x being Point of X holds ||.(f . x).|| <= KT * ||.x.||
proof
let x be Point of X; ::_thesis: ||.(f . x).|| <= KT * ||.x.||
now__::_thesis:_(_x_=_0._X_implies_||.(f_._x).||_<=_KT_*_||.x.||_)
assume A65: x = 0. X ; ::_thesis: ||.(f . x).|| <= KT * ||.x.||
then f . x = f . (0 * (0. X)) by RLVECT_1:10;
then f . x = 0 * (f . (0. X)) by LOPBAN_1:def_5;
then A66: f . x = 0. Y by RLVECT_1:10;
||.x.|| = 0 by A65;
hence ||.(f . x).|| <= KT * ||.x.|| by A66; ::_thesis: verum
end;
hence ||.(f . x).|| <= KT * ||.x.|| by A54; ::_thesis: verum
end;
thus for k being real number st k in { ||.(f . x1).|| where x1 is Point of X : ||.x1.|| <= 1 } holds
k <= KT ::_thesis: verum
proof
let k be real number ; ::_thesis: ( k in { ||.(f . x1).|| where x1 is Point of X : ||.x1.|| <= 1 } implies k <= KT )
assume k in { ||.(f . x1).|| where x1 is Point of X : ||.x1.|| <= 1 } ; ::_thesis: k <= KT
then consider x being Point of X such that
A67: ( k = ||.(f . x).|| & ||.x.|| <= 1 ) ;
( k <= KT * ||.x.|| & KT * ||.x.|| <= KT ) by A36, A40, A64, A67, XREAL_1:153;
hence k <= KT by XXREAL_0:2; ::_thesis: verum
end;
end;
for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.f.|| <= KT
proof
let f be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); ::_thesis: ( f in T implies ||.f.|| <= KT )
reconsider f1 = f as Lipschitzian LinearOperator of X,Y by LOPBAN_1:def_9;
assume f in T ; ::_thesis: ||.f.|| <= KT
then A68: for k being real number st k in PreNorms f1 holds
k <= KT by A52;
||.f.|| = upper_bound (PreNorms f1) by LOPBAN_1:30;
hence ||.f.|| <= KT by A68, SEQ_4:45; ::_thesis: verum
end;
hence ( 0 <= KT & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.f.|| <= KT ) ) by A36, A40; ::_thesis: verum
end;
supposeA69: T = {} ; ::_thesis: 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 ) )
take 0 ; ::_thesis: ( 0 <= 0 & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.f.|| <= 0 ) )
thus ( 0 <= 0 & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.f.|| <= 0 ) ) by A69; ::_thesis: verum
end;
end;
end;
definition
let X, Y be RealNormSpace;
let H be Function of NAT, the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y));
let x be Point of X;
funcH # x -> sequence of Y means :Def2: :: LOPBAN_5:def 2
for n being Element of NAT holds it . n = (H . n) . x;
existence
ex b1 being sequence of Y st
for n being Element of NAT holds b1 . n = (H . n) . x
proof
deffunc H1( Element of NAT ) -> Element of the carrier of Y = (H . $1) . x;
thus ex f being Function of NAT, the carrier of Y st
for n being Element of NAT holds f . n = H1(n) from FUNCT_2:sch_4(); ::_thesis: verum
end;
uniqueness
for b1, b2 being sequence of Y st ( for n being Element of NAT holds b1 . n = (H . n) . x ) & ( for n being Element of NAT holds b2 . n = (H . n) . x ) holds
b1 = b2
proof
let S1, S2 be sequence of Y; ::_thesis: ( ( for n being Element of NAT holds S1 . n = (H . n) . x ) & ( for n being Element of NAT holds S2 . n = (H . n) . x ) implies S1 = S2 )
assume that
A1: for n being Element of NAT holds S1 . n = (H . n) . x and
A2: for n being Element of NAT holds S2 . n = (H . n) . x ; ::_thesis: S1 = S2
now__::_thesis:_for_n_being_Element_of_NAT_holds_S1_._n_=_S2_._n
let n be Element of NAT ; ::_thesis: S1 . n = S2 . n
S1 . n = (H . n) . x by A1;
hence S1 . n = S2 . n by A2; ::_thesis: verum
end;
hence S1 = S2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines # LOPBAN_5:def_2_:_
for X, Y being RealNormSpace
for H being Function of NAT, the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for x being Point of X
for b5 being sequence of Y holds
( b5 = H # x iff for n being Element of NAT holds b5 . n = (H . n) . x );
theorem Th6: :: LOPBAN_5:6
for X being RealBanachSpace
for Y being RealNormSpace
for vseq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for tseq being Function of X,Y st ( for x being Point of X holds
( vseq # x is convergent & tseq . x = lim (vseq # x) ) ) holds
( tseq is Lipschitzian LinearOperator of X,Y & ( for x being Point of X holds ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) & ( for ttseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ttseq = tseq holds
||.ttseq.|| <= lim_inf ||.vseq.|| ) )
proof
let X be RealBanachSpace; ::_thesis: for Y being RealNormSpace
for vseq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for tseq being Function of X,Y st ( for x being Point of X holds
( vseq # x is convergent & tseq . x = lim (vseq # x) ) ) holds
( tseq is Lipschitzian LinearOperator of X,Y & ( for x being Point of X holds ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) & ( for ttseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ttseq = tseq holds
||.ttseq.|| <= lim_inf ||.vseq.|| ) )
let Y be RealNormSpace; ::_thesis: for vseq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for tseq being Function of X,Y st ( for x being Point of X holds
( vseq # x is convergent & tseq . x = lim (vseq # x) ) ) holds
( tseq is Lipschitzian LinearOperator of X,Y & ( for x being Point of X holds ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) & ( for ttseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ttseq = tseq holds
||.ttseq.|| <= lim_inf ||.vseq.|| ) )
let vseq be sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)); ::_thesis: for tseq being Function of X,Y st ( for x being Point of X holds
( vseq # x is convergent & tseq . x = lim (vseq # x) ) ) holds
( tseq is Lipschitzian LinearOperator of X,Y & ( for x being Point of X holds ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) & ( for ttseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ttseq = tseq holds
||.ttseq.|| <= lim_inf ||.vseq.|| ) )
let tseq be Function of X,Y; ::_thesis: ( ( for x being Point of X holds
( vseq # x is convergent & tseq . x = lim (vseq # x) ) ) implies ( tseq is Lipschitzian LinearOperator of X,Y & ( for x being Point of X holds ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) & ( for ttseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ttseq = tseq holds
||.ttseq.|| <= lim_inf ||.vseq.|| ) ) )
set T = rng vseq;
set RNS = R_NormSpace_of_BoundedLinearOperators (X,Y);
assume A1: for x being Point of X holds
( vseq # x is convergent & tseq . x = lim (vseq # x) ) ; ::_thesis: ( tseq is Lipschitzian LinearOperator of X,Y & ( for x being Point of X holds ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) & ( for ttseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ttseq = tseq holds
||.ttseq.|| <= lim_inf ||.vseq.|| ) )
A2: for x, y being Point of X holds tseq . (x + y) = (tseq . x) + (tseq . y)
proof
let x, y be Point of X; ::_thesis: tseq . (x + y) = (tseq . x) + (tseq . y)
A3: ( vseq # y is convergent & tseq . y = lim (vseq # y) ) by A1;
A4: tseq . (x + y) = lim (vseq # (x + y)) by A1;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(vseq_#_(x_+_y))_._n_=_((vseq_#_x)_._n)_+_((vseq_#_y)_._n)
let n be Element of NAT ; ::_thesis: (vseq # (x + y)) . n = ((vseq # x) . n) + ((vseq # y) . n)
( vseq . n is Lipschitzian LinearOperator of X,Y & (vseq # (x + y)) . n = (vseq . n) . (x + y) ) by Def2, LOPBAN_1:def_9;
then A5: (vseq # (x + y)) . n = ((vseq . n) . x) + ((vseq . n) . y) by VECTSP_1:def_20;
(vseq . n) . y = (vseq # y) . n by Def2;
hence (vseq # (x + y)) . n = ((vseq # x) . n) + ((vseq # y) . n) by A5, Def2; ::_thesis: verum
end;
then A6: vseq # (x + y) = (vseq # x) + (vseq # y) by NORMSP_1:def_2;
( vseq # x is convergent & tseq . x = lim (vseq # x) ) by A1;
hence tseq . (x + y) = (tseq . x) + (tseq . y) by A3, A6, A4, NORMSP_1:25; ::_thesis: verum
end;
A7: 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 rng vseq holds
||.(f . x).|| <= K ) )
proof
let x be Point of X; ::_thesis: ex K being real number st
( 0 <= K & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in rng vseq holds
||.(f . x).|| <= K ) )
vseq # x is convergent by A1;
then ||.(vseq # x).|| is bounded by NORMSP_1:23, SEQ_2:13;
then consider K being real number such that
A8: for n being Element of NAT holds ||.(vseq # x).|| . n < K by SEQ_2:def_3;
A9: for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in rng vseq holds
||.(f . x).|| <= K
proof
let f be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); ::_thesis: ( f in rng vseq implies ||.(f . x).|| <= K )
assume f in rng vseq ; ::_thesis: ||.(f . x).|| <= K
then consider n being set such that
A10: n in NAT and
A11: f = vseq . n by FUNCT_2:11;
reconsider n = n as Element of NAT by A10;
(vseq . n) . x = (vseq # x) . n by Def2;
then ||.(f . x).|| = ||.(vseq # x).|| . n by A11, NORMSP_0:def_4;
hence ||.(f . x).|| <= K by A8; ::_thesis: verum
end;
||.(vseq # x).|| . 0 < K by A8;
then ||.((vseq # x) . 0).|| < K by NORMSP_0:def_4;
then 0 <= K ;
hence ex K being real number st
( 0 <= K & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in rng vseq holds
||.(f . x).|| <= K ) ) by A9; ::_thesis: verum
end;
vseq in Funcs (NAT, the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y))) by FUNCT_2:8;
then ex f0 being Function st
( vseq = f0 & dom f0 = NAT & rng f0 c= the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)) ) by FUNCT_2:def_2;
then consider L being real number such that
A12: 0 <= L and
A13: for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in rng vseq holds
||.f.|| <= L by A7, Th5;
A14: L + 0 < 1 + L by XREAL_1:8;
for n being Element of NAT holds abs (||.vseq.|| . n) < 1 + L
proof
let n be Element of NAT ; ::_thesis: abs (||.vseq.|| . n) < 1 + L
||.(vseq . n).|| <= L by A13, FUNCT_2:4;
then ||.vseq.|| . n <= L by NORMSP_0:def_4;
then A15: ||.vseq.|| . n < 1 + L by A14, XXREAL_0:2;
0 <= ||.(vseq . n).|| ;
then 0 <= ||.vseq.|| . n by NORMSP_0:def_4;
hence abs (||.vseq.|| . n) < 1 + L by A15, ABSVALUE:def_1; ::_thesis: verum
end;
then A16: ||.vseq.|| is bounded by A12, SEQ_2:3;
A17: for x being Point of X holds ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.||
proof
let x be Point of X; ::_thesis: ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.||
A18: ||.x.|| (#) ||.vseq.|| is bounded by A16, SEQM_3:37;
A19: for n being Element of NAT holds ||.((vseq # x) . n).|| <= ||.(vseq . n).|| * ||.x.||
proof
let n be Element of NAT ; ::_thesis: ||.((vseq # x) . n).|| <= ||.(vseq . n).|| * ||.x.||
( (vseq . n) . x = (vseq # x) . n & vseq . n is Lipschitzian LinearOperator of X,Y ) by Def2, LOPBAN_1:def_9;
hence ||.((vseq # x) . n).|| <= ||.(vseq . n).|| * ||.x.|| by LOPBAN_1:32; ::_thesis: verum
end;
A20: for n being Element of NAT holds ||.(vseq # x).|| . n <= (||.x.|| (#) ||.vseq.||) . n
proof
let n be Element of NAT ; ::_thesis: ||.(vseq # x).|| . n <= (||.x.|| (#) ||.vseq.||) . n
A21: ||.(vseq . n).|| = ||.vseq.|| . n by NORMSP_0:def_4;
( ||.(vseq # x).|| . n = ||.((vseq # x) . n).|| & ||.((vseq # x) . n).|| <= ||.(vseq . n).|| * ||.x.|| ) by A19, NORMSP_0:def_4;
hence ||.(vseq # x).|| . n <= (||.x.|| (#) ||.vseq.||) . n by A21, SEQ_1:9; ::_thesis: verum
end;
A22: lim_inf (||.x.|| (#) ||.vseq.||) = (lim_inf ||.vseq.||) * ||.x.|| by A16, Th1;
A23: ( vseq # x is convergent & tseq . x = lim (vseq # x) ) by A1;
then ||.(vseq # x).|| is convergent by LOPBAN_1:20;
then A24: lim ||.(vseq # x).|| = lim_inf ||.(vseq # x).|| by RINFSUP1:89;
||.(vseq # x).|| is bounded by A23, LOPBAN_1:20, SEQ_2:13;
then lim_inf ||.(vseq # x).|| <= lim_inf (||.x.|| (#) ||.vseq.||) by A18, A20, RINFSUP1:91;
hence ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| by A23, A22, A24, LOPBAN_1:20; ::_thesis: verum
end;
now__::_thesis:_for_s_being_real_number_st_0_<_s_holds_
ex_n_being_Element_of_NAT_st_
for_k_being_Element_of_NAT_holds_0_-_s_<_||.vseq.||_._(n_+_k)
let s be real number ; ::_thesis: ( 0 < s implies ex n being Element of NAT st
for k being Element of NAT holds 0 - s < ||.vseq.|| . (n + k) )
assume A25: 0 < s ; ::_thesis: ex n being Element of NAT st
for k being Element of NAT holds 0 - s < ||.vseq.|| . (n + k)
for k being Element of NAT holds 0 - s < ||.vseq.|| . (0 + k)
proof
let k be Element of NAT ; ::_thesis: 0 - s < ||.vseq.|| . (0 + k)
||.(vseq . k).|| = ||.vseq.|| . k by NORMSP_0:def_4;
then 0 <= ||.vseq.|| . k ;
hence 0 - s < ||.vseq.|| . (0 + k) by A25; ::_thesis: verum
end;
hence ex n being Element of NAT st
for k being Element of NAT holds 0 - s < ||.vseq.|| . (n + k) ; ::_thesis: verum
end;
then A26: 0 <= lim_inf ||.vseq.|| by A16, RINFSUP1:82;
A27: for x being Point of X
for r being Element of REAL holds tseq . (r * x) = r * (tseq . x)
proof
let x be Point of X; ::_thesis: for r being Element of REAL holds tseq . (r * x) = r * (tseq . x)
let r be Element of REAL ; ::_thesis: tseq . (r * x) = r * (tseq . x)
A28: tseq . x = lim (vseq # x) by A1;
A29: now__::_thesis:_for_n_being_Element_of_NAT_holds_(vseq_#_(r_*_x))_._n_=_r_*_((vseq_#_x)_._n)
let n be Element of NAT ; ::_thesis: (vseq # (r * x)) . n = r * ((vseq # x) . n)
( vseq . n is Lipschitzian LinearOperator of X,Y & (vseq # (r * x)) . n = (vseq . n) . (r * x) ) by Def2, LOPBAN_1:def_9;
then (vseq # (r * x)) . n = r * ((vseq . n) . x) by LOPBAN_1:def_5;
hence (vseq # (r * x)) . n = r * ((vseq # x) . n) by Def2; ::_thesis: verum
end;
tseq . (r * x) = lim (vseq # (r * x)) by A1;
then tseq . (r * x) = lim (r * (vseq # x)) by A29, NORMSP_1:def_5;
hence tseq . (r * x) = r * (tseq . x) by A1, A28, NORMSP_1:28; ::_thesis: verum
end;
then reconsider tseq1 = tseq as Lipschitzian LinearOperator of X,Y by A2, A17, A26, VECTSP_1:def_20, LOPBAN_1:def_5, LOPBAN_1:def_8;
for ttseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ttseq = tseq holds
||.ttseq.|| <= lim_inf ||.vseq.||
proof
for k being real number st k in { ||.(tseq . x1).|| where x1 is Point of X : ||.x1.|| <= 1 } holds
k <= lim_inf ||.vseq.||
proof
let k be real number ; ::_thesis: ( k in { ||.(tseq . x1).|| where x1 is Point of X : ||.x1.|| <= 1 } implies k <= lim_inf ||.vseq.|| )
assume k in { ||.(tseq . x1).|| where x1 is Point of X : ||.x1.|| <= 1 } ; ::_thesis: k <= lim_inf ||.vseq.||
then consider x being Point of X such that
A30: ( k = ||.(tseq . x).|| & ||.x.|| <= 1 ) ;
( k <= (lim_inf ||.vseq.||) * ||.x.|| & (lim_inf ||.vseq.||) * ||.x.|| <= lim_inf ||.vseq.|| ) by A17, A26, A30, XREAL_1:153;
hence k <= lim_inf ||.vseq.|| by XXREAL_0:2; ::_thesis: verum
end;
then A31: upper_bound (PreNorms tseq1) <= lim_inf ||.vseq.|| by SEQ_4:45;
let ttseq be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); ::_thesis: ( ttseq = tseq implies ||.ttseq.|| <= lim_inf ||.vseq.|| )
assume ttseq = tseq ; ::_thesis: ||.ttseq.|| <= lim_inf ||.vseq.||
hence ||.ttseq.|| <= lim_inf ||.vseq.|| by A31, LOPBAN_1:30; ::_thesis: verum
end;
hence ( tseq is Lipschitzian LinearOperator of X,Y & ( for x being Point of X holds ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) & ( for ttseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ttseq = tseq holds
||.ttseq.|| <= lim_inf ||.vseq.|| ) ) by A2, A27, A17, A26, VECTSP_1:def_20, LOPBAN_1:def_5, LOPBAN_1:def_8; ::_thesis: verum
end;
begin
theorem Th7: :: LOPBAN_5:7
for X being RealBanachSpace
for X0 being Subset of (LinearTopSpaceNorm X)
for Y being RealBanachSpace
for vseq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st X0 is dense & ( for x being Point of X st x in X0 holds
vseq # x is convergent ) & ( for x being Point of X ex K being real number st
( 0 <= K & ( for n being Element of NAT holds ||.((vseq # x) . n).|| <= K ) ) ) holds
for x being Point of X holds vseq # x is convergent
proof
let X be RealBanachSpace; ::_thesis: for X0 being Subset of (LinearTopSpaceNorm X)
for Y being RealBanachSpace
for vseq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st X0 is dense & ( for x being Point of X st x in X0 holds
vseq # x is convergent ) & ( for x being Point of X ex K being real number st
( 0 <= K & ( for n being Element of NAT holds ||.((vseq # x) . n).|| <= K ) ) ) holds
for x being Point of X holds vseq # x is convergent
let X0 be Subset of (LinearTopSpaceNorm X); ::_thesis: for Y being RealBanachSpace
for vseq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st X0 is dense & ( for x being Point of X st x in X0 holds
vseq # x is convergent ) & ( for x being Point of X ex K being real number st
( 0 <= K & ( for n being Element of NAT holds ||.((vseq # x) . n).|| <= K ) ) ) holds
for x being Point of X holds vseq # x is convergent
let Y be RealBanachSpace; ::_thesis: for vseq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st X0 is dense & ( for x being Point of X st x in X0 holds
vseq # x is convergent ) & ( for x being Point of X ex K being real number st
( 0 <= K & ( for n being Element of NAT holds ||.((vseq # x) . n).|| <= K ) ) ) holds
for x being Point of X holds vseq # x is convergent
let vseq be sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)); ::_thesis: ( X0 is dense & ( for x being Point of X st x in X0 holds
vseq # x is convergent ) & ( for x being Point of X ex K being real number st
( 0 <= K & ( for n being Element of NAT holds ||.((vseq # x) . n).|| <= K ) ) ) implies for x being Point of X holds vseq # x is convergent )
assume A1: X0 is dense ; ::_thesis: ( ex x being Point of X st
( x in X0 & not vseq # x is convergent ) or ex x being Point of X st
for K being real number holds
( not 0 <= K or ex n being Element of NAT st not ||.((vseq # x) . n).|| <= K ) or for x being Point of X holds vseq # x is convergent )
set T = rng vseq;
assume A2: for x being Point of X st x in X0 holds
vseq # x is convergent ; ::_thesis: ( ex x being Point of X st
for K being real number holds
( not 0 <= K or ex n being Element of NAT st not ||.((vseq # x) . n).|| <= K ) or for x being Point of X holds vseq # x is convergent )
vseq in Funcs (NAT, the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y))) by FUNCT_2:8;
then ex f0 being Function st
( vseq = f0 & dom f0 = NAT & rng f0 c= the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)) ) by FUNCT_2:def_2;
then reconsider T = rng vseq as Subset of (R_NormSpace_of_BoundedLinearOperators (X,Y)) ;
assume A3: for x being Point of X ex K being real number st
( 0 <= K & ( for n being Element of NAT holds ||.((vseq # x) . n).|| <= K ) ) ; ::_thesis: for x being Point of X holds vseq # x is convergent
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 ) )
proof
let x be Point of X; ::_thesis: 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 ) )
consider K being real number such that
A4: 0 <= K and
A5: for n being Element of NAT holds ||.((vseq # x) . n).|| <= K by A3;
take K ; ::_thesis: ( 0 <= K & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.(f . x).|| <= K ) )
now__::_thesis:_for_f_being_Point_of_(R_NormSpace_of_BoundedLinearOperators_(X,Y))_st_f_in_T_holds_
||.(f_._x).||_<=_K
let f be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); ::_thesis: ( f in T implies ||.(f . x).|| <= K )
assume f in T ; ::_thesis: ||.(f . x).|| <= K
then consider n being set such that
A6: n in NAT and
A7: f = vseq . n by FUNCT_2:11;
reconsider n = n as Element of NAT by A6;
||.(f . x).|| = ||.((vseq # x) . n).|| by A7, Def2;
hence ||.(f . x).|| <= K by A5; ::_thesis: verum
end;
hence ( 0 <= K & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.(f . x).|| <= K ) ) by A4; ::_thesis: verum
end;
then consider L being real number such that
A8: 0 <= L and
A9: for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds
||.f.|| <= L by Th5;
set M = 1 + L;
A10: L + 0 < 1 + L by XREAL_1:8;
A11: for f being Lipschitzian LinearOperator of X,Y st f in T holds
for x, y being Point of X holds ||.((f . x) - (f . y)).|| <= (1 + L) * ||.(x - y).||
proof
let f be Lipschitzian LinearOperator of X,Y; ::_thesis: ( f in T implies for x, y being Point of X holds ||.((f . x) - (f . y)).|| <= (1 + L) * ||.(x - y).|| )
reconsider f1 = f as Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) by LOPBAN_1:def_9;
assume f in T ; ::_thesis: for x, y being Point of X holds ||.((f . x) - (f . y)).|| <= (1 + L) * ||.(x - y).||
then ||.f1.|| <= L by A9;
then A12: ||.f1.|| < 1 + L by A10, XXREAL_0:2;
let x, y be Point of X; ::_thesis: ||.((f . x) - (f . y)).|| <= (1 + L) * ||.(x - y).||
||.((f . x) - (f . y)).|| = ||.((f . x) + ((- 1) * (f . y))).|| by RLVECT_1:16;
then ||.((f . x) - (f . y)).|| = ||.((f . x) + (f . ((- 1) * y))).|| by LOPBAN_1:def_5;
then ||.((f . x) - (f . y)).|| = ||.(f . (x + ((- 1) * y))).|| by VECTSP_1:def_20;
then A13: ||.((f . x) - (f . y)).|| = ||.(f . (x - y)).|| by RLVECT_1:16;
( ||.(f . (x - y)).|| <= ||.f1.|| * ||.(x - y).|| & ||.f1.|| * ||.(x - y).|| <= (1 + L) * ||.(x - y).|| ) by A12, LOPBAN_1:32, XREAL_1:64;
hence ||.((f . x) - (f . y)).|| <= (1 + L) * ||.(x - y).|| by A13, XXREAL_0:2; ::_thesis: verum
end;
hereby ::_thesis: verum
let x be Point of X; ::_thesis: vseq # x is convergent
for TK1 being Real st TK1 > 0 holds
ex n0 being Element of NAT st
for n, m being Element of NAT st n >= n0 & m >= n0 holds
||.(((vseq # x) . n) - ((vseq # x) . m)).|| < TK1
proof
let TK1 be Real; ::_thesis: ( TK1 > 0 implies ex n0 being Element of NAT st
for n, m being Element of NAT st n >= n0 & m >= n0 holds
||.(((vseq # x) . n) - ((vseq # x) . m)).|| < TK1 )
assume A14: TK1 > 0 ; ::_thesis: ex n0 being Element of NAT st
for n, m being Element of NAT st n >= n0 & m >= n0 holds
||.(((vseq # x) . n) - ((vseq # x) . m)).|| < TK1
A15: 0 < TK1 / 3 by A14, XREAL_1:222;
set V = { z where z is Point of X : ||.(x - z).|| < TK1 / (3 * (1 + L)) } ;
{ z where z is Point of X : ||.(x - z).|| < TK1 / (3 * (1 + L)) } c= the carrier of X
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in { z where z is Point of X : ||.(x - z).|| < TK1 / (3 * (1 + L)) } or s in the carrier of X )
assume s in { z where z is Point of X : ||.(x - z).|| < TK1 / (3 * (1 + L)) } ; ::_thesis: s in the carrier of X
then ex z being Point of X st
( s = z & ||.(x - z).|| < TK1 / (3 * (1 + L)) ) ;
hence s in the carrier of X ; ::_thesis: verum
end;
then reconsider V = { z where z is Point of X : ||.(x - z).|| < TK1 / (3 * (1 + L)) } as Subset of (LinearTopSpaceNorm X) by NORMSP_2:def_4;
0 < 3 * (1 + L) by A8, XREAL_1:129;
then 0 < TK1 / (3 * (1 + L)) by A14, XREAL_1:139;
then ||.(x - x).|| < TK1 / (3 * (1 + L)) by NORMSP_1:6;
then ( V is open & x in V ) by NORMSP_2:23;
then X0 meets V by A1, TOPS_1:45;
then consider s being set such that
A16: s in X0 and
A17: s in V by XBOOLE_0:3;
consider y being Point of X such that
A18: s = y and
A19: ||.(x - y).|| < TK1 / (3 * (1 + L)) by A17;
for s being Real st 0 < s holds
ex n1 being Element of NAT st
for m1 being Element of NAT st n1 <= m1 holds
||.(((vseq # y) . m1) - ((vseq # y) . n1)).|| < s by A2, A16, A18, LOPBAN_3:4;
then vseq # y is Cauchy_sequence_by_Norm by LOPBAN_3:5;
then consider n0 being Element of NAT such that
A20: for n, m being Element of NAT st n >= n0 & m >= n0 holds
||.(((vseq # y) . n) - ((vseq # y) . m)).|| < TK1 / 3 by A15, RSSPACE3:8;
take n0 ; ::_thesis: for n, m being Element of NAT st n >= n0 & m >= n0 holds
||.(((vseq # x) . n) - ((vseq # x) . m)).|| < TK1
for n, m being Element of NAT st n >= n0 & m >= n0 holds
||.(((vseq # x) . n) - ((vseq # x) . m)).|| < TK1
proof
let n, m be Element of NAT ; ::_thesis: ( n >= n0 & m >= n0 implies ||.(((vseq # x) . n) - ((vseq # x) . m)).|| < TK1 )
reconsider f = vseq . n as Lipschitzian LinearOperator of X,Y by LOPBAN_1:def_9;
reconsider g = vseq . m as Lipschitzian LinearOperator of X,Y by LOPBAN_1:def_9;
||.(((vseq # x) . n) - ((vseq # y) . m)).|| <= ||.(((vseq # x) . n) - ((vseq # y) . n)).|| + ||.(((vseq # y) . n) - ((vseq # y) . m)).|| by NORMSP_1:10;
then A21: ||.(((vseq # x) . n) - ((vseq # y) . m)).|| + ||.(((vseq # y) . m) - ((vseq # x) . m)).|| <= (||.(((vseq # x) . n) - ((vseq # y) . n)).|| + ||.(((vseq # y) . n) - ((vseq # y) . m)).||) + ||.(((vseq # y) . m) - ((vseq # x) . m)).|| by XREAL_1:6;
assume ( n >= n0 & m >= n0 ) ; ::_thesis: ||.(((vseq # x) . n) - ((vseq # x) . m)).|| < TK1
then ||.(((vseq # y) . n) - ((vseq # y) . m)).|| < TK1 / 3 by A20;
then ||.(((vseq # x) . n) - ((vseq # y) . n)).|| + ||.(((vseq # y) . n) - ((vseq # y) . m)).|| < ||.(((vseq # x) . n) - ((vseq # y) . n)).|| + (TK1 / 3) by XREAL_1:8;
then A22: (||.(((vseq # x) . n) - ((vseq # y) . n)).|| + ||.(((vseq # y) . n) - ((vseq # y) . m)).||) + ||.(((vseq # y) . m) - ((vseq # x) . m)).|| < (||.(((vseq # x) . n) - ((vseq # y) . n)).|| + (TK1 / 3)) + ||.(((vseq # y) . m) - ((vseq # x) . m)).|| by XREAL_1:8;
||.(((vseq # x) . m) - ((vseq # y) . m)).|| = ||.(((vseq . m) . x) - ((vseq # y) . m)).|| by Def2;
then ||.(((vseq # x) . m) - ((vseq # y) . m)).|| = ||.((g . x) - (g . y)).|| by Def2;
then A23: ||.(((vseq # x) . m) - ((vseq # y) . m)).|| <= (1 + L) * ||.(x - y).|| by A11, FUNCT_2:4;
(1 + L) * ||.(x - y).|| < (1 + L) * (TK1 / (3 * (1 + L))) by A8, A19, XREAL_1:68;
then (1 + L) * ||.(x - y).|| < TK1 / 3 by A8, XCMPLX_1:92;
then ||.(((vseq # x) . m) - ((vseq # y) . m)).|| < TK1 / 3 by A23, XXREAL_0:2;
then ||.(((vseq # y) . m) - ((vseq # x) . m)).|| < TK1 / 3 by NORMSP_1:7;
then A24: ((TK1 / 3) + (TK1 / 3)) + ||.(((vseq # y) . m) - ((vseq # x) . m)).|| < ((TK1 / 3) + (TK1 / 3)) + (TK1 / 3) by XREAL_1:8;
||.(((vseq # x) . n) - ((vseq # y) . n)).|| = ||.(((vseq . n) . x) - ((vseq # y) . n)).|| by Def2;
then ||.(((vseq # x) . n) - ((vseq # y) . n)).|| = ||.((f . x) - (f . y)).|| by Def2;
then A25: ||.(((vseq # x) . n) - ((vseq # y) . n)).|| <= (1 + L) * ||.(x - y).|| by A11, FUNCT_2:4;
||.(((vseq # x) . n) - ((vseq # x) . m)).|| <= ||.(((vseq # x) . n) - ((vseq # y) . m)).|| + ||.(((vseq # y) . m) - ((vseq # x) . m)).|| by NORMSP_1:10;
then ||.(((vseq # x) . n) - ((vseq # x) . m)).|| <= (||.(((vseq # x) . n) - ((vseq # y) . n)).|| + ||.(((vseq # y) . n) - ((vseq # y) . m)).||) + ||.(((vseq # y) . m) - ((vseq # x) . m)).|| by A21, XXREAL_0:2;
then A26: ||.(((vseq # x) . n) - ((vseq # x) . m)).|| < (||.(((vseq # x) . n) - ((vseq # y) . n)).|| + (TK1 / 3)) + ||.(((vseq # y) . m) - ((vseq # x) . m)).|| by A22, XXREAL_0:2;
(1 + L) * ||.(x - y).|| < (1 + L) * (TK1 / (3 * (1 + L))) by A8, A19, XREAL_1:68;
then (1 + L) * ||.(x - y).|| < TK1 / 3 by A8, XCMPLX_1:92;
then ||.(((vseq # x) . n) - ((vseq # y) . n)).|| < TK1 / 3 by A25, XXREAL_0:2;
then ||.(((vseq # x) . n) - ((vseq # y) . n)).|| + (TK1 / 3) < (TK1 / 3) + (TK1 / 3) by XREAL_1:8;
then (||.(((vseq # x) . n) - ((vseq # y) . n)).|| + (TK1 / 3)) + ||.(((vseq # y) . m) - ((vseq # x) . m)).|| < ((TK1 / 3) + (TK1 / 3)) + ||.(((vseq # y) . m) - ((vseq # x) . m)).|| by XREAL_1:8;
then (||.(((vseq # x) . n) - ((vseq # y) . n)).|| + (TK1 / 3)) + ||.(((vseq # y) . m) - ((vseq # x) . m)).|| < ((TK1 / 3) + (TK1 / 3)) + (TK1 / 3) by A24, XXREAL_0:2;
hence ||.(((vseq # x) . n) - ((vseq # x) . m)).|| < TK1 by A26, XXREAL_0:2; ::_thesis: verum
end;
hence for n, m being Element of NAT st n >= n0 & m >= n0 holds
||.(((vseq # x) . n) - ((vseq # x) . m)).|| < TK1 ; ::_thesis: verum
end;
then vseq # x is Cauchy_sequence_by_Norm by RSSPACE3:8;
hence vseq # x is convergent by LOPBAN_1:def_15; ::_thesis: verum
end;
end;
theorem :: LOPBAN_5:8
for X, Y being RealBanachSpace
for X0 being Subset of (LinearTopSpaceNorm X)
for vseq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st X0 is dense & ( for x being Point of X st x in X0 holds
vseq # x is convergent ) & ( for x being Point of X ex K being real number st
( 0 <= K & ( for n being Element of NAT holds ||.((vseq # x) . n).|| <= K ) ) ) holds
ex tseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st
( ( for x being Point of X holds
( vseq # x is convergent & tseq . x = lim (vseq # x) & ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) ) & ||.tseq.|| <= lim_inf ||.vseq.|| )
proof
let X, Y be RealBanachSpace; ::_thesis: for X0 being Subset of (LinearTopSpaceNorm X)
for vseq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st X0 is dense & ( for x being Point of X st x in X0 holds
vseq # x is convergent ) & ( for x being Point of X ex K being real number st
( 0 <= K & ( for n being Element of NAT holds ||.((vseq # x) . n).|| <= K ) ) ) holds
ex tseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st
( ( for x being Point of X holds
( vseq # x is convergent & tseq . x = lim (vseq # x) & ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) ) & ||.tseq.|| <= lim_inf ||.vseq.|| )
let X0 be Subset of (LinearTopSpaceNorm X); ::_thesis: for vseq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st X0 is dense & ( for x being Point of X st x in X0 holds
vseq # x is convergent ) & ( for x being Point of X ex K being real number st
( 0 <= K & ( for n being Element of NAT holds ||.((vseq # x) . n).|| <= K ) ) ) holds
ex tseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st
( ( for x being Point of X holds
( vseq # x is convergent & tseq . x = lim (vseq # x) & ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) ) & ||.tseq.|| <= lim_inf ||.vseq.|| )
let vseq be sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)); ::_thesis: ( X0 is dense & ( for x being Point of X st x in X0 holds
vseq # x is convergent ) & ( for x being Point of X ex K being real number st
( 0 <= K & ( for n being Element of NAT holds ||.((vseq # x) . n).|| <= K ) ) ) implies ex tseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st
( ( for x being Point of X holds
( vseq # x is convergent & tseq . x = lim (vseq # x) & ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) ) & ||.tseq.|| <= lim_inf ||.vseq.|| ) )
assume A1: X0 is dense ; ::_thesis: ( ex x being Point of X st
( x in X0 & not vseq # x is convergent ) or ex x being Point of X st
for K being real number holds
( not 0 <= K or ex n being Element of NAT st not ||.((vseq # x) . n).|| <= K ) or ex tseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st
( ( for x being Point of X holds
( vseq # x is convergent & tseq . x = lim (vseq # x) & ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) ) & ||.tseq.|| <= lim_inf ||.vseq.|| ) )
deffunc H1( Point of X) -> Element of the carrier of Y = lim (vseq # $1);
assume A2: for x being Point of X st x in X0 holds
vseq # x is convergent ; ::_thesis: ( ex x being Point of X st
for K being real number holds
( not 0 <= K or ex n being Element of NAT st not ||.((vseq # x) . n).|| <= K ) or ex tseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st
( ( for x being Point of X holds
( vseq # x is convergent & tseq . x = lim (vseq # x) & ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) ) & ||.tseq.|| <= lim_inf ||.vseq.|| ) )
consider tseq being Function of X,Y such that
A3: for x being Point of X holds tseq . x = H1(x) from FUNCT_2:sch_4();
assume for x being Point of X ex K being real number st
( 0 <= K & ( for n being Element of NAT holds ||.((vseq # x) . n).|| <= K ) ) ; ::_thesis: ex tseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st
( ( for x being Point of X holds
( vseq # x is convergent & tseq . x = lim (vseq # x) & ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) ) & ||.tseq.|| <= lim_inf ||.vseq.|| )
then A4: for x being Point of X holds vseq # x is convergent by A1, A2, Th7;
then reconsider tseq = tseq as Lipschitzian LinearOperator of X,Y by A3, Th6;
reconsider tseq = tseq as Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) by LOPBAN_1:def_9;
take tseq ; ::_thesis: ( ( for x being Point of X holds
( vseq # x is convergent & tseq . x = lim (vseq # x) & ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) ) & ||.tseq.|| <= lim_inf ||.vseq.|| )
thus ( ( for x being Point of X holds
( vseq # x is convergent & tseq . x = lim (vseq # x) & ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) ) & ||.tseq.|| <= lim_inf ||.vseq.|| ) by A4, A3, Th6; ::_thesis: verum
end;